SAT 2004 START ConferenceManager    


Adding a New Conflict Based Branching Heuristic in two Evolved DPLL SAT Solvers

Renato Bruni, Andrea Santori

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


Abstract

The paper is concerned with the computational evaluation of a new branching heuristic for evolved DPLL Satisfiability solvers. Such heuristic, like several other recent ones, is based on the conflicts obtained during the solution of an instance. A score is associated to each literal. When a conflict occurs, some scores are incremented with different values. The branching variable is then selected by choosing the maximum score. This branching heuristic is introduced in two evolved DPLL solvers: ZChaff and Simo. Experiments on several benchmark series, both satisfiable and unsatisfiable, demonstrate advantages of the proposed heuristic.


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