A sharp threshold in proof complexity

No abstract is available for this paper.

• Publication year

  2001

• Venue

  Symposium on the Theory of Computing

• Publication date

  2001-07-06

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1145/380752.380820
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• A machine program for theorem-proving

  2011cited by this paper
• The phase transition in 1-in-k SAT and NAE 3-SAT

  2001cited by this paper
• Short proofs are narrow—resolution made simple

  2001cited by this paper
• Lower bounds for random 3-SAT via differential equations

  2001cited by this paper
• Rigorous results for random (2+p)-SAT

  2001cited by this paper
• Optimal myopic algorithms for random 3-SAT

  2000cited by this paper
• Bounding the unsatisfiability threshold of random 3-SAT

  2000cited by this paper
• Threshold phenomena in random graph colouring and satisfiability

  1999cited by this paper
• Symbolic Model Checking without BDDs

  1999cited by this paper
• 2+p‐SAT: Relation of typical‐case complexity to the nature of the phase transition

  1999cited by this paper
• Sharp thresholds of graph properties, and the -sat problem

  1999cited by this paper
• Determining computational complexity from characteristic ‘phase transitions’

  1999cited by this paper
• Random Cnf’s are Hard for the Polynomial Calculus

  1999cited by this paper
• Boosting Combinatorial Search Through Randomization

  1998cited by this paper
• On the complexity of unsatisfiability proofs for random k-CNF formulas

  1998cited by this paper
• Analysis of Two Simple Heuristics on a Random Instance of k-SAT

  1996influential reference
• Encoding Plans in Propositional Logic

  1996cited by this paper
• Phase transition and search cost in the 2+p-sat problem

  1996cited by this paper
• Generating Hard Satisfiability Problems

  1996cited by this paper
• Pushing the Envelope: Planning, Propositional Logic and Stochastic Search

  1996cited by this paper
• Critical Behavior in the Satisfiability of Random Boolean Expressions

  1994cited by this paper
• Domain-Independent Extensions to GSAT: Solving Large Structured Satisfiability Problems

  1993cited by this paper
• A New Method for Solving Hard Satis ability Problems

  1992cited by this paper
• A Threshold for Unsatisfiability

  1992cited by this paper
• Mick gets some (the odds are on his side) (satisfiability)

  1992cited by this paper
• Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k satisfiability problem

  1990cited by this paper
• Surveys in Combinatorics, 1989: On the method of bounded differences

  1989cited by this paper
• Many hard examples for resolution

  1988cited by this paper
• A Computing Procedure for Quantification Theory

  1960cited by this paper

• Understanding the Empirical Hardness of Random Optimisation Problems

  2019cites this paper
• Understanding and Enhancing CDCL-based SAT Solvers

  2018cites this paper
• Experimental analyses of the K-hidden algorithm

  2017cites this paper
• Hiding multiple solutions in a hard 3-SAT formula

  2015cites this paper
• A fine-grained algorithm for generating hard-toreverse negative databases

  2015cites this paper
• Resolution and Parallelizability: Barriers to the Efficient Parallelization of SAT Solvers

  2013cites this paper
• Unsatisfiability Bounds for Random Constraint Satisfaction Problems from an Energetic Interpolation Method

  2013cites this paper
• Numerical evidence for phase transitions of NP-complete problems for instances drawn from Lévy-stable distributions

  2011cites this paper
• Consistency and Random Constraint Satisfaction Models

  2011influential citation
• Formula Caching in DPLL

  2010cites this paper
• Universality in two-dimensional enhancement percolation

  2008cites this paper
• On the relation among answer set solvers

  2008cites this paper
• Phase Transitions and Complexity of Weighted Satisfiability and Other Intractable Parameterized Problems

  2008cites this paper
• Chapter 2 Satisfiability Solvers

  2008cites this paper
• Random Instances of W[2]-Complete Problems: Thresholds, Complexity, and Algorithms

  2008cites this paper
• A Fixed-Parameter Algorithm for Random Instances of Weighted d-CNF Satisfiability

  2008influential citation
• Satisfying Assignments of Random Boolean Constraint Satisfaction Problems: Clusters and Overlaps

  2007cites this paper
• The state of SAT

  2007cites this paper
• The satisfiability threshold for randomly generated binary constraint satisfaction problems

  2006cites this paper
• The probabilistic analysis of a greedy satisfiability algorithm

  2006cites this paper
• Protecting data privacy through hard-to-reverse negative databases

  2006cites this paper
• MAX k-CUT and approximating the chromatic number of random graphs

  2006cites this paper
• Sharp thresholds for constraint satisfaction problems and homomorphisms

  2006cites this paper
• On the Threshold of Having a Linear Treewidth in Random Graphs

  2006cites this paper
• Introduction: Where Statistical Physics Mects Computation

  2006cites this paper
• Generating Hard Satisfiable Formulas by Hiding Solutions Deceptively

  2005cites this paper
• Restarts and exponential acceleration of the Davis-Putnam-Loveland-Logemann algorithm: A large deviation analysis of the generalized unit clause heuristic for random 3-SAT

  2005cites this paper
• Exploiting phase transitions for fusion optimization problems

  2005cites this paper
• A Generating Function Method for the Average-Case Analysis of DPLL

  2005cites this paper
• On the Relation Between Answer Set and SAT Procedures (or, Between cmodels and smodels)

  2005cites this paper
• Agile Satellite Scheduling via Permutation Search with Constraint Propagation

  2005cites this paper
• Three-query PCPs with perfect completeness over non-Boolean domains

  2005cites this paper
• Restarts and Exponential Acceleration of the Davis–Putnam–Loveland–Logemann Algorithm: A Large Deviation Analysis of the Generalized Unit Clause Heuristic for Random 3-SAT

  2005cites this paper
• Algorithmic applications of propositional proof complexity

  2005cites this paper
• Hiding satisfying assignments

  2005cites this paper
• Cores in random hypergraphs and Boolean formulas

  2005cites this paper
• Exponential bounds for DPLL below the satisfiability threshold

  2004cites this paper
• Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances

  2004cites this paper
• Towards Understanding and Harnessing the Potential of Clause Learning

  2004cites this paper
• The pure literal rule threshold and cores in random hypergraphs

  2004cites this paper
• Optimal length tree-like resolution refutations for 2SAT formulas

  2004influential citation
• Consistency and Random Constraint Satisfaction Models with a High Constraint Tightness

  2004cites this paper
• Exponential Lower Bounds for the Running Time of DPLL Algorithms on Satisfiable Formulas

  2004cites this paper
• Analysis of Backtracking Procedures for Random Decision Problems

  2004cites this paper
• How Much Backtracking Does It Take to Color Random Graphs? Rigorous Results on Heavy Tails

  2004cites this paper
• Hiding Satisfying Assignments: Two Are Better than One

  2004cites this paper
• Clustering Large Graphs via the Singular Value Decomposition

  2004cites this paper
• On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search

  2003cites this paper
• Hard satisfiable formulas for DPLL-type algorithms

  2003cites this paper
• Hard satisfiable instances for DPLL-type algorithms

  2003cites this paper
• Understanding the power of clause learning

  2003cites this paper
• Ten Challenges Redux: Recent Progress in Propositional Reasoning and Search

  2003cites this paper
• Analysis of the Random Walk Algorithm on Random -CNFs

  2003cites this paper
• Local Search on SAT-encoded Colouring Problems

  2003cites this paper
• Random k-SAT: Two Moments Suffice to Cross a Sharp Threshold

  2003cites this paper
• Linear upper bounds for random walk on small density random 3-CNFs

  2003cites this paper
• The resolution complexity of random constraint satisfaction problems

  2003cites this paper
• Ju n 20 02 Restart method and exponential acceleration of random 3SAT instances resolutions : a large deviation analysis of the Davis – Putnam – Loveland – Logemann algorithm

  2002cites this paper
• Models and thresholds for random constraint satisfaction problems

  2002cites this paper
• Resolution Complexity of Random Constraints

  2002cites this paper
• Building State-of-the-Art SAT Solvers

  2002cites this paper
• Analysisof theRandomWalk Algorithm onRandom -CNFs

  2002cites this paper
• First report on an adaptive density based branching rule for DLL-like SAT solvers , using a database for mixed random conjunctive normal forms created using the Advanced Encryption Standard ( AES )

  2002cites this paper
• Phase Transitions and all that

  2002cites this paper
• The probabilistic analysis of a greedy satisfiability algorithm

  2002cites this paper
• Restart method and exponential acceleration of random 3-SAT instances resolutions: a large deviation analysis of the Davis-Putnam-Loveland-Logemann algorithm

  2002cites this paper
• A Gap in Average Proof Complexity

  2002cites this paper
• On Determining the Minimum Length, Tree-Like Resolution Refutation of 2SAT, and Extended 2SAT Formulas

  2002cites this paper
• Efficient conflict driven learning in a Boolean satisfiability solver

  2001cites this paper
• Local Search and Backtracking vs Non-Systematic Backtracking

  2001cites this paper
• A Random Walk in Statistical Physics

  2001cites this paper
• Chaff: engineering an efficient SAT solver

  2001cites this paper
• A tabu search method guided by shifting bottleneck for the job shop scheduling problem

  2000cites this paper
• Random 3-SAT: The Plot Thickens

  2000influential citation
• Ju n 20 05 A generating function method for the average-case analysis of DPLL

  year unknowncites this paper
• Handbook of Knowledge Representation Edited Satisfiability Solvers

  year unknowncites this paper
• Clairvoyant Scheduling with Relative Timing Constraints

  year unknowncites this paper