SCIENCE CHINA Information Sciences, Volume 62, Issue 7: 072103(2019) https://doi.org/10.1007/s11432-017-9467-7

A branching heuristic for SAT solvers based on complete implication graphs

• AcceptedMar 20, 2018
• PublishedApr 17, 2019
Share
Rating

Abstract

The performance of modern conflict-driven clause learning (CDCL) SAT solvers strongly depends on branching heuristics. State-of-the-art branching heuristics, such as variable state independent decaying sum (VSIDS) and learning rate branching (LRB), are computed and maintained by aggregating the occurrences of the variables in conflicts. However, these heuristics are not sufficiently accurate at the beginning of the search because they are based on very few conflicts. We propose the distance branching heuristic, which, given a conflict, constructs a complete implication graph and increments the score of a variable considering the longest distance between the variable and the conflict rather than the simple presence of the variable in the graph. We implemented the proposed distance branching heuristic in Maple_LCM and Glucose-3.0, two of the best CDCL SAT solvers, and used the resulting solvers to solve instances from the application and crafted tracks of the 2014 and 2016 SAT competitions and the main track of the 2017 SAT competition. The empirical results demonstrate that using the proposed distance branching heuristic in the initialization phase of Maple_LCM and Glucose-3.0 solvers improves performance. The Maple_LCM solver with the proposed distance branching heuristic in the initialization phase won the main track of the 2017 SAT competition.

Acknowledgment

This work was partially supported by National Natural Science Foundation of China (Grant Nos. 61370183, 61370184, 61472147), Matrics Platform of the Université de Picardie Jules Verne, and MINECO-FEDER Project RASO (Grant No. TIN2015-71799-C2-1-P).

References

[1] Audemard G, Simon L. Glucose 2.3 in the SAT 2013 competition. In: Proceedings of SAT Competition, 2013. 42--43. Google Scholar

[2] Biere A. Lingeling, Plingeling, Picosat and Precosat at SAT Race 2010. FMV Report Series, Technical Report 10/1, 2010. Google Scholar

[3] Eén N, Sorensson N. An extensible SAT solver. In: Proceedings of SAT, 2003. 502--518. Google Scholar

[4] Marques-Silva J, Sakallah K A. GRASP — a new search algorithm for satisfiability. In: Proceedings of the International Conference on Computer-Aided Design, 1996. 220--227. Google Scholar

[5] Moskewicz M, Madigan C, Zhao Y, et al. Chaff: engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference, 2001. 530--535. Google Scholar

[6] Soos M. CryptoMiniSat v4. In: Proceedings of SAT Competition, 2014. 23. Google Scholar

[7] Marques-Silva J, Lynce I, Malik S. Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability. Washington: IOS Press, 2009. 131--153. Google Scholar

[8] Liang J H, Ganesh V, Poupart P, et al. Exponential recency weighted average branching heuristic for SAT solvers. In: Proceedings of AAAI, 2016. 3434--3440. Google Scholar

[9] Audemard G, Simon L. Predicting learnt clauses quality in modern SAT solvers. In: Proceedings of IJCAI, 2009. 399--404. Google Scholar

[10] Luo M, Li C M, Xiao F, et al. An effective learnt clause minimization approach for CDCL SAT solvers. In: Proceedings of IJCAI, 2017. 703--711. Google Scholar

[11] Xiao F, Luo M, Li C M, et al. MapleLRB LCM, Maple_LCM, Maple_LCM_Dist, MapleLRB_LCMoccRestart and Glucose-3.0+width in SAT Competition 2017. In: Proceedings of SAT Competition, 2017. 22--23. Google Scholar

[12] Audemard G, Simon L. Refining restarts strategies for SAT and UNSAT. In: Proceedings of International Conference on Principles and Practice of Constraint Programming, 2012. 118--126. Google Scholar

[13] Biere A, Fröhlich A. Evaluating CDCL variable scoring schemes. In: Proceedings of SAT, 2015. 405--422. Google Scholar

[14] Goldberg E, Novikov Y. BerkMin: A fast and robust Sat-solver. Discrete Appl Math, 2007, 155: 1549-1561 CrossRef Google Scholar

[15] Jeroslow R G, Wang J. Solving propositional satisfiability problems. Ann Math Artif Intell, 1990, 1: 167-187 CrossRef Google Scholar

[16] Marques-Silva J. The impact of branching heuristics in propositional satisfiability algorithms. In: Proceedings of EPIA, 1999. 850. Google Scholar

[17] Audemard G, Simon L. GLUCOSE: a solver that predicts learnt clauses quality. In: Proceedings of SAT Competition, 2009. 7--8. Google Scholar

[18] Audemard G, Simon L. Glucose in the SAT 2014 competition. In: Proceedings of SAT Competition, 2014. 31--32. Google Scholar

[19] Liang J H, Ganesh V, Poupart P, et al. Learning rate based branching heuristic for SAT solvers. In: Proceedings of SAT, 2016. 123--140. Google Scholar

[20] Liang J H, Oh C, Ganesh V, et al. MapleCOMSPS, MapleCOMSPS LRB, MapleCOMSPS CHB. In: Proceedings of SAT Competition, 2016. 52--53. Google Scholar

[21] Li C M, Manyà F, Mohamedou N O. Resolution-based lower bounds in MaxSAT. Constraints, 2010, 15: 456-484 CrossRef Google Scholar

[22] Chen J. Minisat blbd. In: Proceedings of SAT Competition, 2014. 45. Google Scholar

[23] Pipatsrisawat K, Darwiche A. A lightweight component caching scheme for satisfiability solvers. In: Proceedings of SAT, 2007. 294--299. Google Scholar

• Figure 1

Complete implication graph implying the empty clause from clause $x_{70}\vee~\neg~x_{24}\vee~\neg~x_{67}$. Numbers in parentheses below vertices represent the longest distance from the vertex to $\Box$.

• Figure 2

Example to illustrate that, when a variable needs more clauses to imply a conflict, it has lower probability of being involved in a future conflict. For simplicity, each vertex represents a positive literal $x_i$ in the implication graph.

• Table 1   Comparison of different implementations of the proposed distance branching heuristic on instances of different SAT competitions with cutoff time of 5000 s for each solver and instance
 2* SAT 2014 SAT 2016 SAT 2017 Total App. Crafted App. Crafted Main Solver #Instances 300 300 300 200 350 1450 #solved 229 180 159 58 179 805 Glucose-3.0 #Sat + #Unsat 102+127 84+96 67+92 5+53 77+102 – Mean time 625 s 848 s 771 s 1644 s 1071 s – Score 2205765 3047941 1901709 – #Solved 230 183 157 60 171 801 Glucose-3.0_shDist($\alpha$) #Sat + #Unsat 103+127 88+95 64+93 8+52 70+101 – $\alpha=\mbox{50000}$ Mean time 686 s 834 s 791 s 1740 s 1078 s – Score 2180402 3058587 1974338 – #Solved 226 188 156 60 178 808 Glucose-3.0_Dist($\alpha$) #Sat + #Unsat 101+125 91+97 64+92 8+52 77+101 – $\alpha=\mbox{50000}$ Mean time 596 s 936 s 751 s 1458 s 990 s – Score 2170664 3044636 1896220 – #Solved 265 218 175 56 219 933 Maple_LCM #Sat + #Unsat 121+144 93+125 74+101 8+48 103+116 – Mean time 1054 s 779 s 1023 s 1619 s 878 s – Score 1619132 2959689 1502282 – #Solved 259 220 170 56 222 927 Maple_LCM_shDist($\alpha$) #Sat + #Unsat 113+146 96+124 72+98 8+48 108+114 – $\alpha=\mbox{50000}$ Mean time 1000 s 808 s 906 s 1664 s 906 s – Score 1646760 2987204 1481132 – #Solved 266 219 174 59 226 944 Maple_LCM_Dist($\alpha$) #Sat + #Unsat 119+147 96+123 72+102 8+51 110+116 – $\alpha=\mbox{10000}$ Mean time 1075 s 767 s 1050 s 1773 s 889 s – Score 1603923 2957307 1440914 – #Solved 265 223 173 60 225 946 Maple_LCM_Dist($\alpha$) #Sat + #Unsat 118+147 98+125 74+99 7+53 109+116 – $\alpha=\mbox{25000}$ Mean time 1028 s 799 s 977 s 1693 s 925 s – Score 1570597 2940601 1458125 – #Solved 272 220 174 58 225 949 Maple_LCM_Dist($\alpha$) #Sat + #Unsat 125+147 96+124 72+102 7+51 109+116 – $\alpha=\mbox{50000}$ Mean time 1012 s 758 s 936 s 1620 s 847 s – Score 1522024 2936824 1440575 – #Solved 263 221 177 56 223 940 Maple_LCM_Dist($\alpha$) #Sat + #Unsat 116+147 97+124 75+102 7+49 109+114 – $\alpha=\mbox{75000}$ Mean time 1040 s 798 s 984 s 1538 s 817 s – Score 1609878 2930296 1452191 – #Solved 259 220 177 56 223 935 Maple_LCM_Dist($\alpha$) #Sat + #Unsat 114+145 95+125 73+104 8+48 107+116 – $\alpha=\mbox{100000}$ Mean time 934 s 732 s 1057 s 1529 s 757 s – Score 1612946 2942713 1438811 –
•

Algorithm 1 computeLongestdistances$(C)$

Require:$C$, a clause in which all literals are falsified by the current partial assignment

for each variable $x$ in $C$

longDist$[x]$ $\leftarrow$ $0$; seen$[x]$ $\leftarrow$ $1$;

end for

for each assigned variable $x$ in the decreasing order of their assigning time

if seen$[x]$ = $1$ then

$R$ $\leftarrow$ reason$[x]$;

if $R$ $\neq$ no_reason then

for each variable $y$ in clause $R$

if $x$ $\neq$ $y$ then

if seen$[y]$ = $0$ then longDist$[y]$ $\leftarrow$ longDist$[x]~+1$, seen$[y]$ $\leftarrow$ $1$;

else if longDist$[y]$ $<$ longDist$[x]~+~1$ then longDist$[y]$ $\leftarrow$ longDist$[x]+1$;

end if

end if

end for

end if

end if

end for

for each assigned variable $x$ such that seen$[x]$ = $1$

seen$[x]$ $\leftarrow$ $0$;

end for

•

Algorithm 2 updatedistanceScore$(C)$

Require:$C$, a clause in which all literals are falsified by the current partial assignment

Call Algorithm 1 to construct the complete implication graph $G$ that falsifies $C$ and compute longDist$[x]$ for each variable $x$ occurring in $G$;

for each variable $x$ occurring in $G$

distAct$[x]~\leftarrow~{\rm~distAct}[x]~+~{\rm~inc}\times~1/{\rm~longDist}[x]$;

end for

${\rm~inc}~\leftarrow~{\rm~inc/dist\_Decay}$;

• Table 2   Comparison of different implementations of the distance branching heuristic on instances of different SAT competitions with a cutoff time of 5 h for each solver and instance
 2* SAT 2014 SAT 2016 SAT 2017 Total App. Crafted App. Crafted Main Solver #Instances 300 300 300 200 350 1450 #Solved 244 199 183 77 208 911 Glucose-3.0 #Sat + #Unsat 108+136 92+107 70+113 7+70 88+120 – Mean time 1311 s 1737 s 1977 s 3131 s 2293 s – Score 6317547 9242878 5588944 – #Solved 242 199 183 77 212 913 Glucose-3.0_shDist($\alpha$) #Sat + #Unsat 109+133 94+105 71+112 8+69 89+123 – $\alpha=\mbox{50000}$ Mean time 1156 s 1400 s 2338 s 3030 s 2654 s – Score 6282352 9301164 5530648 – #Solved 246 202 187 82 208 925 Glucose-3.0_Dist($\alpha$) #Sat + #Unsat 112+134 95+107 72+115 9+73 89+119 – $\alpha=\mbox{50000}$ Mean time 1440 s 1528 s 2449 s 3120 s 2343 s – Score 6134896 9029803 5599344 – #Solved 277 226 202 82 253 1040 Maple_LCM #Sat + #Unsat 127+150 99+127 78+124 11+71 117+136 – Mean time 2332 s 1836 s 2972 s 3952 s 2338 s – Score 4552900 8700408 4083514 – #Solved 275 230 203 82 253 1043 Maple_LCM_shDist($\alpha$) #Sat + #Unsat 125+150 102+128 80+123 10+72 117+136 – $\alpha=\mbox{50000}$ Mean time 2506 s 1964 s 2905 s 4059 s 2270 s – Score 4560870 8662553 4066310 – #Solved 278 229 204 84 254 1049 Maple_LCM_Dist($\alpha$) #Sat + #Unsat 128+150 102+127 79+125 12+72 118+136 – $\alpha=\mbox{50000}$ Mean time 2078 s 1874 s 3096 s 4142 s 2262 s – Score 4354830 8611512 4030548 –
•

Algorithm 3 Solver_Dist($\alpha$): a CDCL SAT solver using the distance branching heuristic for the first $\alpha$ conflicts

dist_Decay $\leftarrow~0.95$; nbConflicts $\leftarrow$ 0;

for each variable $x$

distAct$[x]$ $\leftarrow$ 0;

end for

while true do

cl $\leftarrow$ unitpropagate$()$;

if all literals in cl are falsified then

nbConflicts $\leftarrow$ nbConflicts +1;

if the current decision level is 0 (i.e., there is no decision literal) then

return UNSAT;

end if

if nbConflicts $\leq~\alpha$ then

updatedistanceScore(cl);

end if

Conflict analysis to learn a new clause;

Backtrack to the second highest level in the new learned clause;

else

if nbConflicts $\leq~\alpha$ then

$x~\leftarrow$ the free variable with the greatest distance score distAct$[y]$;

else

$x~\leftarrow$ the free variable selected using the solver's own branching heuristic;

end if

Assign $x$ to true or false based on a polarity heuristic such as phase saving;

end if

end while

• Table 3   Comparison of solvers with complete and partial implication graphs
 2* SAT 2014 SAT 2016 SAT 2017 Total App. Crafted App. Crafted Main Solver #Instances 300 300 300 200 350 1450 Maple_LCM_Dist($\alpha$) #Solved 272 220 174 58 225 949 $\alpha=\mbox{50000}$ #Sat + #Unsat 125+147 96+124 72+102 7+51 109+116 – Complete graph Mean time 1012 s 758 s 936 s 1620 s 847 s 937 s3-7 Maple_LCM_Dist($\alpha$,$k$) #Solved 264 220 173 58 229 944 $\alpha=\mbox{50000}$ #Sat + #Unsat 119+145 95+125 73+100 8+50 114+115 – $k=1$ Mean time 990 s 743 s 872 s 1614 s 863 s – Maple_LCM_Dist($\alpha$,$k$) #Solved 266 219 177 58 223 943 $\alpha=\mbox{50000}$ #Sat + #Unsat 121+145 94+125 76+101 8+50 108+115 – $k=2$ Mean time 1004 s 779 s 1044 s 1633 s 886 s – Maple_LCM_Dist($\alpha$,$k$) #Solved 267 218 178 54 224 941 $\alpha=\mbox{50000}$ #Sat + #Unsat 123+144 94+124 75+103 7+47 109+115 – $k=5$ Mean time 1022 s 758 s 1038 s 1593 s 912 s – Maple_LCM_Dist($\alpha$,$k$) #Solved 265 221 178 60 225 949 $\alpha=\mbox{50000}$ #Sat + #Unsat 122+143 96+125 74+104 9+51 107+118 – $k=10$ Mean time 964 s 731 s 1007 s 1692 s 955 s 962 s Maple_LCM_Dist($\alpha$,$k$) #Solved 258 219 178 57 227 939 $\alpha=\mbox{50000}$ #Sat + #Unsat 114+144 94+125 74+104 7+50 111+116 – $k=15$ Mean time 961 s 775 s 1049 s 1633 s 848 s –

Citations

• 0

Altmetric

Copyright 2020 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有