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

decision treeresolutioncliquetheory of computation

Mathematics Subject Classification ID

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

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

• scientific article; zbMATH DE number 1860652 (Why is no real title available?)
• scientific article; zbMATH DE number 5485586 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A characterization of tree-like resolution size
• A combinatorial characterization of resolution width
• A combinatorial characterization of treelike resolution space
• 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
• 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 Complexity of DPLL Search Procedures
• Parameterized bounded-depth Frege is not optimal
• Pebble games, proof complexity, and time-space trade-offs
• Reducibility among combinatorial problems
• Short proofs are narrow—resolution made simple
• Space Complexity in Propositional Calculus
• Space bounds for resolution
• The Complexity of Propositional Proofs
• The Pebbling Problem is Complete in Polynomial Space
• The intractability of resolution
• The monotone complexity of \(k\)-clique on random graphs
• The relative efficiency of propositional proof systems
• The resolution complexity of independent sets and vertex covers in random graphs

Cited in

(3)

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

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)