Sciweavers

IJCAI
2003
13 years 6 months ago
Understanding the Power of Clause Learning
Efficient implementations of DPLL with the addition of clause learning are the fastest complete satisfiability solvers and can handle many significant real-world problems, such as...
Paul Beame, Henry A. Kautz, Ashish Sabharwal
AAAI
2010
13 years 6 months ago
A Restriction of Extended Resolution for Clause Learning SAT Solvers
Modern complete SAT solvers almost uniformly implement variations of the clause learning framework introduced by Grasp and Chaff. The success of these solvers has been theoretical...
Gilles Audemard, George Katsirelos, Laurent Simon
AAAI
2008
13 years 7 months ago
Clause Learning Can Effectively P-Simulate General Propositional Resolution
Currently, the most effective complete SAT solvers are based on the DPLL algorithm augmented by clause learning. These solvers can handle many real-world problems from application...
Philipp Hertel, Fahiem Bacchus, Toniann Pitassi, A...
AAAI
2008
13 years 7 months ago
On the Power of Top-Down Branching Heuristics
We study the relative best-case performance of DPLL-based structure-aware SAT solvers in terms of the power of the underlying proof systems. The systems result from (i) varying th...
Matti Järvisalo, Tommi A. Junttila
CP
2003
Springer
13 years 9 months ago
Ten Challenges Redux: Recent Progress in Propositional Reasoning and Search
Abstract. In 1997 we presented ten challenges for research on satisfiability testing [1]. In this paper we review recent progress towards each of these challenges, including our o...
Henry A. Kautz, Bart Selman
CP
2003
Springer
13 years 9 months ago
Unrestricted Nogood Recording in CSP Search
Recently spectacular improvements in the performance of SAT solvers have been achieved through nogood recording (clause learning). In the CSP literature, on the other hand, nogood ...
George Katsirelos, Fahiem Bacchus
CP
2007
Springer
13 years 10 months ago
Limitations of Restricted Branching in Clause Learning
The techniques for making decisions, i.e., branching, play a central role in complete methods for solving structured CSP instances. In practice, there are cases when SAT solvers be...
Matti Järvisalo, Tommi A. Junttila