Reencoding Unique Literal Clauses

The direct encoding of ExactlyOne $({\mathrm{\ell }}_1,\mathrm{\dots },{\mathrm{\ell }}_k)$ splits the constraint into AtLeastOne $({\mathrm{\ell }}_1,\mathrm{\dots },{\mathrm{\ell }}_k)$ and AtMostOne $({\mathrm{\ell }}_1,\mathrm{\dots },{\mathrm{\ell }}_k)$, where the former is just a clause and the latter blocks any pair of these literals from both being true.:

Note that the number of binary clauses is quadratic in $k$.

If the literals ${\mathrm{\ell }}_1,\mathrm{\dots },{\mathrm{\ell }}_k$ do not occur in other clauses, the binary clauses can be omitted while preserving satisfiability. In that case, we call it an implicit ExactlyOne constraint. If all binary clauses are present, we call it an explicit ExactlyOne constraint.

The sequential counter encoding by Sinz [29] facilitates a compact representation of cardinality constraints. The method works for arbitrary cardinality constraints and uses auxiliary variables $s_{i,j}$ expressing that out of the first $i$ literals, exactly $j$ are true. Since we focus on the ExactlyOne constraint, we only use variables with $j=1$ and therefore drop the second index. For this restricted case, the encoding uses the following definitions: $s_i\leftrightarrow (s_{i-1}\vee {\mathrm{\ell }}_i)$ for and $s_1\leftrightarrow {\mathrm{\ell }}_1$. Additionally, to enforce that at most one can be true, the clauses ${\overline{s}}_{i-1}\vee {\overline{\mathrm{\ell }}}_i$ are included for . Finally, at least one of them must be true, which is encoded as follows: ${\overline{s}}_{k-1}\to {\mathrm{\ell }}_k$.

For our reencoding technique, we will replace a clause $({\mathrm{\ell }}_1\vee \mathrm{\cdots }\vee {\mathrm{\ell }}_k)$ if it represents an implicit or explicit ExactlyOne constraint with the sequential counter encoding shown above. Note that the reencoding replaces one clause by roughly $3k$ clauses. However, clauses of the form $({\overline{\mathrm{\ell }}}_i\vee {\overline{\mathrm{\ell }}}_j)$ become redundant and will therefore be removed if present.

The order encoding [31] uses order variables $o_{\le i}$ with to express if one of ${\mathrm{\ell }}_1,\mathrm{\dots },{\mathrm{\ell }}_i$ is true. To state that ${\mathrm{\ell }}_i$ is true using only order variables, $o_{\le i}$ must be true, while $o_{\le i-1}$ must be false. The case for ${\mathrm{\ell }}_1$ is special: ${\mathrm{\ell }}_1$ is true if and only if $o_{\le 1}$ is true. When encoding ExactlyOne, the case ${\mathrm{\ell }}_k$ is also special: ${\mathrm{\ell }}_k$ is true if and only if $o_{\le k+1}$ is false. The order encoding uses the following clauses ${\overline{o}}_{\le i}\vee o_{\le i+1}$ stating that if one of the first $i$ literals is true, then one of the first $i+1$ is true.

The order encoding eliminates the $x_i$ variables by replacing all their occurrences with $o_{\le i}$ variables. More specifically,

• $\mathrm{■}$

  all literals ${\mathrm{\ell }}_1$, ${\overline{\mathrm{\ell }}}_1$, ${\mathrm{\ell }}_k$, and ${\overline{\mathrm{\ell }}}_k$ are replaced by $o_{\le 1}$, ${\overline{o}}_{\le 1}$, ${\overline{o}}_{\le k-1}$, and $o_{\le k-1}$, respectively.

• $\mathrm{■}$

  all literals ${\overline{\mathrm{\ell }}}_i$ with are replaced by $o_{\le i-1}\vee {\overline{o}}_{\le i}$.

• $\mathrm{■}$

  all clauses with literals ${\mathrm{\ell }}_i$ with are duplicated with one copy using ${\overline{o}}_{\le i-1}$ and the other copy using $o_{\le i}$ instead of ${\mathrm{\ell }}_i$.

Transforming the direct encoding of ExactlyOne into the sequential counter encoding is simple: replace the clauses that encode the constraint. The remaining part of the formula is unaltered. Now, observe that transforming from the sequential counter encoding into the order encoding is also easy: eliminate the original variables using variable elimination (also known as DP resolution). To see this, note that the $s_i$ variables of the sequential counter encoding map to the $o_{\le i}$ variables of the order encoding.

The key building block of our reencoding method is the notion of unique literal clauses, which is defined below.

Given a formula $\mathrm{\Gamma }$, the set of ULCs can be computed in linear time in the size of $\mathrm{\Gamma }$ by first computing which literals occur only once in $\mathrm{\Gamma }$ and then determining which clauses only contain such literals.

To maximize the effectiveness of the reencoding, the ULCs should be as large as possible. Also, we want to reencode all ULCs above a size threshold. Since original variables occur positively and negatively in the definition clauses of the sequential counter encoding, reencoding one ULC may break the ULC property of another clause. We achieve both objectives by resolving “clashing” ULCs.

We can extend Lemma 4 to show that if a satisfiable formula is clash-free, then every ULC can be satisfied on a single literal.

In this section, we assume that a formula is clash-free. Any formula that is not clash-free can be easily turned into one by applying the method described in Section 3.2. While all literals are symmetric in the direct encoding, their order matters when performing our reencoding. Since ULCs are clauses, the literals can be permuted in any way to optimize performance. We consider ULCs as sequences of literals in this section. The following example shows that the order of literals in ULCs could impact the effectiveness of our reencoding.

To allow the solver to make good use of the auxiliary variables, we want to order the literals in the ULCs so that the solver can learn more useful short clauses like the one above. This motivates our definition of aligned ULCs.

As we will show in the experimental evaluation, aligning ULCs increases the effectiveness of our reencoding method. Moreover, when formulas are not aligned or unalignable, the reencoding can become ineffective or even harmful to performance.

Whether a formula is alignable is computable in linear time in the size of the formula. We will discuss this in more detail in Section 4. Since we can efficiently determine whether a formula is alignable, we can run this check first and only reencode alignable formulas.

Manthey and Steinke discuss transforming the direct encoding of ExactlyOne constraints [21]. They look for the following pattern: a clause $({\mathrm{\ell }}_1\vee \mathrm{\cdots }\vee {\mathrm{\ell }}_k)$ together with all binary clauses $({\overline{\mathrm{\ell }}}_i\vee {\overline{\mathrm{\ell }}}_j)$ with . Note that they do not require literals ${\mathrm{\ell }}_1,\mathrm{\dots },{\mathrm{\ell }}_k$ to occur uniquely in the formula, in contrast to ULCs. On the other hand, ULCs do not rely on the presence of binary clauses $({\overline{\mathrm{\ell }}}_i\vee {\overline{\mathrm{\ell }}}_j)$. Thus, each method targets a different pattern. The concept of exclusive literal clauses generalizes both methods.

So, a ULC is an XLC in which all literals are unique, while Manthey and Steinke detect XLCs with no unique literals. For the purpose of experiments, it is convenient to consider XLCs that are not ULCs separately, and we call them proper XLCs.

Similar to a ULC, an XLC can be considered an implicit ExactlyOne constraint as all missing binary clauses can be added via blocked clause addition. The notion of a pair of clashing XLCs is the same as for ULCs: the pair contains complementary literals. In contrast to ULCs, it is not the case that resolving two XLCs always results in a new XLC.

The above issue arises when resolving on unique literals. When resolution on a pair of clashing XLCs is restricted to non-unique literals, then the resulting clause will be XLC. However, doing so can be very costly in practice, as many clauses may contain the resolution variable. We observed that there are many formulas from SAT Competitions for which resolving away all pairs of clashing XLCs resulted in an enormous blowup of the formula. For these reasons, we will not resolve clashing XLCs in our experiments, and we apply only the sequential counter encoding in our experiments, without trying to eliminate into the order encoding. Definitions regarding alignment extend straightforwardly to formulas with XLCs.

Modern SAT solvers support proof logging, so the results of each run can be verified [14]. All techniques used in our reencoding technique can be compactly expressed in the DRAT proof system [33]. The first step of our method, described in Section 3.2, makes the formula clash-free. Each step either resolves two ULCs or eliminates a pure literal. Since clauses are sets of literals, one can shuffle the literals around without any proof logging, so aligning is not explicit in the proof.

The reencoding consists of four stages for the sequential counter encoding and an additional fifth stage for the order encoding. We will explain the proof logging procedure for reencoding ULCs. The procedure for XLC is similar but somewhat more complicated.

1. 1.

   Make the ExactlyOne constraint explicit. Before reencoding a ULC $({\mathrm{\ell }}_1\vee \mathrm{\cdots }\vee {\mathrm{\ell }}_k)$, we need all the binary clauses $({\overline{\mathrm{\ell }}}_i\vee {\overline{\mathrm{\ell }}}_j)$ with to be present in the formula. Each of the missing ones can be added using blocked clause addition.

2. 2.

   Add the definitions. Next, we add the definitions of the sequential counter encoding: $s_1\leftrightarrow {\mathrm{\ell }}_1$ and $s_i\leftrightarrow (s_{i-1}\vee {\mathrm{\ell }}_i)$ for . The clauses corresponding to these definitions can be added using blocked clause addition by adding them in increasing order of $i$.

3. 3.

   Express AtMostOne and AtLeastOne. Now, we need to express that exactly one of the ${\mathrm{\ell }}_1,\mathrm{\dots },{\mathrm{\ell }}_k$ literals can be true using the new definitions. For the at-most-one part, the clauses $({\overline{s}}_{i-1}\vee {\overline{\mathrm{\ell }}}_i)$ are included for , while for the at-least-one part we add the clause $(s_{k-1}\vee {\mathrm{\ell }}_k)$. All these clauses have the reverse unit propagation (RUP) property w.r.t. the formula and can be added in arbitrary order [11].

4. 4.

   Remove the original clauses. At this point, we no longer need the original clauses, including the added binary clauses, and we remove them. After the prior step, these clauses become RUP, so deleting them will not introduce additional satisfying assignments.

5. 5.

   Eliminate the original variables. In case of a transformation to the order encoding, we need to apply variable elimination on all the original variables in the direct encoding. When reencoding ULCs, this step will decrease the number of clauses. However, when reencoding XLCs, this step could substantially increase the number of clauses.

The main difference between reencoding ULCs and proper XLCs is the need for careful accounting in the latter case. It may not be allowed to remove some of the original binary clauses.

This section presents a procedure for aligning the XLCs within a formula. This amounts to assigning each literal occurring in an XLC an integer alignment value and then using these values to sort the literals within the XLCs.

To perform alignment, we first construct a graph $G$ where nodes are literals and the graph contains an undirected edge between two literals $\mathrm{\ell }$ and ${\mathrm{\ell }}^{\prime }$ iff $({\overline{\mathrm{\ell }}}^{\prime }\vee \overline{\mathrm{\ell }})\in \mathrm{\Gamma }$ and both $\mathrm{\ell }$ and ${\mathrm{\ell }}^{\prime }$ occur in distinct XLCs. Next, we sort the XLCs from largest to smallest, sort the literals within each individual XLC by the natural ordering, and initialize the alignment of all literals to $0$. Then, for each $C\in XLCs$ and for each $\mathrm{\ell }\in C$: if $\mathrm{\ell }$ is not aligned, $\mathrm{\ell }$ is assigned $alignment+1$ and all unaligned literals in the connected component of $G$ containing $\mathrm{\ell }$ are aligned with $alignment+1$. We increment $alignment$, then continue to the next literal. After aligning all literals in $C$, the clause is sorted based on the alignment values. If any pair of literals in $C$ shares the same alignment value, the problem is said to be unalignable. This will happen if two literals from an XLC occur in the same connected component in $G$. In this case, the literals are sorted lexicographically by alignment and then by natural ordering. If no alignment occurs and the formula is independent (i.e., $G$ is empty), then each clause retains its natural literal ordering.

The alignment procedure uses a linear number of steps to assign alignment values, processing each literal within an XLC once and processing all binary clauses within the formula at most once. There are multiple possible alignments for any set of alignable XLCs. For instance, in Example 14, ${\mathrm{\ell }}_5$ can be placed at the beginning of $C_2$ and the XLCs would still be aligned. Specifically, after assigning each literal an alignment value, those values can then be ordered in some way, and that ordering can be used to sort the clauses. In addition, the alignment procedure will always produce an aligned formula if the formula is alignable. This is the case because our procedure aligns all variables within a connected component before moving on to the next connected component, ensuring that the property in Definition 10 is not violated.

The independent and unalignable problems may also benefit from ordering. For example, the shift1add family benchmarks each contain only a single ULC (after resolving clashing ULCs) and are thus independent, but in experiments we found by accident that different orderings can lead to $10\times$ difference in solving time. Recent work sorts literals in a single cardinality constraint [25], and a similar approach may be beneficial here. Furthermore, for unalignable problems, partial alignment may still be possible. We focus on the alignable case as these benchmarks tend to yield the most positive results, and leave ordering of independent and unalignable formulas for future work.

The left plot of Figure 1 compares solver runtimes on alignable formulas, contrasting our method’s aligned sequential counter encoding against the original encoding (baseline). For alignable formulas, we observe a clear performance improvement with the aligned reencoding, particularly on UNSAT instances. Most UNSAT points lie well below the diagonal, often on the axes, indicating that adopting our method can solve more UNSAT formulas using much less time. The SAT instances exhibit mixed results, but still, our method solves more SAT formulas and has an overall advantage. We have verified all the proofs and satisfying assignments produced by our method on the original formulas in this plot to make sure these speedups are not due to conceptual or implementation errors.

To understand the importance of aligning variables in ULCs, we also evaluated a shuffled reencoding configuration, where the literals in each ULC are randomized (and not aligned) before reencoding. The right plot of Figure 1 compares this configuration against the original encoding on the same set of alignable benchmarks. In stark contrast to the left one, shuffling largely negates the performance gains of our reencoding method. Most points in the plot lie near the diagonal, indicating no change over the baseline. While some formulas experience degraded performance, several satisfiable instances still benefit substantially from the reencoding, even after shuffling. However, the overall outcome is that shuffling offsets the advantage of our reencoding method.

Table 3 shows solver performance on the subset of benchmarks explicitly labeled with “Shuffled” or “Random”. Sequential counter and order encodings with aligned sorting provide significant benefits, notably improving the number of solved UNSAT instances (from 55 solved by the original encoding to 73 with the order encoding). These results confirm the importance and effectiveness of alignment.

Experiments on shuffled alignable formulas demonstrate that when the formulas are not aligned, our method does not consistently provide benefits. We therefore expect the same when our method is applied to independent and unalignable formulas. Figures 2 examine the solver’s performance on these instances, comparing the reencoded formula to the original. In both classes, most UNSAT instances lie close to the diagonal, and SAT instances are spread out, with no clear performance gains observed. The results suggest that reencoding ULCs tends to provide no benefit, occasionally even hurting performance. As mentioned in Section 4, future work on ordering literals in independent and unalignable formulas may yield better results with our reencoding.

Our reencoding method can transform the direct encoding of ExactlyOne constraints to the sequential counter or the order encoding. The only difference between the two is that for the latter, variables from the direct encoding are eliminated using variable elimination. Bounded variable elimination [9], a technique used in all state-of-the-art SAT solvers, eliminates variables if that results in a reduction in the number of clauses. After reencoding ULCs, this is the case for all variables from the direct encoding, so solvers could eliminate them. However, they may not be eliminated because the solver can choose to eliminate some of the order variables instead. After eliminating some order variables, the variables from the direct encoding can no longer be eliminated without increasing the size of the formula.

Figure 3 shows the comparison between the sequential counter encoding and the order encoding on aligned formulas. When we compare the runtime (left), both encodings perform quite similarly. This is even more apparent when comparing the number of conflicts (right). If we only focus on the number of solved benchmarks, then the order encoding solves a couple of extra UNSAT formulas, while the sequential encoding solves a couple of extra SAT formulas. The results suggest that the solver does not always eliminate the original variables in ULCs, and sometimes it is better to keep them.

Figure 4 shows the runtime and conflict comparison between the sequential counter encoding and the order encoding on unalignable and independent formulas. The left plot shows that the sequential counter encoding is noticeably faster than the order encoding. This contrasts with the aligned formulas, where the two methods performed similarly. The right plot suggests that the worse performance of the order encoding is due to slower propagation rather than increased conflicts.

Bounded variable addition (BVA) is a reencoding technique that searches for sets of clauses that can be reencoded to a smaller set of clauses by introducing a new variable [20]. In most cases, BVA will more compactly encode the set of binary clauses. BVA was recently improved by taking the structure of the formula into account during reencoding. This version is known as structured BVA (SBVA) [13]. The combination of SBVA and CaDiCaL won the main track of SAT Competition 2023.

We compared our reencoding method with SBVA as preprocessor for CaDiCaL. The results are shown in Figure 5. Our sequential counter encoding with alignment can solve dozens of alignable formulas that cannot be solved when using SBVA, suggesting that they reencode the formulas differently. Note that a large majority of SAT formulas are below the diagonal, showing that our reencoding works much better on both SAT and UNSAT formulas.

On unalignable and independent formulas, the picture is more mixed. Although most points are below the diagonal, there are more formulas that time out after applying our reencoding while they can be solved when using SBVA.

Table 4 and Figure 6 show the performance of sequential counter encoding on formulas containing proper XLCs. Our reencoding consistently helps solve UNSAT formulas while making SAT formulas slower to solve. The impact of the reencoding is not as significant as on formulas containing only ULCs, especially when looking at alignable formulas. XLC reencoding solved two more UNSAT instances (134 vs. 132) but one fewer SAT instance (118 vs. 119), with a modest reduction in average UNSAT solving time (PAR2 reduced from 723 to 525), and a slight increase in average SAT solving time (PAR2 increased from 318 to 397).

Although the improvement is small compared with reencoding the ULCs in alignable formulas, reencoding XLCs still provides an overall performance gain. Moreover, the performance is consistent across alignable, independent, and unalignable formulas. Reencoding XLCs always helps solve a couple more UNSAT formulas, even on independent and unalignable formulas. This was not the case when reencoding the formulas with only ULCs, as our reencoding generally slightly hurts performance on non-alignable formulas.

We briefly describe some specific families of alignable formulas that our method for reencoding ULCs drastically improves solver performance on.

• $\mathrm{■}$

  Pigeonhole Pigeonhole formulas try to put $n$ pigeons into $m$ holes, consisting of many ULCs (every pigeon must be in one hole). It is one of the famous problems that is easy for humans and hard for SAT solvers, and reencoding ULCs really helps. For example, both the original encoding and SBVA timed out on the formula php-018-014.shuffled, which is a shuffled formula that tries to put 18 pigeons in 14 holes, while after reencoding it was solved in 192 seconds. Similar speed boosts were found in related families, such as relativized pigeonhole formulas.

• $\mathrm{■}$

  Graph Coloring Another family is graph coloring, also having many ULCs (every vertex has one color). Our method works remarkably well on them. For example, our method solved queen14_14.col.14[15] in 9 seconds and le450_15b.col.15 in 28 seconds, while SBVA and original encoding timed out on both of them.

• $\mathrm{■}$

  FPGA-routing These formulas are Field-Programmable Gate Arrays routing constraints encoded as large SAT problems, in which satisfying assignments correspond to feasible routing solutions. The ULCs in these formulas encode connectivity constraints to ensure the existence of a conductive path for each two-pin connection [22]. Reencoding ULCs shows significant performance improvement on almost all such formulas. For example, homer19.shuffled timed out with original encoding and took SBVA 75 seconds, but with our method, it was solved in 2 seconds.

• $\mathrm{■}$

  Petri Net Concurrency Petri nets are a model for concurrent computation that uses places and transitions [6]. Each formula represents whether there exists a valid partitioning of the Petri net’s places into distinct subsets (units) respecting a given concurrency relation. The ULCs in these formulas encode that every place belongs to a unit. Our method drastically improved solver performance on these formulas. For example, vlsat2_30744_3925645.dimacs[3], a formula that timed out with both the original encoding and SBVA, was solved by our method in 177 seconds.

We also noticed that the majority of unalignable formulas belong to the Graph/Subgraph Isomorphism family. These formulas consider two random graphs and the question of whether one is a subgraph of the other. This is encoded by searching for a permutation of one of the graphs such that they overlap [2]. The formula contains many unalignable ULCs encoding the permutations.

Based on the strong results on graph-coloring problems, we tested whether our version of CaDiCaL enhanced with reencoding boosts SAT-based graph-coloring approaches. For this purpose, we used the CliColCom framework [16], which represents the state-of-the-art in graph coloring and includes several techniques to improve performance for this application, such as symmetry breaking. We ran CliColCom on the DIMACS graph coloring suite [18]. Using CaDiCaL version 2.1.0 (unmodified), the framework could solve 90 benchmarks within an hour, while using the modified CaDiCaL (same version, but with our reencoding technique) allowed solving two more benchmarks. The additional benchmarks are: queen9_9 (solved in 116 seconds) and queen10_10 (solved in 2103 seconds). The runtime on most graphs was similar. An exception is abb313GPIA, which was solved in 2.12 seconds using the modified version and in 150.11 seconds using the unmodified CaDiCaL. Note that this graph was not solved with CaDiCaL version 1.5.2 used in the CliColCom paper [16].