Learned Clause Minimization in Parallel SAT Solvers

TL;DR

This paper investigates learned clause minimization (LCM) in parallel SAT solvers, revealing that while LCM can improve performance on some instances, it often decreases performance, and only specific approaches are beneficial.

Contribution

The paper introduces multiple LCM approaches for parallel SAT solvers, compares their effectiveness, and analyzes conditions under which LCM improves solver performance.

Findings

LCM boosts performance on a subset of SAT instances

Applying LCM often decreases solver performance

Certain LCM methods can enhance overall parallel SAT solver efficiency

Abstract

Learned clauses minimization (LCM) let to performance improvements of modern SAT solvers especially in solving hard SAT instances. Despite the success of LCM approaches in sequential solvers, they are not widely incorporated in parallel SAT solvers. In this paper we explore the potential of LCM for parallel SAT solvers by defining multiple LCM approaches based on clause vivification, comparing their runtime in different SAT solvers and discussing reasons for performance gains and losses. Results show that LCM only boosts performance of parallel SAT solvers on a fraction of SAT instances. More commonly applying LCM decreases performance. Only certain LCM approaches are able to improve the overall performance of parallel SAT solvers.

Tables

Table 1. Table 1 : Results for main track benchmarks of SAT Competition ’18 (SAT’18), ’17 (SAT’17) and application track of SAT Competition ’16 (SAT’16A) with 15,000 seconds time to solve each of the 1,050 benchmarks.

	SAT’16A			SAT’17			SAT’18			All
Solver	SAT	UNSAT	ALL	SAT	UNSAT	ALL	SAT	UNSAT	ALL	SAT	UNSAT	ALL
Syrup	77	113	190	105	120	225	151	114	265	333	347	680
Syrup-PCM	78	115	193	105	120	225	160	120	280	343	355	698
Syrup-LPCM	77	116	193	104	120	224	150	119	269	331	355	686
Syrup-ECM3	76	122	198	101	126	227	149	119	268	326	367	693
Syrup-ECM4	72	108	180	98	109	207	133	103	236	303	320	623
Sticky	63	93	156	97	109	206	143	105	248	303	307	610
Sticky-LPCM	68	104	172	95	117	212	135	112	247	298	333	631
Sticky-ECM3	66	102	168	97	118	215	133	113	246	296	333	629
TopoSAT2	80	116	196	116	122	238	161	106	267	357	344	701
TopoSAT2-ECM3	75	109	184	119	113	232	159	104	263	353	326	679

Full text

0.1 Introduction

In recent years more modern Conflict-Driven Clause Learning (CDCL) SAT solvers incorporate learned clause minimization (LCM) to increase their overall performance. Despite several clause minimization (CM) approaches used in SAT solvers, LCM mostly refers to vivification [23] of learned clauses, where redundant literals are removed from a clause by unit propagation and conflict analysis. The performance increase results from a more efficient propagation and a higher chance of producing unit clauses due to shortened clauses [19]. The success of LCM in modern SAT solvers is supported by the results of the main track of the SAT Competition’18, where the thirteen highest ranked solvers all use LCM. However, this success seems not to translate directly to parallel SAT solving. The highest ranked LCM solver of the parallel track is ranked third and only a fraction of the track’s participants use LCM at all. Parallel SAT solvers commonly are portfolio solvers, whereby multiple sequential CDCL SAT solver instances run different heuristics in parallel. Each solver instance exports presumably beneficial learned clauses to other instances. Another parallel approach is divide-and-conquer based SAT solving [21, 14, 1, 15], which will not be covered in this paper.

In general, the challenge of incorporating LCM is choosing the trade-off between time spent on CDCL solving and on minimizing clauses. Even in sequential solvers this remains challenging due to the diversity in structure of SAT problems. In parallel solvers this challenge seems to be even greater. Probably, reasoning on a variety of imported beneficial clauses leads to more relevant conflict clauses, which then can be exported again. This creates a leverage effect, whereby spending a significant time on LCM may slow down the overall progress, because most shortened clauses are only used by a fraction of solvers.

In this paper we analyze homogeneous LCM approaches, i.e., every solver instance of a parallel SAT solver uses the same clause minimization approach instead of dedicating a subset of instances to clause minimization. This has two reasons: First, heterogeneous solver structures need to be load balanced [27]. It has to be ensured that all chosen clauses are minimized without stalling any thread, which becomes more difficult with increasing parallelism. Second, successfully minimizing a clause is more likely, when the solver that learned this clause minimizes it. This solver has a higher probability of holding additional conflict clauses that cut similar parts of the search tree.

Our main contributions are:

• •

A general overview of applicable homogeneous LCM approaches in parallel SAT solvers (Section 0.3),

• •

an extended versions of Glucose-Syrup 4.0 implementing the proposed LCM approaches (Section 0.4.1), and

• •

an extensive performance comparison of Glucose implementations and the vivification SAT solvers TopoSAT2 and Sticky (Section 0.4.2).

0.2 Background

In the following, we assume knowledge of fundamental techniques of SAT solving, such as Boolean constraint propagation (BCP), backtracking, clause learning and resolution, as well as basic parallel approaches for SAT solving, especially portfolio solvers with clause sharing. We cover clause minimization approaches only briefly and refer to given references for more details.

Clause minimization is applied either during preprocessing or in-proccessing. Common preprocessing techniques are clause and variable elimination based on SatElite [9]. Thereby, variables are eliminated through resolution [26] and redundant clauses are removed using (self)-subsumption until the given formula cannot be further minimized. This approach is not limited to preprocessing, but the impact is said to be not significant in most cases [7].

Multiple in-proccessing techniques were already proposed. For example, most Minisat [10] based solvers apply recursive clause minimization [25] and binary resolution to remove literals from currently generated conflict clauses. More recently, serial SAT solvers incorporate clause vivification to minimize initial and learned clauses. Vivification is also known as distillation and was first proposed for incremental SAT solving [16, 13] and as preprocessing approach [23]. Later, it was used for in-processing [19], which is the fundamental approach for our analysis of in-processing clause minimization in parallel SAT solvers. Thereby, the negation of each literal of a clause is propagated. During propagation three cases can occur: (1) When a conflict is detected, the resulting conflict clause replaces the original clause. (2) A literal is propagated to true, whereby not yet propagated literals can be removed from the clause. (3) Literals that are non-decisionally propagated to false, can be removed from the clause. In general, vivifications are only independent from the search space, when applied at decision level zero and therefore are only applicable after restarts or complete backtracks. Due to the large overhead of applying unit propagation and the probability that no literal can be removed, vivification is only applied to a subset of clauses. A possible subset are clauses that are most likely to be kept in the near future, i.e., clauses with a low LBD value [2] or activity [5].

Approaches of clause minimization in the context of parallel SAT solving are barely studied. SArtAgnan [17] dedicates one of eight threads to minimize all initial clauses and a subset of learned clause using the SatElite approach. Another approach [27] uses one reducer thread besides a CDCL solver. The reducer performs vivification on learned clauses and communicates successful minimizations to the CDCL solver. Two approaches of the SAT Competition ’18 use a homogeneous approach, where every thread tries to minimize learned clauses. Thereby, ABCDSat applies a variation of vivification to learned clauses with small LBD value and removes redundant clauses by a subsumption check [8]. In contrast, TopoSAT2 vivifies clauses before export [11]. However, no studies on such homogeneous approaches are available and their impact is not evaluated yet. Due to the lack of insights and publications, we are not able to discuss Cryptominisat [24], which also uses vivification during active solving.

0.3 Clause Minimization in Parallel

The basic LCM approach described in the previous section is trivially portable to most modern parallel SAT solvers. However, sharing improvements of clauses is challenging due to redundant clause storage. We describe three homogeneous clause vivification approaches, which target this challenge. In Figure 1 the differences between the approaches are outlined using flowcharts. For comparison, the standard CDCL workflow is given and necessary changes for incorporating each proposed approach are marked in red.

Private Clause Minimization.

Private clause minimization (PCM) resembles the common learned clause minimization [19], whereby only learned clauses are minimized, when they are likely to be kept. In context of parallelism, PCM solvers only minimize clauses that were learned by them, i.e., do not vivify imported clauses. In an early stage of our research we discarded vivification of imported clauses due to two insights we gained: (1) Vivification of imported clauses fail more often, most likely caused by different search spaces of exporting and importing solvers, and (2) the number of kept clauses increases heavily, wherefore the heuristic cut on which clauses are chosen for vivification has to be more restrictive to prevent an imbalance between CDCL solving and LCM. This leads to a worse performance than disabling LCM in most cases. The vivification is always triggered before the clause database is reduced. For example, in Glucose-Syrup it is therefore necessary to delay the clause reduction until the solver reaches level 0 or the current implication graph has to be stashed to be able to apply vivification. Since vivification is triggered independently from the export routine, clause improvements are never exported, when no lazy export policy is used [4].

Linked PCM (LPCM).

To overcome the issue of unshared shortened clauses, each copy of an exported clause is linked by a unique reference in LPCM. Thus, the learning solver can vivify a clause and on success can share the strengthened clause by using the link. For the linked PCM (LPCM) implementation of Syrup we added an atomic pointer to each exported clause that points to a reference counted array containing the new clause. Then, importing solvers can check during clause reduction, whether an improvement of a clause is present. This scheme can be easily applied to most SAT solvers. In contrast, the SAT solver Sticky uses physical clause sharing [27], wherefore such links are already in place, since clauses are not copied during sharing.

Export Clause Minimization.

Instead of sharing a clause’s improvement after the clause was exported, exports can be delayed until the solver is able to vivify the clause, so that only the improved clause is shared. This vivification approach, we call it Export Clause Minimization (ECM), was first proposed and implemented by Ehlers et al. [11] in the solver TopoSAT2. Thereby, it is insufficient to vivify every exported clause, due to a potential high workload on the minimization. Vivification should be restricted by an LBD [12] or size limit. Two theoretical disadvantages occur due to this workflow. First, the export of clauses with good LBD values can be significantly delayed, which can lead to a performance decrease. Second, all clauses with a sufficiently low LBD are vivified, which can lead to a high overhead due to vivification. Our experiments show that ECM should be restricted to clauses with an LBD lower than 4.

0.4 Experimental Results

Optimizing heuristics in parallel SAT solvers is heavily compute-intense. Due to restrictions in compute time, we focus on Glucose based solvers to save initial optimizations on which parameters work well with LCM and ECM.

We implemented PCM, LPCM and ECM in Glucose-Syrup (Syrup) and further compare it to TopoSAT2, which implements ECM, and to our experimental SAT solver Sticky, which implements LPCM and ECM. The benchmarks are taken from the main tracks of the SAT Competition 2018 and 2017 as well as the application track of the SAT Competition 2016. All tests ran on single socket Intel Xeon Phi 7250 with 68 cores at 1.4 GHz clock rate and 96 GB main memory, whereby the MCDRAM was disabled. Due to memory restrictions each solver only uses 34 solver instances in parallel. For each benchmark a time limit of 15,000 seconds was set. The time limit is set three times higher than in the SAT Competition, because of the lower clock rate and the slower memory subsystem of the used hardware. All results and the Syrup implementations are available online111https://github.com/marchartung/glucose4_0_vivi.

0.4.1 Vivification in Syrup

The Syrup extensions are based on the first parallel version 4.0 of Glucose. The VSIDS branching [20] and the dynamic restart [3] heuristics as well as the clause database management are untouched in all extensions. In the PCM implementation vivification is triggered before the clause database is reduced, wherefore reduction may be delayed until the solver restarts. For identifying clauses worth minimizing, all clauses are sorted according to their LBD and activity value and only the half with the lowest LBD values and at most an LBD of 5 or lower are vivified. The solvers only try to vivify a clause once. As mentioned before, minimized clauses are not shared again. LPCM is enabled by reserving extra space for an atomic pointer in each shared clause. When a clause is shared before the solver tried to vivify it, the pointer is set to an array, where the vivified clause is copied to later. Every solver can then check during reduction whether a clause was minimized. The rest of the minimization process of LPCM is equal to PCM. The ECM implementation delays exports of clauses with an LBD lower than 4 (syrup-ECM3) or 5 (syrup-ECM4) until a restart occurs and then vivifies and exports them. These clauses will not be removed before the vivification took place and thus are protected during the database reduction process.

The following factors have to be considered to reason about performance differences between implementations. The two major performance decreasing factors are the slowdown caused by the propagations spend for the clause vivification and the overhead introduced by sharing the clause improvements. Both decreasing factors are only justified, when minimized clauses sufficiently cut the search space or participate in the final proof, i.e., significantly shorten the time to solution.

To estimate the vivification overhead, Figure 2 shows cactus plots of the percentage of propagations spent for vivification of each Syrup implementation on the solved SAT (left) and UNSAT (right) instances. ECM3 spends less than 1 % on propagations for vivification in over 250 SAT instances and in nearly 300 UNSAT benchmarks, which is far less compared to ECM4, where only about 50 SAT and UNSAT instances have such a low vivification overhead. CDCL solvers have a higher chance to generate clauses with a higher LBD and clauses with a higher LBD tend to have more literals. Thus, the increase of vivification overhead from ECM3 to ECM4 is plausible. PCM and LPCM, both spent roughly the same amount of more propagations for vivification than the ECM approaches.

The time spent on vivification is not an indicator for its impact. Even minor clause improvements can significantly improve the solver’s performance. An example for this is the performance decrease from ECM3 to ECM4 in Figure 4, which shows the runtime distribution of the Syrup implementations, whereby an additional zoom plot is given for the range between 50 and 250 solved instances. In the satisfiable and unsatisfiable case, ECM3 is always faster than ECM4 despite seldom but very effective clause minimizations. Also, the percentage of successful shortened clauses over all solved instances is with 6.2 % for ECM3 much lower than for ECM4 with 32.6 %. The impact of vivification depends much more on how often vivified clauses are reused by the solvers. Audemard et al. [4] state that most of the learned clauses participate in one conflict, but only a small percentage appears in multiple conflicts (91 % appear one time, 34 % two times, 22 % three times, 17 % four times). Therefore, vivifying clauses with a high activity is more likely to have a higher impact due to higher probability of reusage. This assumption is substantiated by the results of PCM and LPCM, which prefer vivifying active clauses, where the vivification overhead is larger than in any other approach (both have a success rate of $\approx$39 %), but compared to ECM4 there is an increase in solved instances. Additionally, it is stated by Audemard et al. [4] that on average only 10 % of the imported clauses lead to conflicts in the importing solver. Thus, heavily vivifying export clauses has minor impact for importing solvers, since most of the clauses will not be used.

Regarding the changes in performance through vivification to the default Syrup implementation, ECM4 decreases the number of solved instances and the time to solution for SAT as well as UNSAT instances. As discussed above, the vivification overhead seems to be larger than the vivification impact. Contrary, PCM increases the number of solved instances on SAT and UNSAT, which is visible in Table 1 more clearly, where the number of solved instances of all evaluated vivification solvers are displayed. Thereby, the increase in solved instances (3 additional instances for SAT’16A and 18 for SAT’18) is comparable to the increase of the LCM approach in Glucose [19] (11 additional instances for SAT’14A and 6 for SAT’16A). The additional overhead of LPCM through managing additional resources for linking clauses, seems to cancel out the positive effects of vivification for SAT instances. LPCM solves two fewer SAT instances than the default implementation over all SAT Competitions and does not solve more UNSAT instances than PCM. The same scenario occurs much more clearly, when using ECM3, where 7 fewer SAT instances and 20 more UNSAT instances are solved compared to the default implementation.

Considering the runtime behavior, the default implementation solves 185 SAT instances faster than its PCM implementation and PCM solves only 168 instances faster (see Figure 4(a)). For the UNSAT instances the difference is with 212 to 148 even greater (see Figure 4(b)). But on average this translates only to a runtime increase of less than 2 % over all solved instances. Regarding ECM3, the overall runtime is shortened by $\approx$4 %. In Figure 4(c) and (d) it is visible that this runtime improvement is mostly based on an improved performance in unsatisfiable instances.

0.4.2 Comparison to other SAT solvers

In the following, we compare our Syrup implementations with TopoSAT2 and Sticky. Both solvers incorporate vivification as an additional clause minimization approach, whereby TopoSAT2 uses ECM and Sticky is capable of using ECM or LPCM.

TopoSAT2

has an optional ECM feature similar to our ECM implementation in Glucose. The main difference is that clauses are not protected during reduction. Instead, all clauses with an LBD lower than 4 are copied to an additional buffer and exported after the vivification took place. The disadvantage is that vivified clauses are not updated in the exporting thread’s database. In this configuration TopoSAT2 does not use a lazy clause exchange policy [4] meaning, clauses are directly exported without any additional filter criteria such as times used. TopoSAT2 uses a diversification approach as branching, restart, and database heuristic, where each solver instance uses a different combination of VSIDS or LRB branching [20, 18], dynamic [3], luby [10], or inner-outer restarts [6] and Chanseok Oh [22] or Glucose based clause database management [2]. In our experiments, we use a newer version222available on https://github.com/the-kiel/TopoSAT2 than submitted to the SAT Competition ’18 and reduced the maximum LBD value for vivifying clauses to 3 for better results on the used system.

Sticky

is an experimental SAT solver based on Glucose using physical clause sharing333available on https://github.com/marchartung/sticky. Instead of copying clauses during export, solvers simply share the reference of a clause, which is used by the other solvers to access the clause. Therefore, the watcher scheme of Glucose was adjusted to support such concurrent usage of clauses by ensuring that clauses remain constant during propagation. Each clause contains a reference counter to keep track of the number of solvers allocating the clause and a placeholder for an additional clause reference, in case the clause is replaced. ECM is used in the same way as in our Glucose implementations except that no extra memory for linking the clauses has to be reserved and clauses can be exported directly without delay, since improvements are trivially shared due to physical clause sharing. The LPCM implementation is different from Syrup-LPCM. Sticky does not separate between learned and imported clauses. Thus, vivification is also applied to imported clauses. PCM is not implemented in Sticky, since physical clause sharing would have to be disabled for vivified clauses, which contradicts the main purpose of the solver.

VSIDS is used as branching heuristic in Sticky. Restart and clause management heuristics are combinations of luby or dynamic restart and Chanseok Oh [22] or Glucose based database management [2]. During database reduction, solvers do not distinguish between imported or own clauses, but LPCM is—as described above—only applied to clauses, which were learned by the minimizing solver instance. Sticky uses Glucose’s lazy clause import policy [4] in a relaxed way. Thereby, every clause with an LBD smaller than 4 is directly two-watched. For brevity, we excluded ECM results with a maximal vivification LBD of 4, since they show a similar performance decrease as Syrup-ECM4.

Table 1 shows the number of solved instances of the SAT Competition’16 (application track), ’17 and ’18 (main track) by each solver. TopoSAT2 outperforms the default Syrup implementation in all three competitions. Through incorporating vivification, Syrup is able to solve 2 more instances in the SAT Competition’16 (ECM3), 13 more in ’18 (PCM) and solves over all instances only 3 instances fewer (PCM) than TopoSAT2.

In contrast, the ECM implementation of TopoSAT2 decreases its performance. One reason might be the higher vivification overhead compared to Syrup-ECM3, since TopoSat2 does not use a lazy export policy, wherefore more clauses are vivified and exported. The more likely reason is that vivifications are not visible for the learning solver, which decreases the impact of the vivification process. Sticky increases the number of solved instances through ECM3 and LPCM by around 20 instances, which is the highest increase among all solvers. While the number of solved UNSAT instances raised, the number of SAT instances decreased, which is similar to the behavior of Syrup-LPCM and Syrup-ECM3.

0.5 Conclusion

We described multiple homogeneous and parallel learned clause minimization approaches based on vivification. Each approach was implemented in the state-of-the-art SAT solver Glucose and further tested using SAT problems taken from multiple SAT Competitions. Insights gained from these implementations are backed by other solver implementations. Our main insights are: Applying the basic LCM approach to non-imported clauses (PCM) leads to more solved instances in general. Using LCM for shortening a smaller part of the exported clauses with a small LBD value (ECM) significantly increases the performance on unsatisfiable SAT problems.

Acknowledgment

The compute time was provided by the Norddeutscher Verbund für Hoch- und Höchstleistungsrechnen (HLRN). We thank Gilles Audemard and Laurent Simon for providing the Glucose implementation as well as Thorsten Ehlers for the updated TopoSAT2 implementation.