Catálogo de publicaciones - libros

An of variables is one in which no two variables occur in the same clause in a given instance of -SAT. Instances of -SAT with an independent set of size can be solved in time, within a polynomial factor of 2. In this paper, we present an algorithm for -SAT based on a modification of the . Our algorithm runs within a polynomial factor of , where is the size of an independent set. We also present a variant of Schöning’s randomized local-search algorithm for -SAT that runs in time which is with in a polynomial factor of .

Structural logical formulas sometimes yield a substantial fraction of so called equivalence clauses after translation to CNF. Probably the best known example of this is the -family. Large instances of such CNF formulas cannot be solved in reasonable time if no detection of, and extra reasoning with, these clauses is incorporated. That is, in solving these formulas, there is a more or less separate algorithmic device dealing with the equivalence clauses, called equivalence reasoning, and another dealing with the remaining clauses. In this paper we propose a way to align these two reasoning devices by introducing parameters for which we establish optimal values over a variety of existing benchmarks. We obtain a truly convincing speed-up in solving such formulas with respect to the best solving methods existing so far.

The DPLL procedure has found great success in SAT, where search terminates on the first solution discovered. We show that this procedure is equally promising in a problem where exhaustive search is used, given that it is augmented with appropriate caching. Specifically, we propose two DPLL-based algorithms that construct OBDDs for CNF formulas. These algorithms have a worst-case complexity that is linear in the number of variables and size of the CNF, and exponential only in the or of the variable ordering. We show how modern SAT techniques can be harnessed by implementing the algorithms on top of an existing SAT solver. We discuss the advantage of this new construction method over the traditional approach, where OBDDs for subsets of the CNF formula are built and conjoined. Our experiments indicate that on many CNF benchmarks, the new method runs orders of magnitude faster than a comparable implementation of the traditional method.

We provide a rigorous analysis of a greedy approximation algorithm for the maximum random -SAT (MAX-R-SAT) problem. The algorithm assigns variables one at a time in a predefined order. A variable is assigned TRUE if it occurs more often positively than negatively; otherwise, it is assigned FALSE. After each variable assignment, problem instance is simplified and a new variable is selected. We show that this algorithm gives a 10/9.5-approximation, improving over the 9/8-approximation given by de la Vega and Karpinski [7]. The new approximation ratio is achieved by using a different algorithm than the one proposed in [7], along with a new upper bound on the maximum number of clauses that can be satisfied in a random -SAT formula [2].

The Boolean circuits is well established as a data structure for building propositional encodings of problems in preparation for satisfiability solving. The standard method for converting Boolean circuits to clause form (naming every vertex) has a number of shortcomings.

In this paper we give a projection of several well-known clause form conversions to a simplified form of Boolean circuit. We introduce a new conversion which we show is equivalent to that of Boy de la Tour in certain circumstances and is hence optimal in the number of clauses that it produces. We extend the algorithm to cover reduced Boolean circuits, a data structure used by the model checker NuSMV.

We present experimental results for this and other conversion procedures on BMC problems demonstrating its superiority, and conclude that the CNF conversion has a significant role in reducing the overall solving time.

We introduce a highly structured family of hard satisfiable 3-SAT formulas corresponding to an ordered spin-glass model from statistical physics. This model has provably “glassy” behavior; that is, it has many local optima with large energy barriers between them, so that local search algorithms get stuck and have difficulty finding the true “ground state,” i.e., the unique satisfying assignment. We test the hardness of our formulas with two Davis-Putnam solvers, and , the recently introduced Survey Propagation (), and two local search algorithms, and Record-to-Record Travel (). We compare our formulas to random 3-XOR-SAT formulas and to two other generators of hard satisfiable instances, the minimum disagreement parity formulas of Crawford et al., and Hirsch’s . For the complete solvers the running time of our formulas grows exponentially in , and exceeds that of random 3-XOR-SAT formulas for small problem sizes. is unable to solve our formulas with as few as 25 variables. For , our formulas appear to be harder than any other known generator of satisfiable instances. Finally, our formulas can be solved efficiently by but only if the parameter is tuned to the height of the barriers between local minima, and we use this parameter to measure the barrier heights in random 3-XOR-SAT formulas as well.

CirCUs is a satisfiability solver that works on a combination of an And-Inverter-Graph (AIG), Conjunctive Normal Form (CNF) clauses, and Binary Decision Diagrams (BDDs). We show how BDDs are used by CirCUs to help in the solution of SAT instances given in CNF. Specifically, the clauses are sorted by solving a hypergraph linear arrangement problem. Then they are clustered by an algorithm that strives to avoid explosion in the resulting BDD sizes. If clustering results in a single diagram, the SAT instance is solved directly. Otherwise, search for a satisfying assignment is conducted on the original clauses, enhanced with information extracted from the BDDs. We also describe a new decision variable selection heuristic that is based on recognizing that the variables involved in a conflict clause are often best treated as a related group. We present experimental results that demonstrate CirCUs’s efficiency especially for medium-size SAT instances that are hard to solve by traditional solvers based on DPLL.

In this paper, the notion of equivalence models for quantified Boolean formulas with free variables is introduced. The computational complexity of the equivalence model checking problem is investigated in the general case and in some restricted cases. We also establish a connection between the structure of some quantified Boolean formulas and the structure of models.

Recent work has shown how to use OBDDs for satisfiability solving. The idea of this approach, which we call , is to view an instance of propositional satisfiability as an existentially quantified propositional formula. Satisfiability solving then amounts to quantifier elimination; once all quantifiers have been eliminated we are left with either or . Our goal in this work is to study the effectiveness of symbolic quantifier elimination as an approach to satisfiability solving. To that end, we conduct a direct comparison with the DPLL-based ZChaff, as well as evaluate a variety of optimization techniques for the symbolic approach. In comparing the symbolic approach to ZChaff, we evaluate scalability across a variety of classes of formulas. We find that no approach dominates across all classes. While ZChaff dominates for many classes of formulas, the symbolic approach is superior for other classes of formulas.

Once we have demonstrated the viability of the symbolic approach, we focus on optimization techniques for this approach. We study techniques from constraint satisfaction for finding a good plan for performing the symbolic operations of conjunction and of existential quantification. We also study various variable-ordering heuristics, finding that while no heuristic seems to dominate across all classes of formulas, the maximum-cardinality search heuristic seems to offer the best overall performance.

We consider the satisfiability problem for CNF formulas that contain a (hidden) Horn and a 2-CNF (also called quadratic) part, called . We show that SAT remains NP-complete for such instances and also that any SAT instance can be encoded in terms of a mixed Horn formula in polynomial time. Further, we provide an exact deterministic algorithm showing that SAT for mixed (hidden) Horn formulas containing variables is solvable in time (2). A strong argument showing that it is hard to improve a time bound of (2) for mixed Horn formulas is provided. We also obtain a fixed-parameter tractability classification for SAT restricted to mixed Horn formulas of at most variables in its positive 2-CNF part providing the bound (||||2). Motivating examples for mixed Horn formulas are level graph formulas [14] and graph colorability formulas.