Catálogo de publicaciones - libros

Input Distance (Δ) is introduced as a metric for propositional resolution derivations. If is a formula and is a clause, then is defined as min | – |. The Δ for a derivation is the maximum Δ of any clause in the derivation. Input Distance provides a refinement of the clause-width metric analyzed by Ben-Sasson and Wigderson (JACM 2001) in that it applies to families whose clause width grows, such as pigeon-hole formulas. They showed two upper bounds on , where is the maximum clause width of a narrowest refutation of . It is shown here that (1) both bounds apply with replaced by Δ; (2) for pigeon-hole formulas PHP(, ), the minimum Δ for any refutation is Ω(). A similar result is conjectured for the () family analyzed by Bonet and Galesi (FOCS 1999).

Recently the Mathematical Programming community showed a renewed interest in Hilbert’s Positivstellensatz. The reason for this is that global optimization of polynomials in ℝ[,...,] is -hard, while the question whether a polynomial can be written as a sum of squares has tractable aspects. This is due to the fact that Semidefinite Programming can be used to decide in polynomial time (up to a prescribed precision) whether a polynomial can be rewritten as a sum of squares of linear combinations of monomials coming from a specified set. We investigate this approach in the context of Satisfiability. We examine the potential of the theory for providing tests for unsatisfiability and providing MAXSAT upper bounds. We compare the SOS (Sums Of Squares) approach with existing upper bound and rounding techniques for the MAX-2-SAT case of Goemans and Williamson [8] and Feige and Goemans [6] and the MAX-3-SAT case of Karloff and Zwick [9], which are based on Semidefinite Programming as well. We show that the combination of the existing rounding techniques with the SOS based upper bound techniques yields polynomial time algorithms with a performance guarantee at least as good as the existing ones, but observably better in particular cases.

We present an algorithm that decides the satisfiability of a formula on CNF form in time (1.1279), if has at most occurrences per variable or if has an average of occurrences per variable and no variable occurs only once. For ≤ 4, this is better than previous results. This is the first published algorithm that is explicitly constructed to be efficient for cases with a low number of occurrences per variable. Previous algorithms that are applicable to this case exist, but as these are designed for other (more general, or simply different) cases, their performance guarantees for this case are weaker.

We introduce ApproxCount, an algorithm that approximates the number of satisfying assignments or models of a formula in propositional logic. Many AI tasks, such as calculating degree of belief and reasoning in Bayesian networks, are computationally equivalent to model counting. It has been shown that model counting in even the most restrictive logics, such as Horn logic, monotone CNF and 2CNF, is intractable in the worst-case. Moreover, even approximate model counting remains a worst-case intractable problem. So far, most practical model counting algorithms are based on backtrack style algorithms such as the DPLL procedure. These algorithms typically yield exact counts but are limited to relatively small formulas. Our ApproxCount algorithm is based on SampleSat, a new algorithm that samples from the solution space of a propositional logic formula near-uniformly. We provide experimental results for formulas from a variety of domains. The algorithm produces good estimates for formulas much larger than those that can be handled by existing algorithms.

Modern SAT solvers are highly dependent on heuristics. Therefore, benchmarking is of prime importance in evaluating the performances of different solvers. However, relevant benchmarking is not necessarily straightforward. We present our experiments using the IBM CNF Benchmark on several SAT solvers. Using the results, we attempt to define guidelines for a relevant benchmarking methodology, using SAT solvers for real life BMC applications.

In this paper, the notions of polynomial–time model equivalent reduction and polynomial–space model equivalent reduction are introduced in order to investigate in a subtle way the expressive power of different theories. We compare according to these notions some classes of propositional formulas and quantified Boolean formulas. Our results show that classes of theories with the same complexity might have different representation strength under some conjectures which are widely believed to be true in computation complexity theory.

We present two new branch and bound weighted Max-SAT solvers ( and *) which incorporate original data structures and inference rules, and a lower bound of better quality.

We present a method—called quantifier tree reconstruction—that allows to efficiently recover a portion of the internal structure of QBF instances which was hidden as a consequence of the cast to prenex normal form. Means to profit from a quantifier tree are presented for all the main families of QBF solvers. Experiments on QBFLIB instances are also reported.

In this paper, quantified Horn formulas with free variables () are investigated. The main result is that any quantified Horn formula Φ of length |Φ| with free variables, |∀| universal quantifiers and an arbitrary number of existential quantifiers can be transformed into an equivalent formula of length (| ∀ | ·|Φ|) which contains only existential quantifiers. Moreover, it is shown that quantified Horn formulas with free variables have equivalence models where every existential quantifier is associated with a monotone Boolean function.

The results allow a simple representation of quantified Horn formulas as purely existentially quantified Horn formulas (∃ ). An application described in the paper is to solve -SAT in (| ∀ | ·|Φ|) by using this transformation in combination with a linear-time satisfiability checker for propositional Horn formulas.

Many solvers have been designed for s, the validity problem for Quantified Boolean Formulas for the past few years. In this paper, we describe a new branching heuristics whose purpose is to promote renamable Horn formulas. This heuristics is based on Hébrard’s algorithm for the recognition of such formulas. We present some experimental results obtained by our solver with the new branching heuristics and show how its performances are improved.