Title
Conditional Pure Literal Graphs
Abstract
Conditional Pure Literal Graphs (CPLG) characterize the set of models of a propositional formula and are introduced to help understand connections among formulas, models and autarkies. They have been applied to the SAT problem within the framework of refutation-based algorithms. Experimental results and comparisons show that the use of CPLGs is a promising direction towards efficient propositional SAT solvers based upon model elimination. In addition, they open a new perspective on hybrid search/resolution schemes.
Year
DOI
Venue
2001
10.1007/3-540-45744-5_25
IJCAR
Keywords
Field
DocType
model elimination,conditional pure literal graphs,sat problem,refutation-based algorithm,new perspective,hybrid search,propositional formula,efficient propositional,promising direction,sat solver
Model elimination,Graph,Discrete mathematics,Computer science,Sat problem,Satisfiability,Algorithm,Propositional calculus,Propositional variable,Propositional formula
Conference
ISBN
Citations 
PageRank 
3-540-42254-4
0
0.34
References 
Authors
19
1
Name
Order
Citations
PageRank
Marco Benedetti1312.60