We give a randomized algorithm for testing satisfiability of Boolean formulas in conjunctive normal form with no restriction on clause length. Its running time is at most 2n(1−1...
We propose a new decision heuristic for DPLL-based propositional SAT solvers. Its essence is that both the initial and the conflict clauses are arranged in a list and the next deci...
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...
We introduce two incomplete polynomial time algorithms to solve satisfiability problems which both use Linear Programming (LP) techniques. First, the FlipFlop LP attempts to simul...
Current algorithms for bounded model checking (BMC) use SAT methods for checking satisfiability of Boolean formulas. These BMC methods suffer from a potential memory explosion prob...
Abstract. We present a new generic problem solving approach for overconstrained problems based on Max-SAT. We first define a clausal form formalism that deals with blocks of clau...
Solvers for Quantified Boolean Formulae (QBF) use many analogues of technique from SAT. A significant amount of work has gone into extending conflict based techniques such as co...
We present two new branch and bound weighted Max-SAT solvers (Lazy and Lazy ) which incorporate original data structures and inference rules, and a lower bound of better quality.