Catálogo de publicaciones - libros

We define a collection of mappings that transform many-valued clausal forms into satisfiability equivalent Boolean clausal forms, analyze their complexity and evaluate them empirically on a set of benchmarks with state-of-the-art SAT solvers. Our results provide empirical evidence that encoding combinatorial problems with the mappings defined here can lead to substantial performance improvements in complete SAT solvers.

The problem of deciding satisfiability of Boolean combinations of difference constraints is at the core of many important techniques such as planning, scheduling and bounded model checking of real-time systems. Efficient decision procedures for this class of formulas are, therefore, strongly needed. In this paper we present TSAT++, a system implementing a SAT-based decision procedure for this problem, and the techniques implemented in it; in particular, TSAT++ takes full advantage of recent SAT techniques. Comparative experimental results indicate that TSAT++ outperforms its competitors both on randomly generated, hand-made and real world problems.

Conjunctive-query containment is considered as a fundamental problem in database query evaluation and optimization. Kolaitis and Vardi pointed out that constraint satisfaction and conjunctive query containment are essentially the same problem. We study the Boolean conjunctive queries under a more detailed scope, where we investigate their counting problem by means of the algebraic approach through Galois theory, taking advantage of Post’s lattice. We prove a trichotomy theorem for the generalized conjunctive query counting problem, showing this way that, contrary to the corresponding decision problems, constraint satisfaction and conjunctive-query containment differ for other computational goals. We also study the audit problem for conjunctive queries asking whether there exists a frozen variable in a given query. This problem is important in databases supporting statistical queries. We derive a dichotomy theorem for this audit problem that sheds more light on audit applicability within database systems.

We focus on (iCTS), a promising way to push standard SAT-based approaches beyond their limits. We propose the first comprehensive framework that encompasses all the aspects of an , from the encoding to the incremental solver. We apply our guidelines to a real-world CTS approach () and show how to modify both the generation mechanism of a real BMC tool () and the solving engine of a public-domain SAT solver (). Related approaches and experimental results are discussed as well.

We present a novel expansion based decision procedure for quantified boolean formulas (QBF) in conjunctive normal form (CNF). The basic idea is to resolve existentially quantified variables and eliminate universal variables by expansion. This process is continued until the formula becomes propositional and can be solved by any SAT solver. On structured problems our implementation is competitive with state-of-the-art QBF solvers based on DPLL. It is orders of magnitude faster on certain hard to solve instances.

We make use of the algebraic theory that has been used to study the complexity of constraint satisfaction problems, to investigate tractable quantified boolean formulas. We present a pair of results: the first is a new and simple algebraic proof of the tractability of quantified 2-satisfiability; the second is a purely algebraic characterization of models for quantified Horn formulas that were given by Kleine Büning, Subramani, and Zhao, and described proof-theoretically.

Recently Schuler [17] presented a randomized algorithm that solves SAT in expected time at most up to a polynomial factor, where and are, respectively, the number of variables and the number of clauses in the input formula. This bound is the best known upper bound for testing satisfiability of formulas in CNF with no restriction on clause length (for the case when is not too large comparing to ). We derandomize this algorithm using deterministic -SAT algorithms based on search in Hamming balls, and we prove that our deterministic algorithm has the same upper bound on the running time as Schuler’s randomized algorithm.

Combining graph theory and linear algebra, we study SAT problems of low “linear algebra complexity”, considering formulas with bounded hermitian rank. We show polynomial time SAT decision of the class of formulas with hermitian rank at most one, applying methods from hypergraph transversal theory. Applications to heuristics for SAT algorithms and to the structure of minimally unsatisfiable clause-sets are discussed.

During the recent years, the development of tools for deciding Quantified Boolean Formulas (QBFs) satisfiability has been accompanied by a steady supply of real-world instances, i.e., QBFs originated by translations from application domains such as formal verification and planning. QBFs from these domains showed to be challenging for current state-of-the-art QBF solvers, and, in order to tackle them, several techniques and even specialized solvers have been proposed. Among these techniques, there are () efficient detection and propagation of unit and monotone literals, () branching heuristics that leverages the information extracted during the learning phase, and () look-back techniques based on learning.

In this paper we discuss their implementation in our state-of-the-art solver , pointing out the non trivial issues that arised in the process. We show that all the techniques positively contribute to performances . In particular, we show that monotone literal fixing is the most important technique in order to improve capacity, followed by learning and the heuristics. The situation is reversed if we consider productivity. These and other observations are detailed in the body of the paper. For our analysis, we consider the formal verification and planning benchmarks from the 2003 QBF evaluation.

In this paper, a new polynomial time technique for extracting functional dependencies in Boolean formulas is proposed. It makes an original use of the well-known Boolean constraint propagation technique (BCP) in a new preprocessing approach that extracts more hidden Boolean functions and dependent variables than previously published approaches on many classes of instances.