SAT 2004 START ConferenceManager    


Using Rewarding Mechanisms for Improving Branching Heuristics

Elsa Carvalho & Joćo Marques-Silva

Presented at The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada, 10-13 May 2004


Abstract

The variable braching heuristics used in the most recent and most effective SAT solvers, including zChaff and BerkMin, can be viewed as consisting of a simple mechanism for rewarding the variables participating in conflicts during the search process. In this paper we propose to extend the simple rewarding mechanism used in zChaff and BerkMin, and develop different rewarding based on information provided by the search algorithm, namely the size of learned clauses and the size of the backjumps in the search tree. The results show that very significant gains can be obtained for real-world problem instances of SAT.


  
START Conference Manager (V2.47.2)
Maintainer: rrgerber@softconf.com