loading...
MFSAT: A SAT Solver Using Multi-Flip Local Search
Sacramento, California, USA November 03-November 05
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TAI.2003.125017415th IEEE International Conference on ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Amol Dattatraya Mali, University of Wisconsin at Milwaukee
Yevgeny Lipen, Strong Financial Corporation
Local search-based methods of SAT solving have received a significant attention in the last decade. All local search-based methods choose the next truth assignment by flipping the value of only one variable. Simultaneously flipping values of multiple variables on an iteration can allow a local search-based solver to take long leaps in the search space. We report on SAT solver MFSAT, which has nine local search-based procedures. One of them is similar to conventional procedures which flip the value of one variable on an iteration. Other eight procedures are capable of simultaneously flipping values of multiple variables on an iteration to generate the successor truth assignment. We call these procedures "multi-flip" procedures. We report on the empirical evaluation of the nine procedures on more than 2700 benchmark SAT problems. Our results show that multi-flip procedures solve many more problems than the uni-flip procedure. Several multi-flip procedures solve problems many times faster than the uni-flip procedure.
Citation:
Amol Dattatraya Mali, Yevgeny Lipen, "MFSAT: A SAT Solver Using Multi-Flip Local Search," ictai, pp.84, 15th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.