Name
Abstract | ||
|---|---|---|
The modern SAT solvers usually update score of corresponding variables by increasing a bump value on each conflict. Those values are usually constant, but are independent of decision levels and conflicts. Sometimes, it is more efficient for local conflict optimization but weak in global searching. In this paper, we propose a CRB method (Conflicting Rate Branching), which is a variant of VSIDS but different implementation. The CRB updates the score which integrated with the decision level and conflicts whenever a variable is used in conflict analysis. We integrated CRB with MiniSat solvers and evaluated CRB on instances from the SAT Race 2015. Experimental results show that the proposed strategy can solve more instances than EVSIDS and improve performance for both SAT and UNSAT instances. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1109/ISKE.2017.8258777 | 2017 12th International Conference on Intelligent Systems and Knowledge Engineering (ISKE) |
Keywords | Field | DocType |
Sat problem,Boolean satisfiability problem,Branching heuristic,VSIDS,Conflicting rate | Mathematical optimization,Heuristic,Algorithm design,Intelligent decision support system,Decision level,Computer science,Probability distribution,Conflict analysis,Branching (version control) | Conference |
ISBN | Citations | PageRank |
978-1-5386-1830-1 | 0 | 0.34 |
References | Authors | |
0 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Qingshan Chen | 1 | 1 | 1.38 |
| Yang Xu | 2 | 711 | 83.57 |
| Guanfeng Wu | 3 | 0 | 0.34 |
| Xingxing He | 4 | 84 | 13.90 |