Fast Blocked Clause Decomposition with High Quality

Any CNF formula can be decomposed two blocked subsets such that both can be solved by BCE (Blocked Clause Elimination). To make the decomposition more useful, one hopes to have the decomposition as unbalanced as possible. It is often time consuming to achieve this goal, since it has been proven to be NP-hard. So far there have been several decomposition and post-processing algorithms such as PureDecompose, QuickDecompose, EagerMover etc. We found that these existing algorithms are often either inefficient or low-quality decomposition. To build an efficient and high-quality algorithm, we improve the existing BCE, and present two new variants of PureDecompose, a new heuristic decomposition called LessInterfereDecompose, and a new post-processing algorithm called RsetGuidedDecompose. Combining these new techniques results in a new algorithm called MixDecompose. In our experiments, there is no application formula where the quality of PureDecompose+EagerMover is better than MixDecompose. In terms of speed, MixDecompose is also very fast. Our average runtime is a little longer, but the worst-case runtime is shorter. In theory, our two variants of PureDecompose requires linear time in the number of clauses. By limiting the size of the touch list used by BCE, we can guarantee always that MixDecompose runs in linear time.


Introduction
Recently, one found that blocked clause decomposition can not only efficiently find backbone variables [1] and implied binary equivalences through SAT sweeping, but also improve the performance of the state-of-the-art SAT solvers such as Lingeling [2] on hard application benchmarks [3,4]. Due to its importance, many researchers have been attracted to pay attention to this subject.
A set of clauses is said to a blocked set if it can be removed it completely by Blocked Clause Elimination (BCE) [5,6]. Any CNF formula can be decomposed into two blocked subsets. To make a blocked clause decomposition more useful, one wants always to have two blocked subsets as unbalanced as possible. The problem is that it is not easy to find the most unbalanced subsets. In theory, one has proven that finding a maximal blocked subset of a CNF formula with the largest cardinality (MaxBS for short) is NP-hard [3]. In other words, it is impossible to find the best decomposition in polynomial time unless P = N P . So far a few decomposition algorithms were proposed. However, no algorithm achieves optimization in all terms. PureDecompose [3] is the fastest, but its quality is poor. To improve the quality, Heule et al [3] presented QuickDecompose. However, QuickDecompose is time-consuming. Soon after, to improve the speed, Balyo et al [4] developed a post-processing algorithm called EagerMover. Through a exhaustive series of experiments, we noted that although the decomposition quality of PureDecompose+EagerMover (PureEager for short) and QuickDecompose can outperform PureDecompose, their quality is not high yet.
This paper aims to present an algorithm for finding efficiently a high-quality decomposition. To achieve this goal, we present two new variants of PureDecompose, a new decomposition algorithm based on clause correlation degree, and a new post-processing algorithm. In addition, we improve the existing BCE to speed up the decomposition. The algorithm resulting from integrating these new techniques is called MixDecompose, which can improve significantly the quality of decomposition. On application instances, the decomposition quality of MixDecompose is better than that of PureEager. there is no application formula where the quality of PureEager is better than MixDecompose. In terms of speed, MixDecompose is still fast. On average, it took 8.97 seconds on our machine, which is a little slower than PureEager took 7.41 seconds. However, in the worst case, MixDecompose was faster than PureEager. The latter exceeded 300 seconds in some cases, whereas the former took at most 110 seconds.

Preliminaries
In this section, we present basic concepts that will be used in subsequent algorithms for blocked clause decomposition.
CNF. It is short for conjunctive normal form. A formula in CNF is formulated as a conjunction of clauses, where each clause is a disjunction of literals, each literal being either a Boolean variable or its negation. The negation of a variable x is denoted byx or ¬x. In general, a clause C is written as is a clause. The symbols var(F ) and lit(F ) denote the sets of variables and literals occurring in a formula F , respectively.
Resolution. Given two clauses C 1 = (l ∨ a 1 ∨ · · · ∨ a m ) and C 2 = (l ∨ b 1 ∨ · · · b n ), the clause C = (l ∨ a 1 ∨ · · · ∨ a m ∨ b 1 ∨ · · · b n ) is called the resolvent of C 1 and C 2 on the literal l, which is denoted by Blocked Clauses.Given a CNF formula F , a clause C, a literal l ∈ C is said to block C w.r.t. F if (i) C is a tautology w.r.t. l, or (ii) for each clause C ′ ∈ F withl ∈ C ′ , C ′ ⊗ l C is a tautology. A clause is a tautology if it contains both x andx for some variable x. When l blocks C w.r.t. F , the literal l and the clause C are called a blocking literal and a blocked clause, respectively. BCE. It is short for blocked clause elimination, which removes blocked clauses from CNF formulas. By BCE(F ) we mean the CNF formula resulting from repeating the following operation until fixpoint: If there is a blocked clause C ∈ F w.r.t. F , let F := F − {C}. It is said that BCE can solve a formula F if and only if BCE(F ) = ∅. The seminal work in BCE is due to Kullmmann [5].

Blocked Clause Decomposition
In theory, any CNF formula can be decomposed into two blocked subsets. However, not all the decompositions are effective. In general, The larger one of the blocked sets is, the better the decomposition quality is, since the larger it is, the more it resembles the original formula. Therefore, the size difference of the two sets is considered as a measure of the decomposition quality. Nevertheless, computing the largest blocked set from a CNF formula is NP-hard. Hence, we here aim to find a fast decomposition with higher quality, rather than the highest quality.
The simplest decomposition way is called pure decomposition, which is shown in Fig. 1. Let the symbols L and R denote the left (large) subset and the right (remainder ) subset, respectively. For each variable x, this algorithm adds always the larger of F x and Fx to L and the smaller to R, where F x (Fx) is the set of clauses of F where x occurs positively (negatively). At the termination of this algorithm, we have F = L ∪ R with |L| ≥ |R|. In Fig. 1, max{F x , Fx} means the set with the larger cardinality between F x and Fx.  The advantage of this algorithm is that it can be easily implemented to run in linear time in the size of F , using a standard structure of occurrence lists. Therefore it is very fast. The drawback is that its decomposition quality is not high on many formulas. For this reason, we will improve it by combining some variants of it and the other algorithms.
By a few empirical observations, we found that the performance of PureDecompose rely significantly on the order in which variables are eliminated. Here, we present two variants of PureDecompose with different variable elimination ordering heuristics. The first variant is called min pure decomposition, which is shown in Fig. 2. One fifth of variable eliminations are to be eliminated in the same order as PureDecompose. The remaining variables are to be eliminated in order from the lowest occurrence of literals to the highest. If there are multiple literals with the lowest occurrence, the literal with the minimum total number of clauses containing it is eliminated first. The total clause size of a literal x can be formulated as C∈Fx |C|. Compared to PureDecompose, this algorithm adds only the search of variables to be eliminated. This search can be done in O(n log n) time, using an order heap, where n is the number of variables. In the actual implementation, the number of variables in min x∈lit(F ) |F x | is limited to 30000. This can guarantee that MinPureDecompose is still very fast even if n is very large. In terms of decomposition quality, this algorithm is superior to the other algorithms on some application instances such as ctl 4291 567 5 unsat pre. Now we consider the second variant of PureDecompose. The order of its variable eliminations is opposite to that of the first variant. We call this variant max pure decomposition, which is shown in Fig. 3. It always eliminate first a literal with the highest occurrence. When multiple literals have the same highest occurrence, we select a variable with the lowest different of its two literal occurrences. This can be done by computing min |Fx|=m ||F x | − |Fx||, where m is defined as max x∈lit(F ) |F x |. Actually, the first variant can introduce also this tie-break method. Unlike the first variant, MaxPureDecompose needn't compute the total clause size of each literal. So it should run faster than the first variant. In order to ensure that is still very fast even if the number of variables is very large, the range for finding a literal with the highest occurrence is limited to 5000 variables. The decomposition quality of this algorithm is superior to that of the other algorithms on some application instances such as complete-500. The above two algorithms both are based on the order of variable elimination. However, in some cases, the algorithm obtained by optimizing the order of variable elimination is not necessarily optimal. Therefore, one must find more efficient algorithms to replace them. Blow we present a new algorithm called less interfere decomposition, which is based on the order of clause elimination. Its pseudo-code is shown in Fig. 5. This algorithm may sketch the basic outline as follows: move blocked clauses in F to L by BCE, compute the candidate set S, move each clause C ∈ S ∩ F to R. These steps are repeated until F is empty. The computation of the candidate set S is based on the notion of interfering degree. The interfering degree of a clause C can be defined as ogy clause, and one otherwise. The probability that C ′ ⊗ l C is not a tautology clause is very high. To save the computing cost, we may approximate the interfering degree as Fig. 5 uses this approximation version to compute the interfering degree, and call this measure score, i.e., score[C] = C ′ ∈F |var(C ′ ) ∩ var(C)|. To get clauses with the maximum score, all the clauses in F are traversed. If only one clause with the maximum score is moved to R from F each time F is traversed, it is time consuming. So we decide to move p clauses to R one time, where p = |F | θ , where θ is a constant. In our experiment, when |F | < 8 × 10 4 , θ is set to 2300. Otherwise, θ is set to 400 for random instances, and 100 for non-random instances. When |F | θ < 18, p is set to 18. As shown in Fig. 5, the clauses with the first p highest scores are stored in S as the candidate clauses to be moved to R. In order to save time further, we compute the interfering degree produced by only literals with the lowest occurrence, not all literals.
LessInterfereDecompose calls to BCE shown in Fig. 4 to move blocked clauses to L. BCE here is different from that presented in [6]. BCE in [6] is based on a literal-based priority queue, while our BCE is based on a clause-based linear linked list. Another important difference from the usual BCE is that we do not try to test whether each literal l in C is a blocking literal when |F | ≥ 200000. We test only literal l with |Fl| < 2. That is, we replace the statement " for l ∈ C do " in the usual BCE with the statement " for l ∈ C with (|Fl| < 2 or |F | < 200000) do". Due to this simplification, our BCE is much faster than the usual BCE. Surprisingly, the decomposition quality keep unchanged in most cases. Even if it is changed, its change is still very small. In addition, our touch function is different from that in [6]. Here is our definition about it.
Fx otherwise When |F | ≥ 600000, we consider only the clauses touched by the negation of literals with the number of occurrences < 2. This can speed up the decomposition of large instances. For example, using the above touch, the runtime of decomposing on q query 3 L90 can be reduced from 600 seconds to 9 seconds. The decomposition quality keep unchanged still. The runtime of LessInterfereDecompose consists of three parts: BCE, computing scores and determining S's. The runtime of computing scores is O( |F | 2 p ) = O(θ|F |). If scores are given, determining a S can be done in a linear time in |F |, since there exist linear time algorithms for finding the p-th highest score [7,8]. The total runtime of computing scores plus determining S's does not exceed O(θ|F |). If the number of clauses touched by each clause does not exceed a constant δ, where δ is certainly smaller than the maximal number of literal occurrences times the maximal size of clauses, i.e., max x∈lit(F ) |F x | × max C∈F |C|. The total time required by all BCE 's is at most O(δ|F |). Thus, the total runtime of LessInterfereDecompose is at most O((δ + θ)|F |). In practice, δ is generally very small. Should δ is very large, we can remove a part of touched clauses to reduce the time required by BCE to test whether a clause in the touch list is blocked, or limit the size of the touch list a small constant, say 2000. Using such a policy can guarantee that the time complexity of LessInterfereDecompose is linear in |F |. Compared with EagerMover in [4], the runtime of BCE in LessIn-terfereDecompose is smaller than that in EagerMover. EagerMover calls at least four times BCE on a subset with the size of 0.75|F |. All calls to BCE on each clause C in F can be viewed as a call to BCE on the whole F . Thus, the total runtime of BCE in LessInterfereDecompose corresponds to double the runtime of BCE on a F . As long as the runtime of computing scores and determining S's is smaller than the runtime of BCE on a F , LessInterfereDecompose should be faster than EagerMover. In fact, that is true. On some instances, the former are indeed faster than the latter.
In general, the above algorithms do not achieve maximal blocked set decomposition. However, they can be improved further by post-processing. The postprocessing often used is MoveBlockedClasue algorithm shown in Fig. 7, which is to move blocked (with respect to the current L) clauses from R to L. We noted that even if this post-processing algorithm is applied, the decomposition quality can be improved still. For this reason, we present a new post-processing algorithm, called Right set guided decomposition, which is shown in Fig. 6. It is a simplified version of LessInterfereDecompose. Replacing S with R results in this algorithm. This algorithm requires that the right blocked set R must be given in advance. Hence, it is used generally as post-processing. It is faster than LessIn-terfereDecompose, since it need not computing R. Its time complexity depends mainly on that of BCE. For some benchmarks, this algorithm can improve significantly their decomposition quality. For example, to decompose SAT dat.k75-24 1 rule 3 using MinPureDecompose, the fractions of the large subset (i.e., |L| |F | ) with RsetGuidedDecompose and without it are 83.9% and 69.9%, respectively. If replacing MinPureDecompose with LessInterfereDecompose, their fractions are 87.8% and 87.3%, respectively. RsetGuidedDecompose raises still the quality by 0.5%. However, the speed difference among the three algorithms is big. On this instance, LessInterfereDecompose, RsetGuidedDecompose and MinPureDecompose spent 25, 4 and 1 seconds, respectively. The slowest LessInterfereDecompose is not suitable for huge instances with ten millions of clauses. In general, we do not know which algorithm is the best. Because each of the previous three algorithms is very fast, running the three algorithms one after another does not lose much time. Thus, we can construct an algorithm with high speed and high performance by combining the algorithms above-mentioned. The detailed implementation is shown in Fig. 7. We call this algorithm MixDecom-pose. Its basic idea is to take the maximum from three left sets outputted by three algorithms as the initial L first. If the formula to be decomposition is not large, say the number of clauses is less than 5 × 10 6 , we invoke LessInterfereDecompose to get a larger L. Finally, we enlarge the size of L by calling two post-processing algorithms: RsetGuidedDecompose and MoveBlockedClasue. Like the usual postprocessing, the task of MoveBlockedClasue is to move blocked clauses from R to L. Notice, if F is large, say |F | > 10 7 , the last post-processing can be canceled to save the running time. According to whether both subsets can be solved by BCE, a blocked clause decomposition can be classified as symmetric or asymmetric. If yes, it is symmetric. If only one of the subsets can be solved by BCE, it is asymmetric. Clearly, our two variants of PureDecompose are symmetric. Like EagerMover [4], if blockable clauses (whose definition is given below) are allowed to move to L, RsetGuided-Decompose are asymmetric, since it cannot guarantee that the left set can be solved by BCE. However, by our observation, on almost all application instances, they are symmetric.

Empirical evaluation
We evaluated the performance of decomposition algorithms under the following experimental platform: Intel Core 2 Quad Q6600 CPU with speed of 2.40GHz and 2GB memory.
Because QuickDecompose [3] requires more time than EagerMover [4] for many instances, we decided to select more competitive PureDecompose+EagerMover [9] (PureEager for short) as our comparison object. PureEager and MixDecompose both are written in C.
The large set L obtained by PureEager contains blockable clauses in addition to blocked clauses. A clause C is said to be blockable w.r.t. a blocked set L if each literal l ∈ C is not a blocking literal of any clause in L. The reason why blockable clauses are add to the blocked set is that they do not destroy the blocked property. That is, blocked sets containing blockable clauses are still satisfiable. To keep identical with the performance evaluation of PureEager, the large set L of our MixDecompose contains also blockable clauses. In addition, before calling MixDecompose, we use the same unit decomposition policy given in [4] as EagerMover to preprocess the input formula. We evaluated PureEager and MixDecompose on the 297 instances from the application track of the SAT competition 2014, except for three huge instances. Due to limited space, Table 1 lists only a part of results on the application track and a random instance from the SAT competition 2014 shown in the last row. Column |F | denotes the number of the clauses in formula F in ten thousands of clauses, where F is simplified by removing satisfied clauses, but contains unit clauses. Column |L| |F | indicates the fraction of the large set. Column Time shows the runtime in seconds. As seen in Table 1, in terms of decomposition quality, MixDecompose outperforms completely PureEager. In terms of speed, the former is sometimes faster than the latter, and vice versa. MixDecompose was able to finish the decomposition on all SAT 2014 application benchmarks excluding three huge instances within 110 seconds. However, PureEager was not able to finish on some benchmarks such as 9vliw m 9stage iq3 C1 b7 within 300 seconds.  Table 2 shows the empirical result on 297 benchmarks from SAT Competition 2014 application track. Three huge instances zfcp-2.8-u2-nh, esawn uw3.debugged and post-cbmc-zfcp-2.8-u2 were removed. The second column shows the average fraction of the large set. Column '# of best' indicates the number of the best results obtained by an algorithm. Column '# of eq' is the number of results equivalent to another algorithm. On 226 out of 297 benchmarks, the size of the large set obtained by MixDecompose is larger than that obtained by PureEager. On 71 remaining benchmarks, the quality of the two algorithms is identical. there is no application formula where the quality of PureEager is better than MixDecompose. In addition, we conducted also experiments on random benchmarks. We observed that on all random instances, the quality of MixDecompose is strictly better than that of PureEager. As seen from the last row of Table 2, MixDecompose can solve huge random instances with millions of clauses in a reasonable time. For 3-SAT random instances, it can increase the fraction of the large set by 5%.
The fifth column in Table 2 shows the average runtime taken by each algorithm in seconds. Here, computing the average runtime counts only solved instances, excluding timed-out instances. The last column in Table 2, lists the number of times the time-out was hit. The timeout for each algorithm was set to 300 seconds. MixDecompose did not time out on the tested benchmarks, while PureEager did on 7 benchmarks. MixDecompose took at most 110 seconds. Although on average, PureEager run faster than MixDecompose, in this experiment, the worst-case runtime of the former was significantly lager than the latter.
According to results of four algorithms, MixDecompose outputs the best result among them. For 297 application instances, the number of the best results obtained by LessInterfereDecompose, PureDecompose, MaxPureDecompose and MinPureDecompose are 215, 18, 30 and 34, respectively. This empirical result shows that in most cases, LessInterfereDecompose is superior to the other algorithms.

Conclusions and Future work
In this paper, we developed a new blocked clause decomposition algorithm by combining several decomposition strategies. The new algorithm not only achieves high quality decomposition, but also is fast. Even for large instances, it can ensure that the decomposition is done within 110 seconds on our machine. Because our machine is slower than the platform of SAT competition 2014, If running on the latter, the speed will be more fast.
So far we know only that we can get a higher quality decomposition than the existing algorithms such as PureEager. However, this does not mean that MixDecompose is the best. How to develop a better and more efficient than MixDecompose will be a future research topic.