logo

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

More info
  • ReceivedNov 24, 2017
  • AcceptedMar 20, 2018
  • PublishedApr 17, 2019

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 2014SAT 2016SAT 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 220576530479411901709
    #Solved 230 183 157 60171 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 218040230585871974338
    #Solved 226 188 156 60178 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 21706643044636 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 161913229596891502282
    #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 164676029872041481132
    #Solved 266 219 174 59 226944
    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 160392329573071440914
    #Solved 265 223173 60225 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 157059729406011458125
    #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 152202429368241440575
    #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 160987829302961452191
    #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 161294629427131438811
  •   

    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 2014SAT 2016SAT 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 631754792428785588944
    #Solved 242 199 183 77 212913
    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 62823529301164 5530648
    #Solved 246 202 187 82208 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 613489690298035599344
    #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 455290087004084083514
    #Solved 275 230203 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 456087086625534066310
    #Solved 278229 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 43548308611512 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 2014SAT 2016SAT 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 229944
    $\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 17854 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 60225 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 17857 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

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

京ICP备18024590号-1