Name
Abstract | ||
|---|---|---|
In mainstream conflict driven clause learning (CDCL) solvers, because of frequent restarts and phase saving, there exists a large proportion of duplicate assignment trails before and after restarts, resulting in unnecessary time wastage during solving. This paper proposes a new strategyidentifying those duplicate assignments trails and dealing with them by changing the sort order. This approach's performance is compared with that of the Luby static restart scheme and a dynamic Glucose-restart strategy. We show that the number of solved instances is increased by 3.2% and 4.6%. We also make a compassion with the MapleCOMSPS solver by testing against application benchmarks from the SAT Competitions 2015 to 2017. These empirical results provide further evidence of the benefits of the proposed heuristic, having the advantage of managing duplicate assignments trails and choosing appropriate decision variables adaptively. |
Year | DOI | Venue |
|---|---|---|
2019 | 10.3390/sym11020197 | SYMMETRY-BASEL |
Keywords | Field | DocType |
satisfiability problem,decision variable,restart,duplicate trails | Decision variables,Conflict-Driven Clause Learning,Heuristic,Combinatorics,Adaptive strategies,Existential quantification,Boolean satisfiability problem,Theoretical computer science,Solver,Sort order,Mathematics | Journal |
Volume | Issue | Citations |
11 | 2 | 0 |
PageRank | References | Authors |
0.34 | 2 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Wenjing Chang | 1 | 0 | 1.01 |
| Yang Xu | 2 | 711 | 83.57 |
| Shuwei Chen | 3 | 1 | 2.39 |