Journal on Satisfiability, Boolean Modeling and Computation - Volume 1, issue 1

Authors: Anjos, Miguel F.

Article Type: Research Article

Abstract: Semidefinite optimization, commonly referred to as semidefinite programming, has been a remarkably active area of research in optimization during the last decade. For combinatorial problems in particular, semidefinite programming has had a truly significant impact. This paper surveys some of the results obtained in the application of semidefinite programming to satisfiability and maximum-satisfiability problems. The approaches presented in some detail include the ground-breaking approximation algorithm of Goemans and Williamson for MAX-2-SAT, the Gap relaxation of de Klerk, van Maaren and Warners, and strengthenings of the Gap relaxation based on the Lasserre hierarchy of semidefinite liftings for polynomial optimization problems. We …include theoretical and computational comparisons of the aforementioned semidefinite relaxations for the special case of 3-SAT, and conclude with a review of the most recent results in the application of semidefinite programming to SAT and MAX-SAT. Show more

Keywords: satisfiability, maximum-satisfiability, semidefinite programming, semidefinite optimization, approximation algorithms, semidefinite relaxations, lifting procedures

DOI: 10.3233/SAT190001

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 1, no. 1, pp. 1-47, 2006

Authors: Dantsin, Evgeny | Wolpert, Alexander

Article Type: Research Article

Abstract: We give a randomized algorithm for testing satisfiability of Boolean formulas in conjunctive normal form with no restriction on clause length. This algorithm uses the clause-shortening approach proposed by Schuler [14]. The running time of the algorithm is O ( 2 n ( 1 − 1 / α ) ) where α = ln ( m / n ) + O ( ln ln m ) and n , m are respectively the number of variables and the number of clauses in the input formula. This bound is asymptotically better …than the previously best known 2 n ( 1 − 1 / log ( 2 m ) ) bound for SAT. Show more

Keywords: SAT with no restriction on clause length, upper bound, clause shortening

DOI: 10.3233/SAT190002

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 1, no. 1, pp. 49-60, 2006

Authors: Coste-Marquis, Sylvie | Le Berre, Daniel | Letombe, Florian | Marquis, Pierre

Article Type: Research Article

Abstract: Several propositional fragments have been considered so far as target languages for knowledge compilation and used for improving computational tasks from major AI areas (like inference, diagnosis and planning); among them are the ordered binary decision diagrams, prime implicates, prime implicants, “formulae” in decomposable negation normal form. On the other hand, the validity problem val (QPROP PS ) for Quantified Boolean Formulae (QBF) has been acknowledged for the past few years as an important issue for AI, and many solvers have been designed. In this paper, the complexity of restrictions of the validity problem for QBF obtained by imposing …the matrix of the input QBF to belong to propositional fragments used as target languages for compilation, is identified. It turns out that this problem remains hard (PSPACE -complete) even under severe restrictions on the matrix of the input. Nevertheless some tractable restrictions are pointed out. Show more

Keywords: automated reasoning, quantified Boolean formulae

DOI: 10.3233/SAT190003

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 1, no. 1, pp. 61-88, 2006