A sharp threshold in proof complexity yields lower bounds for satisfiability search

DOI10.1016/j.jcss.2003.07.011zbMath1093.03033OpenAlexW2062671967MaRDI QIDQ1887710

Yanyan Li

Publication date: 22 November 2004

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/1807/9460

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Complexity of proofs (03F20)

Related Items (7)

Advice complexity of adaptive priority algorithms ⋮ A NEW UPPER BOUND FOR RANDOM (2 + p)-SAT BY FLIPPING TWO VARIABLES ⋮ Limitations of restricted branching in clause learning ⋮ Statistical and algebraic analysis of a family of random Boolean equations ⋮ The solution space geometry of random linear equations ⋮ Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT ⋮ When does the giant component bring unsatisfiability?

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A threshold for unsatisfiability
• Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k-satisfiability problem
• Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
• Generating hard satisfiability problems
• The scaling window of the 2-SAT transition
• Critical Behavior in the Satisfiability of Random Boolean Expressions
• Setting 2 variables at a time yields a new lower bound for random 3-SAT (extended abstract)
• Many hard examples for resolution
• The threshold for random k-SAT is 2 ^k (ln 2 - O(k))
• Sharp thresholds of graph properties, and the $k$-sat problem
• Short proofs are narrow—resolution made simple
• Bounding the unsatisfiability threshold of random 3-SAT
• Analysis of Two Simple Heuristics on a Random Instance ofk-sat
• Determining computational complexity from characteristic ‘phase transitions’
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Rigorous results for random (\(2+p)\)-SAT
• Lower bounds for random 3-SAT via differential equations

This page was built for publication: A sharp threshold in proof complexity yields lower bounds for satisfiability search