Name
Abstract | ||
|---|---|---|
The paper is concerned with the computational evaluation of a new branching heuristic, called reverse assignment sequence (RAS), for evolved DPLL Satisfiability solvers. Such heuristic, like several other recent ones, is based on the history of 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 dierent values. The branching variable is then selected by using the maximum score. This branching heuristic is introduced in two evolved DPLL solvers: ZCha and Simo. Experiments on several benchmark series, both satisfiable and unsatisfiable, demonstrate advantages of the proposed heuristic. |
Year | Venue | Keywords |
|---|---|---|
2004 | SAT | satisfiability,sat solver |
Field | DocType | Citations |
Heuristic,Computer science,Satisfiability,Theoretical computer science,DPLL algorithm,Branching (version control) | Conference | 3 |
PageRank | References | Authors |
0.41 | 15 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Renato Bruni | 1 | 127 | 15.79 |
| Andrea Santori | 2 | 4 | 0.76 |