Finding the Hardest Formulas for Resolution

A CNF formula is harder than another CNF formula with the same number of clauses if it requires a longer resolution proof. In this paper we introduce resolution hardness numbers; they give for m=1,2,... the length of a shortest proof of a hardest formula on m clauses. We compute the first ten resolution hardness numbers, along with the corresponding hardest formulas. To achieve this, we devise a candidate filtering and symmetry breaking search scheme for limiting the number of potential candidates for hardest for- mulas, and an efficient SAT encoding for computing a shortest resolution proof of a given candidate formula.

Finding the Hardest Formulas for Resolution (Extended Abstract)

A CNF formula is harder than another CNF formula with the same number of clauses if it requires a longer resolution proof. We introduce resolution hardness numbers; they give for m=1,2,... the length of a shortest proof of a hardest formula on m clauses. We compute the first ten resolution hardness numbers, along with the corresponding hardest formulas. To achieve this, we devise a candidate filtering and symmetry breaking search scheme for limiting the number of potential candidates for hardest formulas, and an efficient SAT encoding for computing a shortest resolution proof of a given candidate formula.

Chapter 10. Random Satisfiabiliy

In the last twenty years a significant amount of effort has been devoted to the study of randomly generated satisfiability instances. While a number of generative models have been proposed, uniformly random k-CNF formulas are by now the dominant and most studied model. One reason for this is that such formulas enjoy a number of intriguing mathematical properties, including the following: for each k≥3, there is a critical value, rk, of the clauses-to-variables ratio, r, such that for r<rk a random k-CNF formula is satisfiable with probability that tends to 1 as n→∞, while for r>rk it is unsatisfiable with probability that tends to 1 as n→∞. Algorithmically, even at densities much below rk, no polynomial-time algorithm is known that can find any solution even with constant probability, while for all densities greater than rk, the length of every resolution proof of unsatisfiability is exponential (and, thus, so is the running time of every DPLL-type algorithm). By now, the study of random k-CNF formulas has also attracted attention in areas such as mathematics and statistical physics and is at the center of an area of intense research activity. At the same time, random k-SAT instances are a popular benchmark for testing and tuning satisfiability algorithms. Indeed, some of the better practical ideas in use today come from insights gained by studying the performance of algorithms on them. We review old and recent mathematical results about random k-CNF formulas, demonstrating that the connection between computational complexity and phase transitions is both deep and highly nuanced.

Simulating Strong Practical Proof Systems with Extended Resolution

Proof systems for propositional logic provide the basis for decision procedures that determine the satisfiability status of logical formulas. While the well-known proof system of extended resolution—introduced by Tseitin in the sixties—allows for the compact representation of proofs, modern SAT solvers (i.e., tools for deciding propositional logic) are based on different proof systems that capture practical solving techniques in an elegant way. The most popular of these proof systems is likely DRAT, which is considered the de-facto standard in SAT solving. Moreover, just recently, the proof system DPR has been proposed as a generalization of DRAT that allows for short proofs without the need of new variables. Since every extended-resolution proof can be regarded as a DRAT proof and since every DRAT proof is also a DPR proof, it was clear that both DRAT and DPR generalize extended resolution. In this paper, we show that—from the viewpoint of proof complexity—these two systems are no stronger than extended resolution. We do so by showing that (1) extended resolution polynomially simulates DRAT and (2) DRAT polynomially simulates DPR. We implemented our simulations as proof-transformation tools and evaluated them to observe their behavior in practice. Finally, as a side note, we show how Kullmann’s proof system based on blocked clauses (another generalization of extended resolution) is related to the other systems.

Augmenting the Power of (Partial) MaxSat Resolution with Extension

The refutation power of SAT and MaxSAT resolution is challenged by problems like the soft and hard Pigeon Hole Problem PHP for which short refutations do not exist. In this paper we augment the MaxSAT resolution proof system with an extension rule. The new proof system MaxResE is sound and complete, and more powerful than plain MaxSAT resolution, since it can refute the soft and hard PHP in polynomial time. We show that MaxResE refutations actually subtract lower bounds from the objective function encoded by the formulas. The resulting formula is the residual after the lower bound extraction. We experimentally show that the residual of the soft PHP (once its necessary cost of 1 has been efficiently subtracted with MaxResE) is a concise, easy to solve, satisfiable problem.

Hard Examples for Common Variable Decision Heuristics

The CDCL algorithm for SAT is equivalent to the resolution proof system under a few assumptions, one of them being an optimal non-deterministic procedure for choosing the next variable to branch on. In practice this task is left to a variable decision heuristic, and since the so-called VSIDS decision heuristic is considered an integral part of CDCL, whether CDCL with a VSIDS-like heuristic is also equivalent to resolution remained a significant open question.We give a negative answer by building a family of formulas that have resolution proofs of polynomial size but require exponential time to decide in CDCL with common heuristics such as VMTF, CHB, and certain implementations of VSIDS and LRB.

Seeking Practical CDCL Insights from Theoretical SAT Benchmarks

Over the last decades Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) have developed to the point where they can handle formulas with millions of variables. Yet a deeper understanding of how these solvers can be so successful has remained elusive. In this work we shed light on CDCL performance by using theoretical benchmarks, which have the attractive features of being a) scalable, b) extremal with respect to different proof search parameters, and c) theoretically easy in the sense of having short proofs in the resolution proof system underlying CDCL. This allows for a systematic study of solver heuristics and how efficiently they search for proofs. We report results from extensive experiments on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raise a number of intriguing questions for further study.