Paper Info
Title
On-the-Fly Clause Improvement
Abstract
Abstract. Most current propositional SAT solvers apply resolution at various stages to derive new clauses or simplify existing ones. The former happens during conict analysis, while the latter is usually done during preprocessing. We show how subsumption,of the operands by the resolvent can be inexpensively detected during resolution; we then show how this detection is used to improve three stages of the SAT solver: variable elimination, clause distillation, and conict analysis. The ìon-the-yî subsumption,check is easily integrated in a SAT solver. In par- ticular, it is compatible with the strong conict analysis and the generation of unsatisability proofs. Experiments show the effectiveness of this technique and illustrate an interesting synergy between preprocessing and the DPLL procedure.
Year
DOI
Venue
2009
10.1007/978-3-642-02777-2_21
Theory and Applications of Satisfiability Testing
Keywords
Field
DocType
on-the-fly clause,strong conflict analysis,new clause,sat solvers,interesting synergy,dpll procedure,subsumption check,conflict analysis,clause distillation,current propositional,sat solver,variable elimination
Discrete mathematics,Variable elimination,Computer science,Boolean satisfiability problem,Operand,Algorithm,Mathematical proof,Preprocessor,Conjunctive normal form,DPLL algorithm,Conflict analysis
Conference
Volume
ISSN
Citations 
5584
0302-9743
19
PageRank 
References 
Authors
0.69
8
2
Name
Order
Citations
PageRank
Hyojung Han1613.51
Fabio Somenzi23394302.47