DocumentCode
405774
Title
A SAT solver using advanced reasoning
Author
Min Ding ; Pushan Tang
Author_Institution
Microelectron. Dept., Fudan Univ., Shanghai, China
Volume
1
fYear
2003
fDate
21-24 Oct. 2003
Firstpage
183
Abstract
This paper presents a SAT solver. The main purpose is to study the tradeoff between more reasoning and quicker decision. It shows that though good result can be obtained by quick decision and fast implementation, the reasoning step is still useful in several benchmarks. We choose FLD as our reasoning technique and discuss heuristic of obtaining the set of literals to be tested in FLD. Experiment results show that by careful implementation, this old technique still can be used in a fast SAT solver.
Keywords
computability; computational complexity; constraint handling; decision making; learning (artificial intelligence); BCP; FLD; SAT solver; boolean constraint propagation; decision making; failed literal detection; learning; reasoning technique; satisfiability solver;
fLanguage
English
Publisher
ieee
Conference_Titel
ASIC, 2003. Proceedings. 5th International Conference on
ISSN
1523-553X
Print_ISBN
0-7803-7889-X
Type
conf
DOI
10.1109/ICASIC.2003.1277519
Filename
1277519
Link To Document