Paper Info
Title
Sat-solving based on boundary point elimination
Abstract
We study the problem of building structure-aware SAT-solvers based on resolution. In this study, we use the idea of treating a resolution proof as a process of Boundary Point Elimination (BPE). We identify two problems of using SAT-algorithms with Conflict Driven Clause Learning (CDCL) for structure-aware SAT-solving. We introduce a template of resolution based SAT-solvers called BPE-SAT that is based on a few generic implications of the BPE concept. BPE-SAT can be viewed as a generalization of CDCL SAT-solvers and is meant for building new structure-aware SAT-algorithms. We give experimental results substantiating the ideas of the BPE approach. In particular, to show the importance of structural information we compare an implementation of BPE-SAT and state-of-the-art SAT-solvers on narrow CNF formulas.
Year
DOI
Venue
2010
10.1007/978-3-642-19583-9_12
Haifa Verification Conference
Keywords
Field
DocType
boundary point elimination,structure-aware sat-solving,bpe approach,cdcl sat-solvers,structure-aware sat-solvers,bpe concept,new structure-aware sat-algorithms,resolution proof,conflict driven clause,state-of-the-art sat-solvers,sat solver
Conflict-Driven Clause Learning,Boundary (topology),Computer science,Theoretical computer science,Artificial intelligence
Conference
Volume
ISSN
Citations 
6504
0302-9743
5
PageRank 
References 
Authors
0.55
11
2
Name
Order
Citations
PageRank
Eugene Goldberg1258.01
Panagiotis Manolios263453.62