Sciweavers

Share
CP
2008
Springer
10 years 1 months ago
A New Empirical Study of Weak Backdoors
Abstract. Work by Kilby, Slaney, Thiebaux and Walsh [1] showed that the backdoors and backbones of unstructured Random 3SAT instances are largely disjoint. In this work we extend t...
Peter Gregory, Maria Fox, Derek Long
ECAI
2006
Springer
10 years 1 months ago
Solving Optimization Problems with DLL
Propositional satisfiability (SAT) is a success story in Computer Science and Artificial Intelligence: SAT solvers are currently used to solve problems in many different applicati...
Enrico Giunchiglia, Marco Maratea
MEMOCODE
2003
IEEE
10 years 5 months ago
Methods for exploiting SAT solvers in unbounded model checking
— Modern SAT solvers have proved highly successful in finding counterexamples to temporal properties of systems, using a method known as ”bounded model checking”. It is natu...
Kenneth L. McMillan
ASPDAC
2005
ACM
85views Hardware» more  ASPDAC 2005»
10 years 5 months ago
Integration of supercubing and learning in a SAT solver
Abstract— Learning is an essential pruning technique in modern SAT solvers, but it exploits a relatively small amount of information that can be deduced from the conflicts. Rece...
Domagoj Babic, Alan J. Hu
SAT
2007
Springer
73views Hardware» more  SAT 2007»
10 years 5 months ago
SAT Solving for Termination Analysis with Polynomial Interpretations
Abstract. Polynomial interpretations are one of the most popular techniques for automated termination analysis and the search for such interpretations is a main bottleneck in most ...
Carsten Fuhs, Jürgen Giesl, Aart Middeldorp, ...
SAT
2009
Springer
79views Hardware» more  SAT 2009»
10 years 6 months ago
Minimizing Learned Clauses
Minimizing learned clauses is an effective technique to reduce memory usage and also speed up solving time. It has been implemented in MINISAT since 2005 and is now adopted by mos...
Niklas Sörensson, Armin Biere
DATE
2009
IEEE
85views Hardware» more  DATE 2009»
10 years 6 months ago
Faster SAT solving with better CNF generation
Boolean satisfiability (SAT) solving has become an enabling technology with wide-ranging applications in numerous disciplines. These applications tend to be most naturally encode...
Benjamin Chambers, Panagiotis Manolios, Daron Vroo...
CP
2009
Springer
11 years 9 days ago
On the Power of Clause-Learning SAT Solvers with Restarts
In this work, we improve on existing work that studied the relationship between the proof system of modern SAT solvers and general resolution. Previous contributions such as those ...
Knot Pipatsrisawat, Adnan Darwiche
DAC
2004
ACM
11 years 19 days ago
Refining the SAT decision ordering for bounded model checking
Bounded Model Checking (BMC) relies on solving a sequence of highly correlated Boolean satisfiability (SAT) problems, each of which corresponds to the existence of counter-example...
Chao Wang, HoonSang Jin, Gary D. Hachtel, Fabio So...
books