Sciweavers

AAAI
2010
13 years 9 months ago
Exploiting QBF Duality on a Circuit Representation
Search based solvers for Quantified Boolean Formulas (QBF) have adapted the SAT solver techniques of unit propagation and clause learning to prune falsifying assignments. The tech...
Alexandra Goultiaeva, Fahiem Bacchus
AI
2005
Springer
13 years 11 months ago
MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability
Maximum Boolean satisfiability (max-SAT) is the optimization counterpart of Boolean satisfiability (SAT), in which a variable assignment is sought to satisfy the maximum number of...
Zhao Xing, Weixiong Zhang
CORR
2008
Springer
108views Education» more  CORR 2008»
13 years 11 months ago
Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
Resolution refinements called w-resolution trees with lemmas (WRTL) and with input lemmas (WRTI) are introduced. Dag-like resolution is equivalent to both WRTL and WRTI when there...
Samuel R. Buss, Jan Hoffmann 0002, Jan Johannsen
CP
2007
Springer
14 years 3 months ago
On Inconsistent Clause-Subsets for Max-SAT Solving
Recent research has focused on using the power of look-ahead to speed up the resolution of the Max-SAT problem. Indeed, look-ahead techniques such as Unit Propagation (UP) allow to...
Sylvain Darras, Gilles Dequen, Laure Devendeville,...
DATE
2003
IEEE
92views Hardware» more  DATE 2003»
14 years 4 months ago
Local Search for Boolean Relations on the Basis of Unit Propagation
We propose a method for local search of Boolean relations relating variables of a CNF formula. The method is to branch on small subsets of the set of CNF variables and to analyze ...
Yakov Novikov
TABLEAUX
2005
Springer
14 years 5 months ago
Unit Propagation in a Tableau Framework
Unit propagation is one of the most important techniques of efficient SAT solvers. Unfortunately, this technique is not directly applicable to first-order clausal tableaux. We sho...
Gernot Stenz
FLOPS
2010
Springer
14 years 6 months ago
A Pearl on SAT Solving in Prolog
A succinct SAT solver is presented that exploits the control provided by delay declarations to implement watched literals and unit propagation. Despite its brevity the solver is su...
Jacob M. Howe, Andy King