Deep Cooperation of CDCL and Local Search for SAT (Extended Abstract)

1 Introduction

The Satisfiability problem (SAT) asks to determine whether a given propositional formula is satisfiable or not. In the SAT problem, propositional formulas are usually presented in Conjunctive Normal Form (CNF), i.e., F = ∧i ∨jℓij. A growing number of problem domains are successfully tackled by SAT solvers, including the electronic design automation (EDA) industry [Silva and Sakallah, 2000], mathematical theorem proving [Heule et al., 2016], AI planning [Kautz and Selman, 1992], spectrum allocation [Newman et al., 2018], among others. Also, SAT solvers are often used as a core component of more complex tools such as solvers for Satisfiability Modulo Theory (SMT), which are indispensable for program analysis and software verification.

*This is an extended abstract of a paper that appeared/won best award at conference SAT 2021.

Conflict driven clause learning (CDCL) is the most popular approach to solving SAT. Since their inception in the mid-90s, CDCL-based SAT solvers have been applied, in many cases with remarkable success, to a number of practical applications. An alternative is local search, which is a main incomplete method biased towards the satisfiable side, and can be more successful on random and hard combinatorial instances [Li and Li, 2012; Cai et al., 2015; Biere et al., 2020]. There have been attempts combining CDCL and local search solvers. However, in previous hybrid solvers, CDCL and local search solvers usually see each other as a black box and the hybrid solver invokes the respective solver according to different situations [Mazure et al., 1998; Habet et al., 2002; Letombe and Marques-Silva, 2008; Balint et al., 2009; Audemard et al., 2010]. This work is devoted to deeper cooperation of CDCL and local search for SAT, where CDCL is the main solver and local search is used as an aiding tool.

We propose three ideas to use local search to help CDCL in different ways. The first idea is a method for plugging a local search solver into a CDCL solver, by extending promising branches to complete assignments (even meeting conflicts) and then calling local search to search for a model. If the local search cannot find a model within a given time limit, the CDCL search process continues as normal from the node where the algorithm enters the non-backtracking phase. Secondly, We propose a rephasing technique as a heuristic to select the value of the branching variable, which mainly relies on the assignments produced by the integrated local search solver. Lastly, We use the variables' conflict frequency, i.e., the frequency appearing in unsatisfied clauses during local search, to enhance the branching heuristic in CDCL.

We apply our techniques to three state-of-the-art CDCL solvers, including glucose [Audemard and Simon, 2009], and the winner of the Main track of SAT Competition 2019 and 2020 namely MapleLCMDistChronoBT-DL [Kochemazov et al., 2019] and Kissat sat [Biere et al., 2020]. The results show that our techniques allow them to solve a remarkable number of additional instances in the benchmarks of SAT Competition 2017-2020. The integration of our techniques allow the three CDCL solvers to solve 62, 67 and 10 more instances in the benchmark of SAT Competition 2020. Besides, the improved version of the three CDCL solvers shows better results on a benchmark arising from a spectrum repacking problem.

The relaxed CDCL and local search rephasing techniques are very helpful for satisfiable instances, with slight degradation on unsatisfiable instances (usually solving 2 or 3 fewer unsatisfiable instances). The conflict frequency technique can be positive to satisfiable and also saves back a few unsatisfiable instances. Overall, these techniques significantly improve the performance of the CDCL solvers, leading to a remarkable increase on the number of solved instances.

2 Preliminaries

2.1 Preliminary Definitions and Notations

A mapping α : V → {0, 1} is called an assignment. If α maps all variables to a Boolean value, it is a complete assignment; otherwise, it is a partial assignment. The size of an assignment α, denoted as |α|, is the number of assigned variables in it. The value of a variable x under an assignment α is denoted as α[x]. An assignment α satisfies a clause iff at least one literal evaluates to true under α, and satisfies a CNF formula iff it satisfies all its clauses.

A clause that contains exactly one single (unassigned) literal is called a unit clause. A key procedure in CDCL solvers is unit propagation. For a unit clause, the variable is assigned to satisfy this unit clause, and then the formula is simplified according to this setting. The iterative execution of such steps until no more unit clause remains is called unit propagation.

2.2 CDCL Solvers

A CDCL solver performs a backtracking search (can be nonchronological) in the space of partial assignments. Each node of the tree corresponds to a partial assignment, and the out edges represent the two branching value (aka. phase) . Each leaf corresponds to a complete assignment. CDCL solvers can prune a large part of the tree thanks to reasoning techniques. A branch is a path from the root to an inner node. In this work, we use α longeste to denote the largest conflictfree assignment that has been encountered by the solver so far.

Algorithm 1shows the standard procedure of a CDCL solver, where α is the current assignment, dl is the current decision level and bl denotes the backtrack level. Arguments to the functions are assumed to be passed by reference, and thus F and α are supposed to be modified during the search. The functions are explained here. PickBranchVar consists of selecting a variable to assign and the respective phase. UnitPropagation performs unit propagation on the formula, and if a conflict is identified, then a conflict indication is returned. Once a conflict is derived, the reasons are analyzed and a clause is learnt (known as learnt conflict clause) and then added to the clause database. Finally, BackTrack backtracks to the decision level computed by ConflictAnalysis.

Two popular branching heuristics that are used to pick the branching variable include Variable State Independent Decaying Sum (VSIDS) [Moskewicz et al., 2001] and Learn-

Algorithm 1: Typical CDCL algorithm: CDCL(F, α) 1 dl ← 0; //decision level 2 if UnitPropagate(F,α)==CONFLICT then return UNSAT; 3 while ∃ unassigned variables do 4 (x, v) ← P ickBranchV ar(F, α); 5 dl ← dl +1; 6 α←α∪ {(x, v)}; 7 if UnitPropagate(F ,α)==CONFLICT then 8 bl ← Conf lictAnalysis(F, α); 9 if bl < 0 then 10 return UNSAT; 11 else 12 BackTrack(F, α, bl); 13 dl ← bl; 14 return SAT;

ing Rate Branching (LRB) [Liang et al., 2016]. In VSIDS [Moskewicz et al., 2001], each variable has an activity, and VSIDS picks the variable with the maximum activity. Every time a variable occurs in a conflict clause, its activity is increased (aka bumped). After the conflict, the activity of all the variables in the system are multiplied by a constant less than 1, thus decaying the activity of variables over time. LRB frames branching as an optimization problem that picks a variable to maximize a metric called learning rate. The learning rate of a variable x at interval I is defined as P(x,I) L(I) , where I is the interval of time between the assignment of x until x transitions back to being unassigned, P(x, I) is the number of learnt clauses x participates in interval I, and L(I) is the number of learnt clauses generated in interval I.

2.3 Local Search Solvers

For local search algorithms, we need to define the search space and a neighborhood relation. In the context of SAT, the search space is the set of complete assignments which can be characterized as the set of strings {0, 1}n , where n is the number of variables in the formula. For SAT, the seemingly most natural neighborhood N maps candidate solutions to their set of Hamming neighbors, i.e., candidate solutions that differ in exactly one variable. A local search algorithm starts from a position of search space and then moves to one neighbor of the current position in each step, trying to find a position which represents a satisfying assignment.

2.4 Experiment Preliminaries

Base Solvers. We choose three state of the art CDCL solvers as the base solvers for our studies, including glucose (v4.2.1) [Audemard and Simon, 2009], MapleLCMDistChronoBT-DL (v2.1) [Kochemazov et al., 2019], and Kissat sat (2414b6d) [Biere et al., 2020]. Glucose is a milestone of modern CDCL solvers and has won several gold medals in SAT Competitions. MapleLCMDistChronoBT-DL won the SAT Race 2019 and Kissat sat won the Main Track of SAT Competition 2020.

We choose CCAnr [Cai et al., 2015] as the local search solver to integrate into the CDCL solvers glucose and MapleLCMDistChronoBT-DL, whileKissat sat itself already includes a local search solver YalSAT [Biere, 2014]. CCAnr has shown competitive results on various structured instances from SAT competitions and applications.

Benchmarks. Besides the benchmarks of the latest four SAT Competitions/Race (2017-2020), we include a benchmark suite consisted of 10000 instances from the spectrum repacking [Newman et al., 2018].

Experiment Setup. Experimentswere conducted on a cluster of computers with Intel Xeon Platinum 8153 @2.00GHz CPUs and 1024G RAM under the operating system CentOS 7.7.1908. For each instance, each solver was performed one run, with a cutoff time of 5000 CPU seconds. For each solver for each benchmark, we report the number of solved SAT/UNSAT instances and total solved instances, denoted as '#SAT', '#UNSAT' and '#Solved', and penalized run time 'PAR2' (as in SAT Competitions), where the run time of a failed run is penalized as twice the cutoff time.

3 Exploring Promising Branches

In CDCL, some promising branches that are close to a satisfying assignment are also pruned without any exploitation. This would make CDCL solvers miss some opportunities of finding a solution. The exploration on promising branches may improve CDCL solvers on satisfiable formulas, and a natural way to do so is to employ local search at such branches.

We present a method to explore promising branches in CDCL solvers, which can improve the ability to find solutions while keeping the completeness of the solvers. For this method, we need to identify which branches (i.e., partial assignments) deserve exploration. We propose two conditions below, and any assignment α satisfying at least one of them is considered as promising and will be explored:

• |α| |V | > p and there is no conflict under α, where p is a parameter and is set to 0.4 according to preliminary experiments on a random sample of instances from recent SCs.
• |α| |α longest| > q and there is no conflict under α, where q is set to 0.9 similarly.

In order to ensure that the search space of adjacent local search calls is sufficiently different, we disallow local search for a certain number of k restarts, where k is set to 500 for glucose, and 400 for Maple.

During the search of CDCL, whenever reaching a promising branch, the algorithm enters a non-backtracking mode, which uses unit propagation and heuristics in CDCL to assign the remaining variables without backtracking, even an empty clause is detected. At the end, this leads to a complete assignment β, which is fed to a local search solver to search for a model nearby. If the local search fails to find a model within a certain time budget (reaching 5 × 107 memory accesses), then the algorithm goes back to the normal CDCL search from the node where it was interrupted.

https://www.cs.ubc.ca/labs/beta/www-projects/SATFC/ cacm cnfs.tar.gz

4 Rephasing with Local Search

Now, we propose an rephasing heuristic to import back an improved assignments obtained by the local search process, which is referred to as local-search rephasing (LS rephasing for short).

After each time the CDCL solver is restarted, the technique overwrites the saved phases of all variables with assignments produced by local search. When we say the assignment of a local search procedure, we refer to the best assignment (with fewest unsatisfied clauses) in this procedure.

For our phase resetting technique, we consider the following assignments, all of which come from the assignments of the local search procedures.

• α longest LS: the assignment of the local search procedure in which the initial solution is extended based on α longest.
• α latest LS: the assignment of the latest local search procedure.
• α best LS: the best assignment (with the fewest unsatisfied clauses) among all local search procedures so far.

It is easy to see that α longest LS and α best LS serve for the aim to maximize the depth of the branch, while α latest LS adds diversification, as different local search procedures start with initial assignments built upon different branches. Whenever the CDCL is restarted, we reset all variables with one complete assignment which is selected according to the rephasing probabilities given in Table 1. Such changes are always allowed, because they do not impact the underlying CDCL calculus, its correctness, nor termination.

5 Branching with Conflict Frequency

CDCL is a powerful framework owing largely to the utilization of the conflict information, and branching strategies aim to promote conflicts. Intuitively, both VSIDS and LRB prefer to pick variables with higher frequencies occurring in conflicts, with an emphasis in a recent period. We propose to enhance the branching strategy by utilizing the conflict frequency of variables in the latest local search procedure.

In a local search process, for a variable x, its conflict frequency, ls confl freq(x), is defined as the number of steps in which it appears in at least one unsatisfied clause divided by the total number of steps of the local search process.

For each variable x, we multiply ls confl freq(x) with a constant integer (100 in this work), and the resulting number is denoted as ls conflict num(x). We use ls conflict num(x) to enhance the branching strategies as follows. Note that ls conflict num(x) is calculated according to the latest local search procedure. After each restart of the CDCL solver, ls conflict num(x) is used to modify the activity score for VSIDS and learning rate for LRB.

• VSIDS: for each variable x, its activity score is increased by ls conflict num(x).
• LRB: for each variable x, the number of learnt clause during its period I is increased by ls conflict num(x). That is, both P(x, I) and L(I) are increased by ls conflict num(x).

6 Experiment Results

For glucose and MapleLCMDistChronoBT-DL-v2.1, we implement all the three techniques, including relaxed CDCL (denoted as rx), LS rephasing (denoted as rp) and conflict frequency (denoted as cf). For Kissat sat, we only implement the cf technique. All the source codes and experiment statistics can be downloaded online.

Evaluations on Benchmarks of SAT Competitions (Table 2). By implementing all the three techniques, very large improvements are obtained for glucose and MapleLCMDistChronoBT-DL-v2.1 for all the benchmarks. Particularly, glucose+rx+rp+cf solves 62 additional instances than the original solver, and Maple-DL+rx+rp+cf solves 67 additional instances than its original solver for the SC2020 benchmark (which has 400 instances). Maple-DL+rx+rp+cf is a simplified and optimized version of our solver Relaxed LCMDCBDL newTech which won the gold medal of Main Track SAT category and the silver medal of the Main Track ALL category in SC 2020.

Evaluations on Spectrum Repacking (Table3). For each CDCL solver, the improved version with our techniques has better performance than the base solver. Maple+rx+rp+cf solves the most instances (8759+218=8977), significantly better than all the other solvers.

FurtherAnalyses on theCooperation. We can see that the local search solver returns a solution for some instances. A natural question is: Whether the improvements come mainly from the complementation of CDCL and local search solvers that they solve different instances? To answer this question, we compare the instances solved by the hybrid solvers with those by the base CDCL solver and the local search solver. We observe that, there is a large number of instances that both CDCL and local search solvers fail to solve but can be solved by the hybrid solvers. For glucose, this number reaches 29, 36, 26 and 37 for the four benchmarks respectively, while for MapleLCMDIstChronoBT-DL, this number reaches 16, 18, 15 and 36 respectively. This indicates the cooperation techniques have essential contributions to the good performance of the hybrid solvers.

https://github.com/caiswgroup/relaxed-sat

The number of local search calls is usually from 10 to 25 for these benchmarks. The portion of the time spent on local search is between 6% and 20% for satisfiable instances, and usually less than 7% for UNSAT instances.

7 Conclusions

This work took a large step towards deep cooperation of CDCL and local search. We proposed three techniques for using local search to improve CDCL solvers.

This is the first time that the combination of stochastic search and systematic search techniques leads to essential improvements over the state of the art of both approaches on application benchmarks, thus answering Challenge 7 of the Ten Challenges in Propositional Reasoning and Search [Selman et al., 1997].

Acknowledgements

This work is supported by NSFC Grant 62122078, Beijing Academy of Artificial Intelligence (BAAI).