Catálogo de publicaciones - libros

The importance of producing a certificate of unsatisfiability is increasingly recognized for high performance propositional satisfiability solvers. The leading solvers develop a conflict graph as the basis for deriving (or “learning”) new clauses. Extracting a resolution derivation from the conflict graph is theoretically straightforward, but it turns out to have some surprising practical pitfalls (as well as the unsurprising problem that resolution proofs can be extremely long). These pitfalls are exposed, solutions are presented, and analyzed for worse cases. Dramatic improvements on industrial benchmarks are demonstrated.

Finding small unsatisfiable cores for SAT problems has recently received a lot of interest, mostly for its applications in formal verification. Surprisingly, the same problem in the context of SAT Modulo Theories (SMT) has instead received very little attention in the literature; in particular, we are not aware of any work aiming at producing small unsatisfiable cores in SMT.

The purpose of this paper is to start filling the gap in this area, by proposing a novel approach for computing small unsat cores in SMT. The main idea is to combine an SMT solver with an external propositional core extractor: the SMT solver produces the theory lemmas found during the search; the core extractor is then called on the boolean abstraction of the original SMT problem and of the theory lemmas. This results in an unsatisfiable core for the original SMT problem, once the remaining theory lemmas have been removed.

The approach has several advantages: it is extremely simple to implement and to update, and it can be interfaced with every propositional core extractor in a plug-and-play way, so that to benefit for free of all unsat-core reduction techniques which have been or will be made available.

Polynomial interpretations are one of the most popular techniques for automated termination analysis and the search for such interpretations is a main bottleneck in most termination provers. We show that one can obtain speedups in orders of magnitude by encoding this task as a SAT problem and by applying modern SAT solvers.

In this paper, we study the use of QBF solvers for fault localization and correction of sequential circuits. Given a violated specification, we compute whether the circuit can be repaired by evaluating a sequence of quantified Boolean formulas. If a repair exists, it can be extracted from a certificate for another quantified Boolean formula. Because it only finds components when a repair is possible, this approach is more precise than a satisfiability-based approach that we have developed earlier. We demonstrate this in an experimental evaluation.

Unmanned aerial vehicles (UAVs) represent an important class of net worked robotic applications that must be both highly dependable and autonomous. This paper addresses sensor deployment problems for distributed failure diagnosis in such networks where multiple vehicles must agree on the fault status of another UAV. Sensor placement is formulated using an integer linear programming (ILP) approach and solved using Boolean satisfiability (SAT)-based ILP solvers as well as generic ILP solvers. Our results indicate that the proposed models are tractable for medium-sized UAV networks.

Inverting a function at a given point in its range involves finding any in the domain such that () = . This is a general problem. We wish to find a heuristic for inverting those functions which satisfy certain statistical properties similar to those of random functions. As an example, we choose popular secure hash functions which are expected to be hard to invert and any successful strategy to do so will be quite useful. This provides an excellent challenge for solvers. We first find the limits of inverting via direct encoding of these functions as : for this is one round and twelve steps and for it is one round and ten steps. Then, we show that by adding customized constraints obtained by modifying an earlier attack by Dobbertin, we can invert up to 2 rounds and 7 steps in < 8 hours.