Sciweavers

SAT
2005
Springer
111views Hardware» more  SAT 2005»
14 years 4 months ago
On Subsumption Removal and On-the-Fly CNF Simplification
Conjunctive Normal Form (CNF) Boolean formulas generated from resolution or solution enumeration often have much redundancy. It is desirable to have an efficient algorithm to simpl...
Lintao Zhang
SAT
2005
Springer
145views Hardware» more  SAT 2005»
14 years 4 months ago
A New Approach to Model Counting
We introduce ApproxCount, an algorithm that approximates the number of satisfying assignments or models of a formula in propositional logic. Many AI tasks, such as calculating degr...
Wei Wei, Bart Selman
SAT
2005
Springer
98views Hardware» more  SAT 2005»
14 years 4 months ago
Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variable
We present an algorithm that decides the satisfiability of a
Magnus Wahlström
SAT
2005
Springer
162views Hardware» more  SAT 2005»
14 years 4 months ago
Heuristics for Fast Exact Model Counting
An important extension of satisfiability testing is model-counting, a task that corresponds to problems such as probabilistic reasoning and computing the permanent of a Boolean ma...
Tian Sang, Paul Beame, Henry A. Kautz
SAT
2005
Springer
95views Hardware» more  SAT 2005»
14 years 4 months ago
Random Walk with Continuously Smoothed Variable Weights
Many current local search algorithms for SAT fall into one of two classes. Random walk algorithms such as Walksat/SKC, Novelty+ and HWSAT are very successful but can be trapped for...
Steven David Prestwich
SAT
2005
Springer
122views Hardware» more  SAT 2005»
14 years 4 months ago
A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas
We tackle the problem of finding a smallest-cardinality MUS (SMUS) of a given formula. The SMUS provides a succinct explanation of infeasibility and is valuable for applications th...
Maher N. Mneimneh, Inês Lynce, Zaher S. Andr...
SAT
2005
Springer
142views Hardware» more  SAT 2005»
14 years 4 months ago
Optimizations for Compiling Declarative Models into Boolean Formulas
Advances in SAT solver technology have enabled many automated analysis and reasoning tools to reduce their input problem to a SAT problem, and then to use an efficient SAT solver ...
Darko Marinov, Sarfraz Khurshid, Suhabe Bugrara, L...
SAT
2005
Springer
138views Hardware» more  SAT 2005»
14 years 4 months ago
On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization
The utilization of cutting planes is a key technique in Integer Linear Programming (ILP). However, cutting planes have seldom been applied in Pseudo-Boolean Optimization (PBO) algo...
Vasco M. Manquinho, João P. Marques Silva