SAT on Monday, July 12th

09:00‑10:00 SAT Invited Talk
Location: AT LT2
09:00 Ramamohan Paturi.
Exact Algorithms and Complexity

Over the past couple of decades, a series of exact exponential-time algorithms have been developed with improved run times for a number of problems including IndependentSet, k-SAT, and k-colorability using a variety of algorithmic techniques such as backtracking, dynamic programming, and inclusion-exclusion. The series of improvements are typically in the form of better exponents compared to exhaustive search. These improvements prompt several questions, chiefamong them is whether we can expect continued improvements in the exponent. Is there a limit beyond which one should not expect improvement? If we assume NP != P or other appropriate complexity statement, what can we say about the likely exact complexities of various NP-complete problems? Besides the improvement in exponents, there are two other general aspects to the algorithmic developments. Problems seem to differ considerably in terms of the improvements in the exponents. Secondly, different algorithmic paradigms seem to work best for different problems. These aspects are particularly interesting given the well-known fact that all NP-complete problems are equivalent as far as polynomial-time solvability is concerned. How do the best possible exponents differ for different problems? Can we explain the difference in terms of the structural properties of the problems? Are the likely complexities of various problems related? What is relative power of various algorithmic paradigms? One approach would be to consider natural, though restricted, computational models. For example, consider the class OPP of one-sided error probabilistic polynomial-time algorithms. OPP captures a common design paradigm for randomized exact exponential-time algorithms: to repeat sufficiently many times a one-sided error probabilistic polynomial-time algorithm that is correct with an exponentially small probability so that the overall algorithm finds a witness with constant probability. This class includes Davis-Putnam-style backtracking algorithms developed in recent times to provide improved exponential-time upper bounds for a variety of NP-hard problems. While the original versions of some of these algorithms are couched as exponential-time algorithms, one can observe from a formalization due to Eppstein that these algorithms can be converted into probabilistic polynomial-time algorithms whose success probability is the reciprocal of the best exponential-time bound. The class is interesting not just because of ubiquity, but because such algorithms are ideal from the point of view of space efficiency, parallelization, and speed-up by quantum computation. What are the limitations of such algorithms for deciding NP-complete problems? Could the best algorithm for specific NP-complete problems be in this class?

On the other hand, the recent algorithms for k-colorability for k >= 3 use inclusion-exclusion principle in combination with dynamic programming to achieve the bound of $2^n$. This raises a natural question whether we can expect an OPP algorithm for k-colorability whose success probability is at least $2^{-n}$. More generally, can we expect OPP-style optimal algorithms for k-colorability? Does there exist any OPP algorithm for k-colorability whose success probability is at least $c^{-n}$ where c is independent of k? Negative answers (or evidence to that effect) for these questions would provide convincing proof (or evidence) that exponential-time inclusion-exclusion and dynamic programming paradigms are strictly more powerful than that of OPP. On the other hand, algorithmic results that would place k-colorability in the class OPP with $c^{-n}$ success probability would be exciting.

The current state of the art in complexity theory is far from being able to resolve these questions, especially the question of best exponents, even under reasonable complexity assumptions. However, recent algorithmic and complexity results are interesting and they provide food for thought. In this talk, I will present key algorithmic results as well as our current understanding of the limitations.

10:30‑12:30 Theory + Combinatorics
Location: AT LT2
10:30 Evgeny Dantsin and Alexander Wolpert
On Moderately Exponential Time for SAT

Can SAT be solved in ``moderately exponential'' time, i.e., in time $O(2^{cn})$ where $c<1$ is a constant and $n$ is the number of variables in the input CNF formula? This challenging question is far from being resolved. We have an answer only for some restrictions of SAT: for example, there are moderately exponential time algorithms for $k$-SAT and for the restriction of SAT to formulas of constant clause density. In this paper, we consider another restriction: SAT$^{(d)}$ is the restriction of SAT to formulas with at most $n^d$ clauses. We show that the complexity of SAT$^{(d)}$ is in between the complexity of $k$-SAT and the complexity of unrestricted SAT. It follows that, assuming the Exponential Time Hypothesis \cite{IP01}, the complexity of SAT$^{(d)}$ for any $d>1$ is strictly higher than the complexity of $k$-SAT. Can SAT$^{(d)}$ be solved in moderately exponential time? We reduce this question to a question about the complexity of a fragment of existential second-order logic. This fragment is an extension of the complexity class SNP (Strict NP) consisting of problems defined by existential second-order sentences where the first-order part has a universal prefix. Impagliazzo, Paturi, and Zane \cite{IPZ01} proved that any problem in SNP can be solved in moderately exponential time. We extend SNP by allowing a $\forall \ldots \forall \, \exists \ldots \exists$ prefix in the first-order part, and we prove that SAT$^{(d)}$ can be solved in moderately exponential time for any $d$ if and only if each problem in this extension can also be solved in moderately exponential time.

11:00 Eli Ben-Sasson and Jan Johannsen
Lower bounds for width-restricted clause learning on small width formulas

It has been observed empirically that clause learning does not significantly improve the performance of a SAT solver when restricted to learning clauses of small width only. This experience is supported by lower bound theorems. It is shown that lower bounds on the runtime of width-restricted clause learning follow from resolution width lower bounds. This yields the first lower bounds on width-restricted clause learning for formulas in 3-CNF.

11:30 Scott Cotton
Some Techniques for Minimizing Resolution Proofs

Some SAT-solvers are equipped with the ability to produce resolution proofs for problems which are unsatisfiable. Such proofs are used in a variety of contexts, including finding minimal unsatisfiable sets of clauses, interpolant generation, configuration management, and proof replay in interactive theorem proovers. More generally, standalone proofs can act as certificates which are to be checked multiple times, as occurs with proof-carrying code. In all of these settings, it can be helpful to produce small proofs. Indeed SAT-solvers generally produce proofs which are full of structural and semantic redundancies and are thus far from minimal. At the same time, the problem of finding a minimum length proof is highly intractable -- in the general case we cannot hope to find or even approximate minimum length proofs. Consequently, we suggest some new heuristic methods for resolution proof minimization. First, we identify a simple and effective method of extracting shared structure from a proof using structural hashing. Second, we suggest $2$ content-based heuristically-guided proof rewriting techniques; one is based on proof valuations and the other makes use of extended resolution. Our findings indicate structural sharing always reduces proof length significantly and efficiently, and our proposed semantic rewriting techniques can give significant reductions, sometimes resulting in proofs a small fraction the size of the original.

11:50 Allen Van Gelder and Ivor Spence
Zero-One Designs Produce Small Hard SAT Instances

Some basics of combinatorial block design are combined with certain constraint satisfaction problems of interest to the satisfiability community. The paper shows how such combinations lead to satisfiability problems, and shows empirically that these are some of the smallest very hard satisfiability problems ever constructed. Partially balanced (0,1) designs (PB01Ds) are introduced as an extension of balanced incomplete block designs (BIBDs) and (0,1) designs. Also, (0,1) difference sets are introduced as an extension of certain cyclical difference sets. Constructions based on (0,1) difference sets enable generation of PB01Ds over a much wider range of parameters than is possible for BIBDs. Building upon previous work of Spence, it is shown how PB01Ds lead to small, very hard, unsatisfiable formulas. A new three-dimensional form of combinatorial block design is introduced, and leads to small, very hard, satisfiable formulas. The methods are validated on solvers that performed well in the SAT 2009 and earlier competitions.

12:10 William Matthews and Ramamohan Paturi
Uniquely Satisfiable k-SAT Instances with Almost Minimal Occurrences of Each Variable

Let (k,s)-SAT refer the family of satisfiability problems restricted to CNF formulas with exactly k distinct literals per clause and at most s occurrences of each variable. Kratochvil, Savicky and Tuza show that there exists a function f(k) such that for all s at most f(k), all (k,s)-SAT instances are satisfiable whereas for k at least 3 and s > f(k), (k,s)-SAT is NP-complete. We define a new function u(k) as the minimum s such that uniquely satisfiable (k,s)-SAT formulas exist. We show that for k at least 3, unique solutions and NP-hardness occur at almost the same value of s: f(k) is at most u(k), and u(k) is at most f(k)+2.

We also give a parsimonious reduction from SAT to (k,s)-SAT for any k at least 3 and s at least f(k)+2. When combined with the Valiant--Vazirani Theorem, this gives a randomized polynomial time reduction from SAT to UNIQUE-(k,s)-SAT.

14:00‑14:50 SAT Usage
Location: AT LT2
14:00 Carsten Fuhs and Peter Schneider-Kamp
Synthesizing Shortest Straight-Line Programs over GF(2) using SAT

Non-trivial linear straight-line programs over the Galois field of two elements occur frequently in applications such as encryption or high-performance computing. Finding the shortest linear straight-line program for a given set of linear forms is known to be MaxSNP-complete, i.e., there is no $\epsilon$-approximation for the problem unless P = NP.

This paper presents an efficient non-approximative approach for finding the shortest linear straight-line program. In other words, we show how to search for a circuit of XOR gates with the minimal number of such gates. The approach is based on a reduction of the associated decision problem (“Is there a program of length k?”) to satisfiability of propositional logic. Using modern SAT solvers, optimal solutions to interesting problem instances can be obtained.

14:30 Oliver Kullmann
Green-Tao Numbers and SAT

Van-der-Waerden numbers vdw_m(k_1,...,k_m) are defined as the smallest n such that whenever {1, ..., n} is partitioned into parts P_1, ..., P_m, then there exists some 1 <= i <= m such that P_i contains an arithmetic progression of length k_i. Van der Waerden's theorem is the assertion that these numbers always exist (are finite). SAT solvers are rather efficient in computing vdW-numbers, with the biggest success yet the computation of vdw_2(6,6) = 1132.

A major development now has taken place in the field of additive number theory, leading to the Green-Tao Theorem which asserts that the vdW-theorem still holds when we consider the first n prime numbers instead of just the first n (natural) numbers (this major breakthrough was decisively involved in the Fields Medal of Terence Tao in 2006). In this paper we introduce the Green-Tao numbers grt_m(k_1, ..., k_m) (defined as above, but now considering the first n prime numbers), and we establish over the whole parameter range the boundaries of what current SAT solving can compute. An interesting outcome here is that the behaviour is very diverse, where many types of complete and incomplete solvers are each best for certain parameter ranges.

A natural question is about the directions in the infinite-dimensional parameter space where the numbers only grow polynomially. For a general framework of Ramsey theory we prove that numbers N(2, ..., 2, k_1, ..., k_m) grow only linearly with growing initial segment of 2's and for arbitrary constant factor > 1, where N for example can be vdw or grt, and where the final tuple (k_1, ..., k_m) is fixed.

Finally, for translating non-boolean clause-sets (arising naturally when m > 2) into boolean clause-sets, we study the generic translation scheme introduced by the author, which covers all known translations, and allows infinitely many variations. In all cases we considered, translations far superior over the standard translation are (empirically) demonstrated.

15:30‑17:20 QBF
Location: AT LT2
15:30 Uwe Bubeck and Hans Kleine Büning
Rewriting (Dependency-)Quantified 2-CNF with Arbitrary Free Literals into Existential 2-HORN

We extend quantified 2-CNF formulas by also allowing literals over free variables which are exempt from the 2-CNF restriction. That means we consider quantified CNF formulas with clauses that each contain at most two bound literals and an arbitrary number of free literals. We show that these Q2-CNF^b formulas can be transformed in polynomial time into purely existentially quantified CNF formulas in which the bound literals are in 2-HORN (E2-HORN^b).

Our result still holds if we allow Henkin-style quantifiers with explicit dependencies. In general, dependency quantified Boolean formulas (DQBF) are assumed to be more succinct at the price of a higher complexity. This paper shows that DQ2-CNF^b has a similar expressive power and complexity as E2-HORN^b. In the special case that the 2-CNF restriction is also applied to the free variables (DQ2-CNF^*), the satisfiability can be decided in linear time.

16:00 Christian Miller, Stefan Kupferschmid, Matthew Lewis and Bernd Becker
Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs

This paper focuses on bounded invariant checking for partially specified circuits -- designs containing so-called blackboxes -- using the well known 01X- and QBF-encoding techniques. For detecting counterexamples, modeling the behavior of a blackbox using 01X-encoding is rather coarse as it limits what problems can be verified. We introduce the idea of 01X-hardness, mainly the classification of problems for which this encoding technique does not provide any useful information about the existence of a counterexample. Furthermore, we provide a proof for 01X-hardness based on Craig interpolation, and show how the information contained within the proof can be used to determine heuristically which blackbox outputs to model in a more precise way. This allows us to compare 01X, QBF and an optimzed hybrid encoding containing both modeling techniques. Finally, our total work flow and multiple state-of-the-art QBF-solvers are shown to perform well on a range of industrial blackbox circuit problems.

16:30 Enrico Giunchiglia, Paolo Marin and Massimo Narizzano
sQueezeBF: An effective preprocessor for QBFs

In this paper we present sQueezeBF, an effective preprocessor for QBFs that combines various techniques for eliminating variables and/or redundant clauses. In particular sQueezeBF combines (i) variable elimination via Q-resolution, (ii) variable elimination via equivalence substitution and (iii) equivalence literals breaking via equivalence rewriting. The experimental analysis shows that sQueezeBF can produce significant reductions in the number of clauses and/or variables - up to the point that some instances are solved directly by sQueezeBF - and that it can significantly improve the efficiency of a range of state-of-the-art QBF solvers - up to the point that some instances cannot be solved without sQueezeBF preprocessing.

17:00 Alexandra Goultiaeva and Fahiem Bacchus
Exploiting Circuit Representations in QBF solving

Circuit representations have been utilized in QBF solvers, and previous work has shown that this form of non-clausal representation can be exploited to obtain useful performance improvements. In this paper we examine some additional techniques for exploiting a circuit representation so as to obtain further performance improvements. We discuss the techniques of propagating a dual set of values through the circuit, conversion from simple negation normal form to a more optimized circuit representation, and adding phase memorization during search. We have implemented these techniques in a new QBF solver called CirQit2 and evaluated their impact experimentally. The solver has also been entered in the QBFEval’10 competition.