Paper Info
Title
sharpSAT: counting models with advanced component caching and implicit BCP
Abstract
We introduce sharpSAT, a new #SAT solver that is based on the well known DPLL algorithm and techniques from SAT and #SAT solvers. Most importantly, we introduce an entirely new approach of coding components, which reduces the cache size by at least one order of magnitude, and a new cache management scheme. Furthermore, we apply a well known look ahead based on BCP in a manner that is well suited for #SAT solving. We show that these techniques are highly beneficial, especially on large structured instances, such that our solver performs significantly better than other #SAT solvers.
Year
DOI
Venue
2006
10.1007/11814948_38
SAT
Keywords
Field
DocType
large structured instance,dpll algorithm,sat solvers,implicit bcp,coding component,cache size,new cache management scheme,sat solver,advanced component caching,new approach,look ahead
Constraint satisfaction,Computer science,CPU cache,Boolean satisfiability problem,Satisfiability,Parallel computing,Propositional calculus,Theoretical computer science,DPLL algorithm,Conjunctive normal form,Solver
Conference
Volume
ISSN
ISBN
4121
0302-9743
3-540-37206-7
Citations 
PageRank 
References 
29
1.02
11
Authors
1
Name
Order
Citations
PageRank
Marc Thurley1996.02