loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Fourth International Workshop on Microprocessor Test and Verification Common Challenges and Solutions
Heuristic Backtracking Algorithms for SAT
Hyatt Town Lake Hotel, Austin, Texas
May 29-May 30
ISBN: 0-7695-2045-6
A. Bhalla, Technical University of Lisbon, Portugal
I. Lynce, Technical University of Lisbon, Portugal
J.T. de Sousa, Technical University of Lisbon, Portugal
J. Marques-Silva, Technical University of Lisbon, Portugal
In recent years backtrack search SAT solvers have been the subject of dramatic improvements. These improvements allowed SAT solvers to successfully replace BDDs in many areas of formal verification, and also motivated the development of many new challenging problem instances, many of which too hard for the current generation of SAT solvers. As a result, further improvements to SAT technology are expected to have key consequences in formal verification. The objective of this paper is to propose heuristic approaches to the backtrack step of backtrack search SAT solvers, with the goal of increasing the ability of the SAT solver to search different parts of the search space. The proposed heuristics to the backtrack step are inspired by the heuristics proposed in recent years for the branching step of SAT solvers, namely VSIDS and some of its improvements. The preliminary experimental results are promising, and motivate the integration of heuristic backtracking in state-of-the-art SAT solvers.
Citation:
A. Bhalla, I. Lynce, J.T. de Sousa, J. Marques-Silva, "Heuristic Backtracking Algorithms for SAT," mtv, pp.69, Fourth International Workshop on Microprocessor Test and Verification Common Challenges and Solutions, 2003
Usage of this product signifies your acceptance of the Terms of Use.