Cliques enumeration and tree-like resolution proofs

DOI10.1016/J.IPL.2018.03.001MaRDI QIDQ1708271zbMATH OpenOpenAlexWikidataFDO

Authors Massimo Lauria

Publication date 5 April 2018

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ipl.2018.03.001

zbMATH Keywords

cliquedecision treeresolutiontheory of computation

Mathematics Subject Classification ID

Complexity of proofs (03F20) Vertex subsets with special properties (dominating sets, independent sets, cliques, etc.) (05C69) Analysis of algorithms and problem complexity (68Q25) Graph theory (including graph drawing) in computer science (68R10)

Recommendations

• Clique Is Hard on Average for Regular Resolution
• Clique is hard on average for regular resolution
• Parameterized complexity of DPLL search procedures
• Parameterized Complexity of DPLL Search Procedures
• Short proofs are narrow -- resolution made simple

Cites work

• A characterization of tree-like resolution size
• A combinatorial characterization of resolution width
• A combinatorial characterization of treelike resolution space
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Clique is hard on average for regular resolution
• Clique is hard to approximate within \(n^{1-\epsilon}\)
• Concentration of Measure for the Analysis of Randomized Algorithms
• Finding, minimizing, and counting weighted subgraphs
• From small space to small width in resolution
• Fundamentals of parameterized complexity
• GRASP: a search algorithm for propositional satisfiability
• scientific article; zbMATH DE number 1860652 (Why is no real title available?)
• scientific article; zbMATH DE number 5485586 (Why is no real title available?)
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds based on the exponential time hypothesis
• Narrow proofs may be spacious, separating space and width in resolution
• Near optimal seperation of tree-like and general resolution
• Non-Ramsey graphs are c n-universal
• On the complexity of k-SAT
• Optimality of size-width tradeoffs for resolution
• Parameterized bounded-depth Frege is not optimal
• Parameterized Complexity of DPLL Search Procedures
• Pebble games, proof complexity, and time-space trade-offs
• Reducibility among combinatorial problems
• Short proofs are narrow—resolution made simple
• Space bounds for resolution
• Space Complexity in Propositional Calculus
• The Complexity of Propositional Proofs
• The intractability of resolution
• The monotone complexity of \(k\)-clique on random graphs
• The Pebbling Problem is Complete in Polynomial Space
• The relative efficiency of propositional proof systems
• The resolution complexity of independent sets and vertex covers in random graphs

Cited in

(3)

• Clique Is Hard on Average for Regular Resolution
• Algorithms – ESA 2005
• Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024

Describes a project that uses

Uses Software

• Chaff

This page was built for publication: Cliques enumeration and tree-like resolution proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1708271)