Journal on Satisfiability,Boolean Modelling and Computation

This paper is concerned with the complexity of some natural subclasses of minimal unsatisfiable formulas. We show the D P –completeness of the classes of maximal and marginal minimal unsatisfiable formulas. Then we consider the class Unique–MU of minimal unsatisfiable formulas which have after removing a clause exactly one satisfying truth assignment. We show that Unique–MU has the same complexity as the unique satisfiability problem with respect to polynomial reduction. However, a slight modification of this class leads to the D P –completeness. Finally we show that the class of minimal unsatisfiable formulas which can be divided for every variable into two separate minimal unsatisfiable formulas is at least as hard as the unique satisfiability problem.

Inductive data types are a valuable modeling tool for software verification. In the past, decision procedures have been proposed for various theories of inductive data types, some focused on the universal fragment, and some focused on handling arbitrary quantifiers. Because of the complexity of the full theory, previous work on the full theory has not focused on strategies for practical implementation. However, even for the universal fragment, previous work has been limited in several significant ways. In this paper, we present a general and practical algorithm for the universal fragment. The algorithm is presented declaratively as a set of abstract rules which we show to be terminating, sound, and complete. We show how other algorithms can be realized as strategies within our general framework, and we propose a new strategy and give experimental results indicating that it performs well in practice. We conclude with a discussion of several useful ways the algorithm can be extended.

The last few years have seen the advent of a new breed of decision procedures for various fragments of first-order logic based on propositional abstraction. A lazy satisfiability checker for a given fragment of first-order logic invokes a theory-specific decision procedure (a theory solver) on a (partial) model for the abstraction. If the model is found to be consistent in the given theory, then a model for the original formula has been found. Otherwise, a refinement of the propositional abstraction is extracted from the proof of inconsistency and the search is resumed. We describe a theory solver for integer difference logic that is effective when the formula to be decided contains equality and disequality (negated equality) constraints so that the decision problem partakes of the nature of the pigeonhole problem. We propose a reduction of the problem to propositional satisfiability by computing bounds on a sufficient subset of solutions, and present experimental evidence for the efficiency of this approach.

We consider the satisfiability problem for Boolean combinations of unit two variable per inequality (UTVPI) constraints. A UTVPI constraint is linear constraint containing at most two variables with non-zero coefficients, where furthermore those coefficients must be either − 1 or 1. We prove that if a satisfying solution exists, then there is a solution with each variable taking values in [ − n · ( b max + 1 ) , n · ( b max + 1 ) ] , where n is the number of variables, and b max is the maximum over the absolute values of constants appearing in the constraints. This solution bound improves over previously obtained bounds by an exponential factor. Our result can be used in a finite instantiation-based approach to deciding satisfiability of UTVPI formulas. An experimental evaluation demonstrates the efficiency of such an approach. One of our key results is to show that an integer point inside a UTVPI polyhedron, if one exists, can be obtained by rounding a vertex. As a corollary of this result, we also obtain a polynomial-time algorithm for approximating optima of UTVPI integer programs to within an additive factor.

Existing difference logic (DL) solvers can be broadly classified as eager or lazy, each with its own merits and de-merits. We propose a novel difference logic solver SDSAT that combines the strengths of both these approaches and provides a robust performance over a wide set of benchmarks. The solver SDSAT works in two phases: allocation and solve. In the allocation phase, it allocates non-uniform adequate ranges for variables appearing in difference predicates. This phase is similar to previous small domain encoding approaches, but uses a novel algorithm Nu-SMOD with 1-2 orders of magnitude improvement in performance and smaller ranges for variables. Furthermore, the difference logic formula is not transformed into an equi-satisfiable Boolean formula in a single step, but rather done lazily in the following phase. In the solve phase, SDSAT uses a lazy refinement approach to search for a satisfying model within the allocated ranges. Thus, any partially DL-theory consistent model can be discarded if it cannot be satisfied within the allocated ranges. Note the crucial difference: in eager approaches, such a partially consistent model is not allowed in the first place, while in lazy approaches such a model is never discarded. Moreover, we dynamically refine the allocated ranges and search for a feasible solution within the updated ranges. This combined approach benefits from both the smaller search space (as in eager approaches) and also from the theory-specific graph-based algorithms (characteristic of lazy approaches). Experimental results show that our method is robust and always better than or comparable to state-of-the art solvers using similar eager or lazy techniques.