SAT on Sunday, August 13th

Invited Talk (09:00‑10:00)
Chair: Armin Biere
Location: Grand Ballroom D

09:00‑10:00

Karem Sakallah (University of Michigan, Ann Arbor) From Propositional Satisfiability To Satisfiability Modulo Theories [ppt] In this talk we present a review of SAT-based approaches for building scalable and efficient decision procedures for quantifier-free first-order logic formulas in one or more decidable theories, known as Satisfiability Modulo Theories (SMT) problems. As applied to different system verification problems, SMT problems comprise of different theories including fragments of elementary theory of numbers, the theory of arrays, the theory of list structures, etc. In this talk we focus on different DPLL-style satisfiability procedures for decidable fragments of the theory of integers. Leveraging the advances made in SAT solvers in the past decade, we introduce several SAT-based SMT solving methods that in many applications have outperformed classical decision methods. Aside from the classical method of translating the SMT formula to a purely Boolean problem, in recent methods, a SAT solver is utilized to serve as the "glue" that ties together the different theory atoms and forms the basis for reasoning and learning within and across them. Several methods have been developed to provide a combination framework for implications to flow through the theory solvers and to possibly activate other theory atoms based on the current assignments. Similarly, conflict-based learning is also extended to enable the creation of learned clauses comprising of the combination of theory atoms. Additional methods unique to one or more types of theory atoms have also been proposed that learn more expressive constraints and significantly increase the pruning power of these combination schemes. We will describe several combination strategies and their impact on scalability and performance of the overall solver in different settings and applications.

Break (10:00‑10:30)

Session 4: SMT (10:30‑12:30)
Chair: Alessandro Cimatti
Location: Grand Ballroom D

10:30‑11:00	Yinlei Yu (Princeton University) Sharad Malik (Princeton University) Lemma Learning in SMT on Linear Constraints The past decade has seen great improvement in Boolean Satisfiability(SAT) solvers. SAT solving is now widely used in different areas, including electronic design automation, software verification and artificial intelligence. However, many applications have non-Boolean constraints, such as with linear relations and uninterpreted functions. Converting such constraints into SAT is very hard and sometimes impossible. This has given rise to a recent surge of interest in Satisfiability Modulo Theories (SMT). SMT combines a Boolean formula and predicates in other theories, such as linear real arithmetic. Solving an SMT problem entails either finding an assignment for all Boolean and theory specific variables in the formula that evaluates the formula to TRUE or proving such assignment does not exist. To solve such an SMT instance, a solver typically combines SAT and theory-specific solving under the Nelson-Oppen procedure framework. Fast SAT and theory-specific solvers and good integration is required for efficient SMT solving. Efficient learning contributes greatly to the success of the recent SAT solvers. However, the learning technique in SMT is limited in the current literature. In this paper, we propose methods of efficient lemma learning on SMT problems with linear real/integer arithmetic constraints. We describe a static learning technique by analyzing the relationship of the linear constraints. Conflict driven learning derived from infeasible set of linear real/integer constraints is also discussed. These methods can be expanded to many other theories. Our experimental results show that incorporation of learning can significantly improve the speed of SMT solvers.
11:00‑11:30	Robert Nieuwenhuis (Tech. University Catalonia) Albert Oliveras (Tech. Univ. Catalonia, Barcelona) On SAT Modulo Theories and Optimization Problems Solvers for SAT Modulo Theories (SMT) can nowadays handle large industrial (e.g., formal hardware and software verification) problems over theories such as the integers, arrays, or equality. Here we show that SMT approaches can also efficiently solve problems that, at first sight, do not have a typical SMT flavor. In particular, here we deal with SAT and SMT problems where models $M$ are sought such that a given cost function f(M) is minimized. For this purpose, we introduce a variant of SMT where the theory T becomes progressively stronger, and prove it correct using the Abstract DPLL Modulo Theories framework. We discuss two different examples of applications of this SMT variant: weighted Max-SAT and weighted Max-SMT. We show how, with relatively little effort, one can obtain a competitive system that, in the case of weighted Max-SMT in the theory of Difference Logic, can even handle well-known hard radio frequency assignment problems without any tailored heuristics. These results seem to indicate that Max-SAT/SMT techniques can already be used for realistic applications.
11:30‑12:00	Scott Cotton (Verimag) Oded Maler (Verimag) Fast and Flexible Difference Constraint Propagation for DPLL(T) In the context of DPLL(T), theory propagation is the process of dynamically selecting consequences of a conjunction of constraints from a given set of candidate constraints. We present improvements to a fast theory propagation procedure for difference constraints of the form x - y <= c. These improvements are demonstrated eperimentally.
12:00‑12:30	Hossein Sheini (University of Michigan) Karem Sakallah (University of Michigan) A Progressive Simplifier for Satisfiability Modulo Theories In this paper we present a new progressive cooperating simplifier for deciding the satisfiability of a quantifier-free formula in the first-order theory of integers involving combinations of sublogics, referred to as Satisfiability Modulo Theories (SMT). Our approach, given an SMT problem, replaces each non-propositional theory atom with a Boolean indicator variable yielding a purely propositional formula to be decided by a SAT solver. Starting with the most abstract representation (the Boolean formula), the solver gradually integrates more complex theory solvers into the working decision procedure. Additionally, we propose a method to simplify "expensive" atoms into suitable conjunctions of "cheaper" theory atoms when conflicts occur. This process considerably increases the efficiency of the overall procedure by reducing the number of calls to the slower theory solvers. This is made possible by adopting our novel inter-logic implication framework, as proposed in this paper. We have implemented these methods in our Ario SMT solver by combining three different theory solvers within a DPLL-style SAT solver: a Unit-Two-Variable-Per-Inequality (UTVPI) solver, an integer linear programming (ILP) solver, and a solver for systems of equalities with uninterpreted functions. The efficiencies of our proposed algorithms are demonstrated and exhaustively investigated on a wide range of benchmarks in hardware and software verification domain. Empirical results are also presented showing the advantages/limitations of our methods over other modern techniques for solving these SMT problems.

Lunch break (12:30‑14:00)

Session 5: Structure (14:00‑15:30)
Chair: Stefan Szeider
Location: Grand Ballroom D

14:00‑14:30	Uwe Bubeck (University of Paderborn) Hans Kleine Büning (University of Paderborn) Dependency Quantified Horn Formulas: Models and Complexity Dependency quantified Boolean formulas (DQBF) extend quantified Boolean formulas with Henkin-style partially ordered quantifiers. It has been shown that this is likely to yield more succinct representations at the price of a computational blow-up from PSPACE to NEXPTIME. In this paper, we consider dependency quantified Horn formulas (DQHORN), a subclass of DQBF, and show that the computational simplicity of quantified Horn formulas is preserved when adding partially ordered quantifiers. We investigate the structure of satisfiability models for DQHORN formulas and prove that for both DQHORN and ordinary QHORN formulas, the behavior of the existential quantifiers depends only on the cases where at most one of the universally quantified variables is zero. This allows us to transform DQHORN formulas with free variables into equivalent QHORN formulas with only a quadratic increase in length. An application of these findings is to determine the satisfiability of a dependency quantified Horn formula Phi with n universal quantifiers in time O(|Phi| * n), which is just as hard as QHORN-SAT.
14:30‑15:00	Stefan Porschen (Institut fuer Informatik, Universitaet Koeln) Ewald Speckenmeyer (Institut fuer Informatik, Universitaet zu Koeln) Bert Randerath (Institut fuer Informatik, Universitaet Koeln) On Linear CNF Formulas In the present paper we introduce the class of {\em linear} CNF formulas generalizing the notion of linear hypergraphs. Clauses of a linear formula intersect in at most one variable. We show that SAT for the general class of linear formulas remains NP-complete. Moreover we show that the subclass of exactly linear formulas is always satisfiable. We further consider the class of uniform linear formulas and investigate conditions for the formula graph to be complete. We define a formula hierarchy such that one can construct a $3$-uniform linear formula belonging to the $i$th such that the clause-variable density is of $\Omega(2.5^{i-1})\cap O(3.2^{i-1})$. Finally, we introduce the subclasses $\LCNF_{\ge k}$ of linear formulas having only clauses of length at least $k$, and show that SAT remains NP-complete for $\LCNF_{\ge 3}$.
15:00‑15:30	Su Chen (Rutgers University) Tomasz Imielinski (Rutgers University) Karin Johnsgard (Monmouth University) Donald Smith (Rutgers University) Mario Szegedy (Rutgers University) A Dichotomy Theorem for Constraint Satisfaction Problems with Disjoint Domains This paper is a contribution to the general investigation into how the complexity of constraint satisfaction problems (CSPs) is determined by the form of the constraints. Schaefer proved that the Boolean generalized CSP has the dichotomy property (i.e., all instances either in P or are NP-complete), and gave a complete and simple classification of those instances which are in P (assuming NP is not P). In this paper we consider a special subcase of the generalized CSP (inspired by polygenetic diseases). For this CSP subcase, we require that the variables be drawn from disjoint Boolean domains. Our relation set contains only two elements: a monotone multiple-arity Boolean relation, and its complement. We prove a dichotomy theorem for these monotone function CSPs, and give a succinct characterization of those monotone functions such that the corresponding problem resides in P.

Break (15:30‑16:00)

Poster Session (16:00‑18:00)
Location: Grand Ballroom D

LICS-SAT-RTA Joint Banquet (19:00‑22:00)
Location: Grand Ballroom B