Catálogo de publicaciones - libros

We show how to aggressively add uninferred constraints, in a controlled manner, to formulae for finding Van der Waerden numbers during search. We show that doing so can improve the performance of standard SAT solvers on these formulae by orders of magnitude. We obtain a new and much greater lower bound for one of the Van der Waerden numbers, specifically a bound of 1132 for (2,6). We believe this bound to actually be the number we seek. The structure of propositional formulae for solving Van der Waerden numbers is similar to that of formulae arising from Bounded Model Checking. Therefore, we view this as a preliminary investigation into solving hard formulae in the area of Formal Verification.

The choice of the variable to flip in the Walksat family procedures is always random in that it is selected from a randomly chosen unsatisfied clause . This choice in Novelty or R-Novelty heuristics also contains some determinism in that the variable to flip is always limited to the two best variables in . In this paper, we first propose a diversification parameter for Novelty (or R-Novelty) heuristic to break the determinism in Novelty and show its performance compared with the random walk parameter in Novelty+. Then we exploit promising decreasing paths in a deterministic fashion in local search using a gradient-based approach. In other words, when promising decreasing paths exist, the variable to flip is no longer selected from a randomly chosen unsatisfied clause but in a deterministic fashion to surely decrease the number of unsatisfied clauses. Experimental results show that the proposed diversification and the determinism allow to significantly improve Novelty (and Walksat).

Much attention has been given in recent years to the problem of finding Minimally Unsatisfiable Subformulas (MUSes) of Boolean formulas. In this paper, we present a new view of the problem, strongly linking it to the maximal satisfiability problem. From this relationship, we have developed a novel technique for extracting all MUSes of a CNF formula, tightly integrat ing our implementation with a modern SAT solver. We also present another algorithm for finding all MUSes, developed independently but based on the same relationship. Experimental comparisons show that our approach is con sistently faster than the other, and we discuss ways in which ideas from both could be combined to improve further.

Advances in SAT solver technology have enabled many automated analysis and reasoning tools to reduce their input problem to a SAT problem, and then to use an efficient SAT solver to solve the underlying analysis or reasoning problem. The solving time for SAT solvers can vary substantially for semantically identical SAT problems depending on how the problem is expressed. This property motivates the development of new optimization techniques whose goal is to produce more efficiently solvable SAT problems, thereby improving the overall performance of the analysis or reasoning tool.

This paper presents our experience using several mechanical techniques that enable the Alloy Analyzer to generate optimized SAT formulas from first-order logic formulas. These techniques are inspired by similar techniques from the field of optimizing compilers, suggesting the potential presence of underlying connections between optimization problems from two very different domains. Our experimental results show that our techniques can deliver substantial performance improvement results—in some cases, they reduce the solving time by an order of magnitude.

Many current local search algorithms for SAT fall into one of two classes. Random walk algorithms such as Walksat/SKC, Novelty+ and HWSAT are very successful but can be trapped for long periods in deep local minima. Clause weighting algorithms such as DLM, GLS, ESG and SAPS are good at escaping local minima but require expensive smoothing phases in which all weights are updated. We show that Walksat performance can be greatly enhanced by weighting variables instead of clauses, giving the best known results on some benchmarks. The new algorithm uses an efficient weight smoothing technique with no smoothing phase.

The PPSZ Algorithm presented by Paturi, Pudlak, Saks, and Zane in 1998 has the nice feature that the only satisfying solution of a uniquely satisfiable 3-SAT formula can be found in expected running time at most . Using the technique of limited independence, we can derandomize this algorithm yielding deterministic running time at most.

An important extension of satisfiability testing is model-counting, a task that corresponds to problems such as probabilistic reasoning and computing the permanent of a Boolean matrix. We recently introduced Cachet, an exact model-counting algorithm that combines formula caching, clause learning, and component analysis. This paper reports on experiments with various techniques for improving the performance of Cachet, including component-selection strategies, variable-selection branching heuristics, randomization, backtracking schemes, and cross-component implications. The result of this work is a highly-tuned version of Cachet, the first (and currently, only) system able to exactly determine the marginal probabilities of variables in random 3-SAT formulas with 150+ variables. We use this to discover an interesting property of random formulas that does not seem to have been previously observed.

In this paper, we present a hybrid method for deciding problems involving integer and Boolean variables which is based on generic SAT solving techniques augmented with a) a polynomial-time ILP solver for the special class of Unit-Two-Variable-Per-Inequality (unit TVPI or UTVPI) constraints and b) an independent solver for general integer linear constraints. In our approach, we present a novel method for encoding linear constraints into the SAT solver through binary “indicator” variables. The hybrid SAT problem is subsequently solved using a SAT search procedure in close collaboration with the UTVPI solver. The UTVPI solver interacts closely with the Boolean SAT solver by passing implications and conflicting assignments. The non-UTVPI constraints are handled separately and participate in the learning scheme of the SAT solver through an innovative method based on the theory of cutting planes. Empirical evidence on software verification benchmarks is presented that demonstrates the advantages of our combined method.

We present , a Java tool to visualize the structure of SAT instances and runs of the DPLL (Davis-Putnam-Logemann-Loveland) procedure. uses advanced graph layout algorithms to display the problem’s internal structure arising from its variable dependency (interaction) graph. is also able to generate animations showing the dynamic change of a problem’s structure during a typical DPLL run. Besides implementing a simple variant of the DPLL algorithm on its own, also features an interface to MiniSAT, a state-of-the-art DPLL implementation. Using this interface, runs of MiniSAT can be visualized—including the generated search tree and the effects of clause learning. is supposed to help in teaching the DPLL algorithm and in gaining new insights in the structure (and hardness) of SAT instances.

Over the years, a steadily improving series of local search solvers for propositional satisfiability (SAT) have been constructed. However, these solvers are often fragile, in that they have apparently minor details in their implementation that dramatically affect performance and confound understanding. In order to understand and predict the success of differing strategies, various local search have been proposed. Many of these metrics summarize properties of the boolean assignments examined during the search. This has two consequences: first, they only capture one side of satisfiability, failing to characterize the behaviour with respect to constraints. Secondly, the boolean requirement limits the applicability of these metrics to more general (CSPs), which can have non-boolean domains.

In response, we present , derived from existing (boolean assignment) metrics, that are based on the states of constraints during the search. Experimental results show a strong relationship between the primal and dual versions of these metrics on a variety of random and structured problems. This dual perspective can be easily applied to both SAT and general CSPs, allowing for new insights into the workings of a broad class of local search methods.