SAT on Saturday, August 12th

FLoC Opening and Plenary Session (08:45‑10:00)
Chair: Moshe Vardi, Thomas Ball, Wolfram Schulte, Rajeev Alur
Location: Grand Ballroom C

08:45‑09:00

Introduction and Welcome

09:00‑10:00

Randal E. Bryant (Carnegie Mellon University) Formal Verification of Infinite State Systems using Boolean Methods [ppt] Most successful automated formal verification tools are based on a bit-level model of computation. Using powerful inference engines, such as Binary Decision Diagrams (BDDs) and Boolean satisfiability (SAT) checkers, symbolic model checkers and similar tools can analyze all possible behaviors of very large, finite-state systems. For many hardware and software systems, we would like to go beyond bit-level models to handle systems that are truly infinite state, or that are better modeled as infinite-state systems. Examples include programs manipulating integer data, concurrency protocols involving arbitrary numbers of processes, and systems containing buffers where the sizes are described parametrically. Historically, much of the effort in verifying such systems involved automated theorem provers, requiring considerable guidance and expertise on the part of the user. We would like to devise approaches for these more powerful computational models that retain the desirable features of model checking, such as the high degree of automation and the ability to generate counterexamples. We have developed UCLID, a prototype verifier for infinite-state systems. The UCLID modeling language extends that of SMV, a bit-level model checker, to include integer and function state variables, addition by constants, and relational operations. The underlying logic is quite expressive, yet it still permits a decision procedure that transforms the formula into propositional logic and then uses a SAT solver. UCLID supports multiple forms of verification, requiring different levels of sophistication in the handling of quantifiers. We demonstrate UCLID's modeling and verification capabilities with such examples as out-of-order microprocessors and directory-based cache coherency protocols.

Break (10:00‑10:30)

Session 1: Proofs and Cores (10:30‑12:30)
Chair: Sharad Malik
Location: Grand Ballroom D

10:30‑11:00	Arist Kojevnikov (St.Petersburg Department of Steklov Institute of Mathematics) Alexander S. Kulikov (St.Petersburg Department of Steklov Institute of Mathematics) Complexity of Semialgebraic Proofs with Restricted Degree of Falsity A weakened version of the Cutting Plane (CP) proof system with a restriction on the degree of falsity of intermediate inequalities was introduced by Goerdt. He proved an exponential lower bound for CP proofs with degree of falsity bounded by n/(log2 n+1) , where n is the number of variables. Hirsch and Nikolenko strengthened this result by establishing a direct connection between CP and Resolution proofs. This result implies an exponential lower bound on the proof length of the Tseitin-Urquhart tautologies, when the degree of falsity is bounded by cn for some constant c. In this paper we generalize this result for extensions of Lovasz-Schrijver calculi (LS), namely for LS^k+CP^k proof systems introduced by Grigoriev et al. We show that any LS^k+CP^k proof with bounded degree of falsity can be transformed into a Res(k) proof. This implies exponential lower bounds for LS^k+CP^k with the degree of falsity bounded by cn for some constant c.
11:00‑11:30	Oliver Kullmann (University of Wales Swansea) Ines Lynce (IST/INESC-ID, Technical University of Lisbon) Joao Marques-Silva (University of Southampton) Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel Finding out that a SAT problem instance F is unsatisfiable is not enough for applications, where "good reasons" are needed for explaining the inconsistency (so that for example the inconsistency may be repaired). Previous attempts of finding such "good reasons" focused on finding some minimally unsatisfiable sub-clause-set F' of F, which in general suffers from the non-uniqueness of F' (and thus it will only find "some reason", albeit there might be others). In our work, we develop a fuller approach, enabling a more fine-grained analysis of necessity and redundancy of clauses, supported by meaningful semantical and proof-theoretical characterisations. We combine known techniques for searching and enumerating minimally unsatisfiable sub-clause-sets with (full) autarky search. To illustrate our techniques, we give a detailed analysis of well-known industrial problem instances.
11:30‑11:45	Alexander Nadel (Tel-Aviv University & Intel Corporation) Nachum Dershowitz (Tel-Aviv University) Ziyad Hanna (Intel Corporation) A Scalable Algorithm for Minimal Unsatisfiable Core Extraction The task of extracting an unsatisfiable core for a given Boolean formula has been finding more and more applications in recent years. The only existing approach that scales well for large real-world formulas exploits the ability of modern SAT solvers to produce resolution refutations. However, the resulting unsatisfiable cores are suboptimal. We propose a new algorithm for minimal unsatisfiable core extraction, based on a deeper exploration of resolution-refutation properties. Experimental results, confirming that the algorithm is able to find minimal unsatisfiable cores for well-known formal verification benchmarks, are provided.
11:45‑12:00	Joshua Buresh-Oppenheim (Simon Fraser University) David Mitchell (Simon Fraser University) Minimum Witnesses for Unsatisfiable 2CNFs We consider the problem of finding the smallest proof of unsatisfiability of a 2CNF formula. In particular, we look at Resolution refutations and at minimum unsatisfiable subsets of the clauses of the CNF. We give a characterization of minimum tree-like Resolution refutations that explains why, to find them, it is not sufficient to find shortest paths in the implication graph of the CNF. The characterization allows us to develop an efficient algorithm for finding a smallest tree-like refutation and to show that the size of such a refutation is a good approximation to the size of the smallest general refutation. We also give a polynomial time dynamic programming algorithm for finding a smallest unsatisfiable subset of the clauses of a 2CNF.
12:00‑12:15	Allen Van Gelder (University of California, Santa Cruz) Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs Input Cover Number (denoted by kappa) is introduced as a metric for difficulty of propositional resolution derivations. If F = {Ci} is the input CNF formula, and clauses are regarded as sets of literals, then the input cover number of a clause D based on F, denoted by kappa(D, F), is defined as the minimum number of clauses Ci needed to form a superset of (i.e., cover) D. The kappa for a derivation is the maximum kappa of any clause in the derivation. Input Cover Number provides a refinement of the clause-width metric analyzed by Ben-Sasson and Wigderson in the sense that it applies to families of formulas whose clause width grows with formula size, such as pigeon-hole formulas and the family GT(n) introduced by Krishnamurthy. Ben-Sasson and Wigderson showed that if formula F has the property that every resolution refutation of F contains a clause of width W, then certain lower bounds can be expressed in terms of (W - width(F)) for the shortest tree-like refutation and for the shortest refutation. It is shown here that both bounds apply with (W - width(F)) replaced by kappa. For families of formulas whose clause width is bounded by a constant, the two metrics provide essentially the same bounds. Evidence is presented that kappa may be a sharper metric than clause width for distinguishing polynomial families from super-polynomial families. Ben-Sasson and Wigderson showed that pigeon-hole formulas PHP(n, n+1) formulas require clause-width to be Omega(n), and it is well known that pigeon-hole formulas require refutation length to be exponential in n. Bonet and Galesi showed that GT(n) formulas also require clause-width to be Omega(n), although the GT(n) family has polynomial-length refutations. It is shown here that kappa is Omega(n) for pigeon-hole formulas and is O(1) for GT(n) formulas and variants of GT(n).
12:15‑12:30	Toni Jussila (Johannes Kepler University) Carsten Sinz (Johannes Kepler University, Linz) Armin Biere (Johannes Kepler University) Extended Resolution Proofs for Symbolic SAT Solving with Quantification Symbolic SAT solving is an approach where the clauses of a CNF formula are represented using BDDs. These BDDs are then conjoined, and finally checking satisfiability is reduced to the question of whether the final BDD is identical to false. We present a method combining symbolic SAT solving with BDD quantification (variable elimination) and generation of extended resolution proofs. Proofs are fundamental to many applications, and our results allow the use of BDDs instead of—or in combination with—established proof generation techniques like clause learning. We have implemented a symbolic SAT solver with variable elimination that produces extended resolution proofs. We present details of our implementation, called EBDDRES, which is an extension of the system presented in [1], and also report on experimental results.

Lunch break (12:30‑14:00)

Session 2: Heuristics and Algorithms (14:00‑15:30)
Chair: Inęs Lynce
Location: Grand Ballroom D

14:00‑14:30	Mark Chavira (University of California, Los Angeles) Adnan Darwiche (University of California, Los Angeles) Pre-Processing CNFs to Enhance Component Analysis Recent algorithms for logical inference work by decomposing a CNF into syntactically independent components and solving the components recursively. When components cannot be identified, the algorithms resort to variable splitting, which can lead to inefficiencies. In this paper, we observe that syntactic component analysis can miss great opportunities because the syntax may hide existing semantic independence. We show that by applying a limited resolution strategy to the CNF prior to inference, one can transform the CNF to syntactically reveal such semantic independence. We describe a general strategy for this purpose, and a more structured strategy that utilizes problem-specific structure. We apply the idea of structured resolution to an application that reduces probabilistic inference to logical inference on a CNF. Experimental results demonstrate that structured resolution can have a large effect on the efficiency of inference, reducing time and space requirements significantly, and allowing inference to be performed on many CNFs that exhausted resources previously.
14:30‑15:00	Himanshu Jain (Carnegie Mellon University) Constantinos Bartzis (Carnegie Mellon University) Edmund Clarke (Carnegie Mellon University, Pittsburgh PA 15213) Satisfiability Checking of Non-clausal Formulas using General Matings Most state-of-the-art SAT solvers are based on DPLL search and require the input formula to be in clausal form (CNF). However, typical formulae that arise in practice are non-clausal. We present a new non-clausal SAT-solver based on General Matings instead of DPLL search. Our technique is able to handle non-clausal formulae involving AND, OR, NOT operators without destroying their structure or introducing new variables. We present techniques for performing search space pruning, learning, non-chronological backtracking in the context of a General Matings based SAT solver. Experimental results show that our SAT solver is competitive to current state-of-the-art SAT solvers on a class of non-clausal benchmarks.
15:00‑15:15	Eugene Goldberg (Cadence Berkeley Labs) Determinization of resolution by an algorithm operating on complete assignments Determinization of resolution is usually done by a DPLL-like procedure that operates on partial assignments. We introduce a resolution-based SAT-solver operating on complete assignments and give a theoretical justification for determinizing resolution this way. In particular, we show that to prove that a CNF formula F is unsatisfiable it is sufficient to check that F=0 at a set of points called a point image of a resolution proof. We give experimental results confirming the viability of our approach to resolution determinization.
15:15‑15:30	Hantao Zhang (University of Iowa) A Complete Random Jump Strategy with Guiding Paths The restart strategy, proposed by Gomes, Selman, and Kautz, is a popular technique for backtrack search algorithms to solve hard satisfiable problems. Most modern SAT solvers implement the restart strategy as one of the options. In 2002, we proposed the so-called random jump strategy, which outperformed the restart strategy, for most experiments. One weakness shared by both the restart strategy and the random jump strategy is the incompleteness: A job which can be finished by a SAT solver in one day might not be finished in one or two days if either strategy is used by the same SAT solver. For the restart strategy, the cause of the incompleteness is due to the fact that repeated search paths are not avoidable. For the random jump strategy, the cause is due to the fact that estimation of unfinished search space is not accurate. In this paper, we propose a simple and effective technique which makes the random jump strategy complete. The technique works as follows: When we jump from the current position to another position, we remember the skipped search space in a simple data structure called ``guiding path''. If we have no more search space left in the current run before running out of the allotted time, we may load one of the saved guiding paths and start another run of the search. The search ends when either a model is found or when no time left or when no more guiding paths left. Because the overhead of saving and loading guiding paths is very small, the completeness of SAT solvers is preserved when using this kind of the random jump strategy. When intelligent backjumping is used with the random jump strategy, a special clause is created to prevent the search to visit the skipped space. The power of the new strategy is demonstrated by solving both satisfiable and unsatisfiable previously open quasigroup problems. This technique can be used for any combinatorial backtrack search procedures.

Break (15:30‑16:00)

Session 3: Applications (16:00‑17:30)
Chair: Miroslav Velev
Location: Grand Ballroom D

16:00‑16:30	Ilya Mironov (Microsoft Research) Lintao Zhang (Microsoft Research) Applications of SAT-Solvers to Cryptanalysis Several novel attacks on standard cryptographic hash functions appeared in 2005. Some aspects of these attacks lend themselves well to an encoding as CNF formulas, which are within reach of modern SAT solvers. In this paper we demonstrate effectiveness of this approach, which is a first, to the best of our knowledge, truly practical application of SAT solvers to cryptanalysis. We expect the SAT solvers to find new applications as a validation and testing tool of cryptanalysts.
16:30‑17:00	Yuliya Zabiyaka (University of California, Los Angeles) Adnan Darwiche (University of California, Los Angeles) Functional Treewidth: Bounding Complexity in the Presence of Functional Dependencies Many reasoning problems in logic and constraint satisfaction have been shown to be exponential only in the treewidth of their interaction graph: a graph which captures the structural interactions among variables in a problem. It has long been observed in both logic and constraint satisfaction, however, that problems may be easy even when their treewidth is high. To bridge some of the gap between theoretical bounds and actual runtime, we propose a complexity parameter, called functional treewidth, which refines treewidth by being sensitive to non--structural aspects of a problem: functional dependencies in particular. This measure dominates treewidth and can be used to both bound the complexity of certain algorithms and to improve the complexity of others. We illustrate the new measure in the context of compiling CNFs into a tractable form known as d-DNNF, and discuss how it applies to other types of reasoning problems, including model counting. We present empirical results which show how the new measure can predict the complexity of certain benchmarks, that would have been considered quite difficult based on treewidth alone.
17:00‑17:15	Roberto Sebastiani (DIT, University of Trento) Michele Vescovi (DIT, University of Trento) Encoding the satisfiability of modal and description logics into SAT: the case study of K(m)/ALC In the last two decades, modal and description logics have been applied to numerous areas of computer science, including artificial intelligence, formal verification, database theory, and distributed computing. For this reason, the problem of automated reasoning in modal and description logics has been throughly investigated. In particular, many approaches have been proposed for efficiently handling the satisfiability of the core normal modal logic K(m), and of its notational variant, the description logic ALC. Although simple in structure, K(m)/ALC is computationally very hard to reason on, its satisfiability being PSPACE-complete. In this paper we explore the idea of encoding K(m)/ALC-satisfiability into SAT, so that to be handled by state-of-the-art SAT tools. We propose an efficient encoding, and we test it on an extensive set of benchmarks, comparing the approach with the main state-of-the-art tools available. Although the encoding is necessarily worst-case exponential, from our experiments we notice that, in practice, this approach can handle most or all the problems which are at the reach of the other approaches, with performances which are comparable with, or even better than, those of the current state-of-the-art tools.
17:15‑17:30	Ines Lynce (IST/INESC-ID, Technical University of Lisbon) Joao Marques-Silva (University of Southampton) SAT in Bioinformatics: Making the Case with Haplotype Inference Mutation in DNA is the principal cause for differences among human beings, and Single Nucleotide Polymorphisms (SNPs) are the most common mutations. Hence, a fundamental task is to complete a map of haplotypes (which identify SNPs) in the human population. Associated with this effort, a key computational problem is the inference of haplotype data from genotype data, since in practice genotype data rather than haplotype data is usually obtained. Different haplotype inference approaches have been proposed, two of which are the most promising in terms of accuracy: the utilization of statistical methods and the utilization of the pure parsimony criterion. Recent work has shown that a SAT-based approach is by far the most efficient approach for the problem of haplotype inference by pure parsimony (HIPP), being several orders of magnitude faster than existing integer linear programming and branch and bound solutions. This paper reviews the original SAT-based model for the HIPP problem and proposes a number of key optimizations. The results are again significant. Compared to the original SAT-based HIPP model, the new version can be orders of magnitude faster, particularly on biological test data. The results are even more significant since the new version of the model makes SAT-based HIPP competitive, in terms of accuracy and efficiency, with the most effective statistical methods.

SAT Business Meeting (18:00‑20:00)
Location: Richmond (4th floor)