Hard industrial planning, timetabling or scheduling instances for SAT typically have many high-level constraints, each expressed by a possibly large number of clauses. When a given instance is reported unsatisfiable by the SAT solver, the user normally needs an explanation why: a (hopefully small) subset of the constraints causing it. Our industrial applications require fast explanations, preferably faster than the original SAT run. For this, we leverage the original solver’s work through its unsatisfiability proof. Here we introduce WhyUnsat, and explain why it is fast and robust. In WhyUnsat one can always plug in the best current SAT solver and proof trimmer, without any modification, by simply indicating the path to their executables. WhyUnsat is also fast because it exploits, via MPI, the -progressively cheaper- shared-memory and distributed computing resources. Another requirement we had is that the tool should be anytime and user-friendly; indeed, it quickly shows a human-readable presentation of (an over-approximation of) the explanation, which is then progressively reduced until minimality (unless interrupted by the user). Finally, and not less importantly, here we explain how and why the WhyUnsat approach is now also directly applicable, at no implementation cost, to IPASIR-UP-based constraint programming by Lazy Clause Generation (LCG) as well as to SAT Modulo Theories (SMT).

Among all procedures that CDCL-based SAT solvers implement, unit propagation dominates the total running time. Hence, it is not a surprise that large research efforts have been invested on improving it. As a result, the two-watched-literal scheme, enhanced with implementation details boosting its performance, emerged as the dominant method. The importance of unit propagation in pseudo-Boolean solvers is similar. However, no dominant method exists: counter and watch-based propagation are well-suited for different types of constraints, opening the door to hybrid methods. The higher complexity of implementing pseudo-Boolean solvers has shifted the research focus to higher-level aspects of other procedures, considering implementation details of unit propagation not a priority. In this paper, we first present execution logs: a novel methodology that allows us to precisely evaluate the performance of different propagation procedures. Secondly, we show how both counter and watch-based propagation routines in the RoundingSat solver can be largely improved thanks to a careful analysis of various implementation issues. Thirdly, a detailed analysis shows that hybrid methods outperform the ones based on a single technique. Finally, our experiments reveal that improvements in propagation lead to a clearly better overall performance of the solver.

We shed new light on the Literal Block Distance (LBD) and glue-based heuristics used in current SAT solvers. For this, we first introduce the concept of stickiness: given a run of a CDCL SAT solver, for each pair of literals we define, by a real value between 0 and 1, how sticky they are, basically, how frequently they are set at the same decision level. By means of a careful and detailed experimental setup and analysis, we confirm the following quite surprising fact: given a SAT instance, when running different CDCL SAT solvers on it, no matter their settings or random seeds, the stickiness relation between literals is always very similar, in a precisely defined sense. We analyze how quickly stickiness stabilizes in a run (quite quickly), and show that it is stable even under different encodings of cardinality constraints. We then describe how and why these solid new insights lead to heuristics refinements for SAT (and extensions, such as SMT) and improved information sharing in parallel solvers.

Pseudo-Boolean constraints are omnipresent in practical applications, and thus a significant effort has been devoted to the development of good SAT encoding techniques for them. Some of these encodings first construct a Binary Decision Diagram (BDD) for the constraint, and then encode the BDD into a propositional formula. These BDD-based approaches have some important advantages, such as not being dependent on the size of the coefficients, or being able to share the same BDD for representing many constraints. We first focus on the size of the resulting BDDs, which was considered to be an open problem in our research community. We report on previous work where it was proved that there are Pseudo-Boolean constraints for which no polynomial BDD exists. We also give an alternative and simpler proof assuming that NP is different from Co-NP. More interestingly, here we also show how to overcome the possible exponential blowup of BDDs by \emph{coefficient decomposition}. This allows us to give the first polynomial generalized arc-consistent ROBDD-based encoding for Pseudo-Boolean constraints. Finally, we focus on practical issues: we show how to efficiently construct such ROBDDs, how to encode them into SAT with only 2 clauses per node, and present experimental results that confirm that our approach is competitive with other encodings and state-of-the-art Pseudo-Boolean solvers.

The extensional theory of arrays is one of the most important ones for applications of SAT modulo theories (SMT) to hardware and software verification. Here we present a new T-solver for arrays in the context of the DPLL(T) approach to SMT. The main characteristics of our solver are: (i) no translation of writes into reads is needed, (ii) there is no axiom instantiation, and (iii) the T-solver interacts with the Boolean engine by asking to split on equality literals between indices. Unlike most state-of-the-art array solvers, it is not based on a lazy instantiation of the array axioms. This novelty might make it more convenient to apply this solver in some particular environments. Moreover, it is very competitive in practice, specially on problems that require heavy reasoning on array literals.

We first introduce Abstract DPLL , a rule-based formulation of the Davis--Putnam--Logemann--Loveland (DPLL) procedure for propositional satisfiability. This abstract framework allows one to cleanly express practical DPLL algorithms and to formally reason about them in a simple way. Its properties, such as soundness, completeness or termination, immediately carry over to the modern DPLL implementations with features such as backjumping or clause learning.We then extend the framework to Satisfiability Modulo background Theories (SMT) and use it to model several variants of the so-called lazy approach for SMT. In particular, we use it to introduce a few variants of a new, efficient and modular approach for SMT based on a general DPLL( X ) engine, whose parameter X can be instantiated with a specialized solver Solver T for a given theory T , thus producing a DPLL( T ) system. We describe the high-level design of DPLL( X ) and its cooperation with Solver T , discuss the role of theory propagation , and describe different DPLL( T ) strategies for some theories arising in industrial applications.Our extensive experimental evidence, summarized in this article, shows that DPLL( T ) systems can significantly outperform the other state-of-the-art tools, frequently even in orders of magnitude, and have better scaling properties.

The confluence property of ground (i.e., variable-free) term rewrite systems (TRS) is well known to be decidable. This was proved independently in Dauchet et al. [1987, 1990] and in Oyamaguchi [1987] using tree automata techniques and ground tree transducer techniques (originated from this problem), yielding EXPTIME decision procedures (PSPACE for strings). Since then, and until last year, the optimality of this bound had been a well-known longstanding open question (see, e.g., RTA-LOOP [2001]).In Comon et al. [2001], we gave the first polynomial-time algorithm for deciding the confluence of ground TRS. Later in Tiwari [2002] this result was extended, using abstract congruent closure techniques, to linear shallow TRS, that is, TRS where no variable occurs twice in the same rule nor at depth greater than one. Here, we give a new and much simpler proof of the latter result.

replace me

The confluence property of ground (i.e., variable-free) term rewrite systems (GTRS) is well-known to be decidable. This was proved independently by M. Dauchet et al. (1987; 1990) and by M. Oyamaguchi (1987) using tree automata techniques and ground tree transducer techniques (originated from this problem), yielding EXPTIME decision procedures (PSPACE for strings). Since then, it has been a well-known longstanding open question whether this bound is optimal. The authors give a polynomial-time algorithm for deciding the confluence of GTRS, and hence alsofor the particular case of suffix- and prefix string rewrite systems or Thue systems. We show that this bound is optimal for all these problems by proving PTIME-hardness for the string case. This result may have some impact on other areas of formal language theory, and in particular on the theory of tree automata.

It is crucial for the performance of ordered resolution or paramodulation-based deduction systems that they incorporate specialized techniques to work efficiently with standard algebraic theories E. Essential ingredients for this purpose are term orderings that are E-compatible, for the given E, and algorithms deciding constraint satisfiability for such orderings. In this paper, we introduce a uniform technique providing the first such algorithms for some orderings for Abelian semigroups, Abelian monoids and Abelian groups, which we believe will lead to reasonably efficient techniques for practice. The algorithms are optimal since we show that, for any well-founded E-compatible ordering for these E, the constraint satisfiability problem is NP-hard, even for conjunctions of inequations, and that our algorithms are in NP.

A new technique is presented for superposition with first order clauses with built-in abelian groups (AG). Compared with previous approaches, it is simpler, and no inferences with the AG axioms or abstraction rules are needed. Furthermore, AG-unification is used instead of the computationally more expensive unification modulo associativity and commutativity. Due to the simplicity and restrictiveness of our inference system, its compatibility with redundancy notions and constraints, and the fact that standard term orderings like RPO can be used, we believe that our technique will become the method of choice for practice, as well as a basis for new theoretical developments like logic-based complexity and decidability analysis.

All current completeness results for ordered paramodulation require the term ordering > to be well-founded, monotonic and total(izable) on ground terms. Here we introduce a new proof technique where the only properties required for > are well foundedness and the subterm property: The technique is a relatively simple and elegant application of some fundamental results on the termination and confluence of ground term rewrite systems (TRS). By a careful further analysis of our technique, we obtain the first Knuth-Bendix completion procedure that finds a convergent TRS for a given set of equations E and a (possibly non-totalizable) reduction ordering p whenever it exists. Note that being a reduction ordering is the minimal possible requirement on >, since a TRS terminates if, and only if, it is contained in a reduction ordering.

A term rewrite system (TRS) terminates if its rules are contained in a reduction ordering >. In order to deal with any set of equations, including inherently non-terminating ones (like commutativity), TRS have been generalised to ordered TRS (E, >), where equations of E are applied in whatever direction agrees with >. The confluence of terminating TRS is well-known to be decidable, but for ordered TRS the decidability of confluence has been open. Here we show that the confluence of ordered TRS is decidable if ordering constraints for > can be solved in an adequate way, which holds in particular for the class of LPO orderings. For sets E of constrained equations, confluence is shown to be undecidable. Finally, ground reducibility is proved undecidable for ordered TRS.

We prove that for sets of Horn clauses saturated under basic paramodulation, the word and unifiability problems are in NP, and the number of minimal unifiers is simply exponential (i). For Horn sets saturated wrt. a special ordering under the more restrictive inference rule of basic superposition, the word and unifiability problems are still decidable and unification is finitary (ii). We define standard theories, which include and significantly extend shallow theories. Standard presentations can be finitely closed under superposition and result (ii) applies. Generalizing shallow theories to the Horn case, we obtain (two versions of) a language we call Catalog, a natural extension of Datalog to include functions and equality. The closure under paramodulation is finite for Catalog sets, hence (i) applies. Since for shallow sets this closure is even polynomial, shallow unifiability is in NP, which is optimal: unifiability in ground theories is already NP-hard. We even go beyond: the shallow word problem is tractable and for Catalog sets S we prove decidability of the full first-order theory of T(F)/=/sub s/.

We design combination techniques for symbolic constraint solving in the presence of associative and commutative (AC) function symbols. This yields an algorithm for solving AC-RPO constraints (where AC-RPO is the AC-compatible total reduction ordering of Rubio and Nieuwenhuis, 1994), which was a missing ingredient for automated deduction strategies with AC-constraint inheritance. As in the AC-unification case, for this purpose we first study the pure case, i.e. we show how to solve AC-ordering constraints built over a single AC function symbol and variables. Since AC-RPO is an interpretation-based ordering, our algorithm also requires the combination of algorithms for solving interpreted constraints and non-interpreted constraints.