Problem Partitioning via Proof Prefixes

This work provides 3 main contributions:

1. 1.

   We developed a tool that performs partitioning based on proof prefixes during partial application of a solver.

2. 2.

   We developed a tool that performs cardinality-based partitioning with the $k$-totalizer encoding, selecting auxiliary variables to split on based on their semantic meanings in the encoding.

3. 3.

   We performed an experimental evaluation comparing our approaches to the widely used partitioning tools, March. We considered SAT and MaxSAT competition formulas, as well as several combinatorial problems and found that our approaches often performed better than existing tools.

We consider propositional formulas in conjunctive normal form (CNF). A CNF formula $\phi$ is a conjunction of clauses where each clause is a disjunction of literals. A literal $\mathrm{\ell }$ is either a variable $x$ (positive literal) or a negated variable $\overline{x}$ (negative literal). An assignment $\alpha$ is a mapping from variables to truth values $1$ (true) and $0$ (false). An assignment $\alpha$ satisfies a positive (negative) literal $\mathrm{\ell }$ if $\alpha$ maps $\mathrm{𝗏𝖺𝗋}(\mathrm{\ell })$ to $\mathrm{𝗍𝗋𝗎𝖾}$ ($\mathrm{𝖿𝖺𝗅𝗌𝖾}$, respectively), and falsifies it if $\alpha$ maps $\mathrm{𝗏𝖺𝗋}(\mathrm{\ell })$ to $\mathrm{𝖿𝖺𝗅𝗌𝖾}$ ($\mathrm{𝗍𝗋𝗎𝖾}$, respectively).

An assignment satisfies a clause if the clause contains a literal satisfied by the assignment, and satisfies a formula if every clause in the formula is satisfied by the assignment. A formula is satisfiable if there exists a satisfying assignment, and unsatisfiable otherwise.

A cardinality constraint on Boolean variables has the form ${\mathrm{\ell }}_1+{\mathrm{\ell }}_2+\mathrm{\cdots }+{\mathrm{\ell }}_s\ge k$ and is satisfied by a partial assignment if the sum of the satisfied literals is at least $k$. The size of the cardinality constraint is the number of literals ($s$) it contains. Variables occurring in the cardinality constraint are data variables, and new variables added in a clausal encoding are auxiliary variables. For a general cardinality constraint with , unit propagation should lead to a conflict when $s-k+1$ data literals in the constraint are falsified. Cardinality constraints occur often in SAT problems, and commonly represent the bound in an optimization problem, for example “at least $k$ packages must be delivered using at most $j$ trucks.” There are many ways to encode a cardinality constraint as clauses [3, 24, 23, 1, 30]. In this work, we will use the totalizer encoding, explained further in Section 3.2.

To evaluate the satisfiability of a formula, a CDCL solver [22] alternates between conflict-driven search and inprocessing. In search, the solver performs a series of variable decisions [5, 20] and unit propagations. If no conflict is reached, the formula is satisfiable. If the solver encounters a conflict, the solver performs conflict analysis potentially learning a clause. In case this clause is the empty clause, the formula is unsatisfiable. Otherwise, the solver revokes some of its variable assignments (“backjumping”) and then repeats the whole procedure. Additionally, modern solvers incorporate pre- and inprocessing techniques that change the formula in some way, usually reducing the number of variables and clauses or shrinking the sizes of clauses. These techniques are intermittently interleaved with search during the solving. Some of the most common inprocessing techniques are bounded variable elimination (BVE) [9], vivification [19], and probing [10]

CDCL solvers produce satisfying assignments for satisfiable formulas and proofs of unsatisfiability for unsatisfiable formulas. A clause $C$ is redundant w.r.t. a formula $\phi$ if $\phi$ and $\phi \cup \{C\}$ are satisfiability equivalent. The clause sequence $\phi ,C_1,C_2,\mathrm{\dots },C_m$ is a clausal proof of $C_m$ if each clause $C_i(1\le i\le m)$ is redundant w.r.t. $\phi \cup \{C_1,C_2,\mathrm{\dots },C_{i-1}\}$. The proof is a refutation of $\phi$ if $C_m$ is $\perp$. Clausal proof systems may also allow deletion.

The strength of a clausal proof system is determined by the syntactic criterion it enforces when checking clause redundancy. The standard SAT solving paradigm CDCL learns clauses that are logically implied by the formula and fall under the reverse unit propagation (RUP) proof system. A clause is RUP if unit propagation on the falsified literals of the clause results in a conflict. The Resolution Asymmetric Tautology (RAT) proof system generalizes RUP and all commonly used inprocessing techniques can be compactly expressed using RAT steps. Proofs are typically transformed to a format with hints, e.g. LRAT, before being passed to a formally-verified checker like cake-lpr [35].

When a CDCL solver logs a proof, the only distinction made between proof steps is if they are clause additions or clause deletions. Without additional processing there is no way to determine if a clause addition in the proof originated from conflict learning or an inprocessing technique. In this work, we consume proofs externally without modifying the solver, so the proof-based heuristics described in Section 3.1 will consider both learned clauses and inprocessed clauses.

Cube-and-Conquer (CnC) [14] is a powerful methodology for solving difficult SAT formulas. In typical usage, a formula $\phi$ is partitioned into many sub-formulas, ${\phi }_1,\mathrm{\dots },{\phi }_n$, such that $\phi$ is satisfiable if and only if at least one ${\phi }_i$ is satisfiable. The cubes to which the name refers are conjunctions of literals. In particular, if a disjunction of cubes $\psi :={\psi }_1\vee \mathrm{\cdots }\vee {\psi }_n$ is a tautology, then

Thus, the choice of partition from which the technique gets its name is ${\phi }_i:=\phi \wedge {\psi }_i$. With this partition, one can dispatch independent CDCL solvers in parallel, as depicted in Figure 1, and enjoy substantial speedups.

In the best case, each $\phi \wedge {\psi }_i$ is of equal difficulty and substantially easier to solve than $\phi$. In the worst case, however, each $\phi \wedge {\psi }_i$ can be no easier, and sometimes harder, than just $\phi$. In this case, the wall-clock time is no better than just running $\phi$, and the CPU time can blow up exponentially. As a result, the choice of $\psi$ is of great importance and the focus of this paper. Historically, this has been done with expert insight and domain knowledge on a problem-by-problem basis [15, 34, 32], or with lookahead techniques [14]. In this paper, we will propose several new, automatic methods for finding good choices of $\psi$.

The state-of-the-art tool for automatically computing partitions is March, which combines the David-Putnam-Logemann-Loveland (DPLL) algorithm [8] with lookaheads. For a general discussion, see the Handbook of Satisfiability [16, 18], while we describe here an exemplary scheme. Given a CNF formula $\phi$, a lookahead on literal $\mathrm{\ell }$ works as follows: First, $\mathrm{\ell }$ is assigned to true, followed by unit propagation. Second, in case there was no conflict, the difference between $\phi$ and the reduced formula ${\phi }^{\prime }$ is measured. The quality of look-ahead techniques depends heavily on the measurement used. A frequently used method weighs the clauses in ${\phi }^{\prime }\setminus \phi$ (i.e., the clauses that are reduced but not satisfied). Third, all simplifications are reversed to return to $\phi$. If a conflict was detected during the lookahead, then $\mathrm{\ell }$ is forced to false and is called a failed literal. The measurements are used to determine the splitting variable in each node of the tree. In general, a variable $x$ is chosen for which both the lookahead on $x$ and $\overline{x}$ result in a large reduction of the formula.

In this section, we describe a partitioning technique based on proof prefixes. A proof, in this context, is a series of clauses that are redundant with respect to the original formula. A formula is unsatisfiable when the empty clause is derived. A proof prefix is a sequence of addition steps starting from the beginning of a proof. The key metrics we extrapolate from proof prefixes are variable occurrences, or the number of times a variable appears in a clause addition step. The partitioning technique arises from two observations regarding proof prefixes.

1. 1.

   Variables which occur frequently in a non-trivial proof prefix will often continue to appear frequently in the remainder of the proof. By non-trivial we mean a proof prefix with a large enough number of steps such that the solver has performed reasoning over several restarts to explore the search space.

2. 2.

   In problems for which effective partitions are known, splitting variables often occur frequently in a proof generated from the original (unpartitioned) formula.

We ground these intuitions in Figure 2, which shows the variable occurrences in the DRAT proof over time for the ${\mu }_5(13)$ problem. Despite the proof taking more than ${10}^7$ clause addition steps, the known best variables have risen to near the top by only ${10}^5$. This observation is what allows us to use prefixes as an adequate substitute for the entire proof.

At a high level, we compute proof prefixes, find the most occurring variables in these prefixes, and use theses variables as splitting variables. From the solver’s brief search we infer which variables are important in the problem. More concretely, given a formula $\phi$, we run it with an off-the-shelf solver until a desired number of clauses are added to the proof emitted. This is achieved by piping the proof output of the solver, waiting for a desired number of addition steps, and then killing the solver. No modifications to the solver are required. Once the proof prefix is known, we count the variable occurrences in the proof, both positive and negative, and pick the most frequently occurring variable as the next variable to split on.

Once a splitting variable $x$ is obtained, we create new formulas, $\phi \wedge x$ as well as $\phi \wedge \overline{x}$, and restart the process on both formulas. Naively, generating a complete partition in this manner, where each cube has size $d$, would require generating $O(2^d)$ proof prefixes, which would be prohibitively expensive. To get around this, we introduce the notion of a static partition. A static partition is one where we start with a static set of $d$ splitting variables and then generate cubes with all $2^d$ combinations of polarities. This can be viewed as a balanced binary tree depicted in the left of Figure 3. In contrast, a dynamic partition, depicted in the right of Figure 3, may have unique variables at every vertex in the tree and is not necessarily balanced.

Given a static partition set of size $d$, to generate the $d+1$th variable, we sample a constant number of cubes from the current partition, find the best variable by summing the occurrences across all of the proof prefixes, and use it to extend the set. In this way, we can generate a static partition of depth $d$ by only generating $O(sd)$ proof prefixes, where $s$ is the number of samples per layer. The generation of proof prefixes can be parallelized, so if the number of samples is fewer than the number of cores, which is often sufficient, the cube generation time is a linear function of depth. However, we must synchronize upon solver completion, before processing the proof prefixes. One “layer” of this process is depicted in Figure 4. The specific number of clauses in each proof prefix that produces the best results is formula-dependent, and future work is needed to determine this automatically. However, in our experimental evaluation, we found $100,000$ is an effective cutoff for a wide range of competition formulas, and for many problems this is sufficient. Moreover, the required proof prefix size seems to scale far slower than problem size as demonstrated by the technique’s ability to effectively partition very difficult problems with comparatively little preproccesing. Despite the restriction to static partitions, our technique is highly effective across a variety of benchmarks. Moreover, finding an effective static split for a problem has numerous additional benefits, as will be discussed in Sections 4 and 5. This technique was developed into an automated tool, Proofix.

In this section, we present a partitioning technique based on auxiliary variables from the totalizer encoding. We assume that the problem is given in the cardinality-based input at-least-$k$ conjunctive normal form (KNF [26]), but the cardinality constraint may be encoded as an at-most-$k$ constraint by negating the literals and modifying the bound. This technique makes no assumptions about the clauses in the formula and forms a static partition solely by selecting auxiliary variables from the totalizer encoding.

The totalizer is one of the most widely used classes of cardinality constraint encodings, with incremental variants appearing in modern MaxSAT solvers. The totalizer is structured as a binary tree that incrementally counts the number of true data literals at each node. Data literals form the leaves, and each node has auxiliary variables representing the unary count from the sum of its children counters. For example, in Figure 5 with counters indexed by depth and node id, the counter $c_1^{3,1}$ is set true if either ${\mathrm{\ell }}_1$ or ${\mathrm{\ell }}_2$ is true, and $c_2^{3,1}$ is true if both ${\mathrm{\ell }}_1$ and ${\mathrm{\ell }}_2$ are true. Further, if both counters $c_2^{3,1}$ and $c_2^{3,2}$ are true, then the counter $c_4^{2,1}$ is true.

Output variables denoted by $o_i$ at the root of the tree represent the count of true data literals across the entire cardinality constraint. The bound $k$ for an at-most-$k$ constraint is enforced by adding the unit ${\overline{o}}_{k+1}$. An at-least-$k$ cardinality constraint would enforce the bound with the positive unit $o_k$. The encoding can be simplified by only encoding the count up to $k+1$ at each node [23], and we adopt this simplification for our encoding.

To motivate our splitting heuristic, first consider the totalizer in Figure 5. Selecting $c_4^{1,1}$ as a splitting variable will result in the following two cases:

• $\mathrm{■}$

  If $c_4^{1,1}$ is true, at least $4$ of the data literals from the set ${\mathrm{\ell }}_1,{\mathrm{\ell }}_2,\mathrm{\dots },{\mathrm{\ell }}_8$ are true. This also means that at most $3$ data literals from the set ${\mathrm{\ell }}_9,{\mathrm{\ell }}_{10},\mathrm{\dots },{\mathrm{\ell }}_{16}$ are true due to the bound of at most $7$.

• $\mathrm{■}$

  If $c_4^{1,1}$ is false, at most $3$ of the data literals from the set ${\mathrm{\ell }}_1,{\mathrm{\ell }}_2,\mathrm{\dots },{\mathrm{\ell }}_8$ are true. This provides no information about the data literals from the set ${\mathrm{\ell }}_9,{\mathrm{\ell }}_{10},\mathrm{\dots },{\mathrm{\ell }}_{16}$.

Intuitively, splitting on an auxiliary variable at an internal node in the totalizer will designate how many true data literals are among its children and potentially its sibling nodes. Furthermore, the closer the auxiliary variable is to the root, the more data literals it will impact. However, a bad selection can create unbalanced subproblems. For instance, if we split on $c_7^{1,1}$, when $c_7^{1,1}$ is true all of the data literals from ${\mathrm{\ell }}_9,{\mathrm{\ell }}_{10},\mathrm{\dots },{\mathrm{\ell }}_{16}$ are set false due to the bound. This may create a trivial cube. On the other hand, when $c_7^{1,1}$ is false, we obtain very little information other than that at least one of ${\mathrm{\ell }}_1,{\mathrm{\ell }}_2,\mathrm{\dots },{\mathrm{\ell }}_8$ is false, and this would likely not benefit the solver. Therefore, we focus our splitting on auxiliary variables with a large impact that also correlate with the cardinality constraint’s bound. To achieve this, we use the ratio $Rk=\frac{k}{s}$ for a cardinality constraint with bound $k$ and $s$ data literals. We select a counter from a node ($id$) with $n$ counters as $\mathrm{𝖲𝖾𝗅𝖾𝖼𝗍𝖢𝗈𝗎𝗇𝗍𝖾𝗋}(id)=\lfloor Rk\times n\rfloor$. The selection procedure is as follows:

1. 1.

   Select a starting depth $d$ and desired number of splitting variables $v$.

2. 2.

   Sort the nodes at depth $d$ by number of counters, largest to smallest.

3. 3.

   For each node ($id$) in $d$, select the counter $\mathrm{𝖲𝖾𝗅𝖾𝖼𝗍𝖢𝗈𝗎𝗇𝗍𝖾𝗋}(id)+1$ for odd nodes and $\mathrm{𝖲𝖾𝗅𝖾𝖼𝗍𝖢𝗈𝗎𝗇𝗍𝖾𝗋}(id)$ for even nodes.

4. 4.

   If $v$ variables are selected, break. Otherwise, proceed to depth $d+1$ and return to step 2 to select the remaining variables.

Consider the totalizer in Figure 5 with $Rk=\frac{7}{16}=0.4375$. Assume that we want $6$ splitting variables, starting from depth $1$. Start with node $1$ which contains $8$ counters. The counter from node $1$ will be $\mathrm{𝖲𝖾𝗅𝖾𝖼𝗍𝖢𝗈𝗎𝗇𝗍𝖾𝗋}(1)+1=\lfloor 8\times 0.4375\rfloor +1=4$, which is variable $c_4^{1,1}$. Then move on to node $2$ and select $c_3^{1,2}$. Next, move to depth $2$, and since all nodes have the same number of counters we process them in order. At node $1$ with $4$ counters take $\mathrm{𝖲𝖾𝗅𝖾𝖼𝗍𝖢𝗈𝗎𝗇𝗍𝖾𝗋}(1)+1=\lfloor 4\times 0.4375\rfloor +1=2$, which is variable $c_2^{2,1}$. Proceed with the remaining nodes at depth $2$ selecting $c_1^{2,2}$, $c_2^{2,3}$, and $c_1^{2,4}$. These $6$ variables are then used as the splitting variables to generate a static partition of the formula.

The reason we alternate between $\mathrm{𝖲𝖾𝗅𝖾𝖼𝗍𝖢𝗈𝗎𝗇𝗍𝖾𝗋}(id)$ and $\mathrm{𝖲𝖾𝗅𝖾𝖼𝗍𝖢𝗈𝗎𝗇𝗍𝖾𝗋}(id)+1$ is to ensure that the sum of the counts of selected splitting variables across all nodes for a given depth resembles the ratio. This reduces the number of unhelpful or trivial cubes. For example, the selected variables at depth $2$: $c_2^{2,1}$, $c_1^{2,2}$, $c_2^{2,3}$, and $c_1^{2,4}$ will sum to $6$ in the cube where they are all set to true. If we only selected the $c_1$ counters, the sum would be $4$ and this is far from the bound of $7$, and if we only selected $c_2$ counters, the sum would be $8$ and this is trivially unsatisfiable.

The starting depth is assigned based on the number of desired splitting variables such that all nodes in a given depth are processed if possible. In our experimental configuration, we chose $12$ splitting variables and therefore started at depth $2$, giving $4$ variables at this depth and $8$ variables at depth $3$.

This approach could be adapted to the more compressed modulus totalizer [24], which uses a quotient and remainder at each node to reduce the number of auxiliary variables required to count the sum, by selecting quotient variables at each node. Other hierarchical encodings, for example, those used in pseudo-Boolean solving, would also be candidates for this approach. However, it is not clear how splitting could be achieved with a non-hierarchical encoding like a sequential counter. Also, we do not consider splitting on formulas with many cardinality constraints. It is possible to select a subset of variables from each cardinality constraint encoding, but this would require heuristics for determining the relative importance of each cardinality constraint. Lastly, we focus on unsatisfiable problems with a tight bound, which means that adding $1$ to the bound would make the problem satisfiable. If the bound is not tight, we may need to adjust the ratio $Rk$ by sampling for trivial cubes.

One of the properties that makes the proof prefix technique powerful is the fact that the preprocessing time required scales far slower than problem difficulty. Indeed, looking at several difficult problems, if Proofix is able to find known good splitting variables, it can do so without needing to search deep into the proof.

The ${\mu }_n(k)$ problem asks to find the minimum number of convex $n$-gons induced by placing $k$ points in the plane with no three points in a line. Recently, Subercaseaux et al. [34] conjectured that ${\mu }_5(n)=\left(\genfrac{}{}{0pt}{}{\lfloor n/2\rfloor }{5}\right)+\left(\genfrac{}{}{0pt}{}{\lceil n/2\rceil }{5}\right)$. The ${\mu }_5(15)$ benchmark asks whether it is possible to construct only $76$ convex pentagons in the plane with $15$ points, one less than the known minimum of $77$. It should be noted that ${\mu }_5(15)$ is substantially easier for state-of-the-art MaxSAT solvers with an out-of-the-box wcnf formula than for CaDiCaL using the totalizer encoding. This problem takes at least $48$ CPU hours.

The ${\chi }_{\rho }({\mathbb{Z}}^{\mathit{2}})$ problem is a heavily optimized formula which was shown to be logically equivalent to asking whether there exists a packing chromatic number of the subset of the plane, $\{(x,y)\in {\mathbb{Z}}^2\mid |x|+|y|\le 15\}$, using $14$ colors and center color $6$. The “good” variables are precisely the ones corresponding to the “plus” tiling of the graph as described by Subercaseaux et al. [33]. With a manual partition of over $5,000,000$ cubes, this problem was solved in $4,851$ CPU hours.

The $7$gon-$6$hole problem asks whether every set of $24$ points with no $3$ three points in a line contains either a convex $7$-gon, or a $6$-hole (a convex $6$-gon with no points inside of it). This problem is estimated to have a single-core runtime of $1,000$ CPU hours and a manual partition was found reducing it to $200$ CPU hours (on a single core) [15].

Table 1 depicts the tool looking for variables that are known to be good on $3$ very difficult problems. Using just $32$ samples per variable, on two of them Proofix is able to pick out many known good variables after only searching for a tiny fraction of the time that the problem itself would take. While it is possible that Proofix was able to come up with an alternative set of “good” variables for the ${\mu }_5(15)$ problem, it more likely provides evidence that for certain proofs the prefix is not an adequate substitute. Understanding why this is the case is the subject of future work.

One caveat to note is that while finding good splitting variables can now be done automatically for many problems, for large problems such as these, it is not necessarily the case that the cubes found will always achieve comparable performance to the ones found manually due to factors such as variable ordering or the specific subset of “good” variables used in the static partition. The partition used to solve the ${\chi }_{\rho }({\mathbb{Z}}^2)$ problem, for example, used a dynamic partition with an unbalanced binary tree that Proofix cannot capture directly. Future work is required on how to use proof prefixes to efficiently capture dynamic partitions.

In this section, we evaluate the totalizer-based splitting and proof-based splitting on problems containing one large cardinality constraint. These types of problems occur naturally as unweighted maximum satisfiability (MaxSAT) problems. Each MaxSAT problem consists of a set of hard clauses and soft units. The objective is to find the optimum (minimum) number of soft units that must be falsified while satisfying all hard clauses. MaxSAT problems can be converted to SAT by combining the hard clauses with one, often large, cardinality constraint stating at most k soft units are falsified. We can generate an unsatisfiable SAT problem by making the cardinality constraint’s bound the optimum minus one, and a satisfiable SAT problem by making the bound the optimum.

In our evaluation, we consider MaxSAT benchmarks from the $2023$ competition unweighted track [17]. We generate unsatisfiable SAT problems from formulas with known bounds. The SAT problem is transformed into CNF by encoding the cardinality constraint as a totalizer. The cardinality constraint is transformed from at-least-$k$ to at-most-$k$ if this makes the encoding size smaller. Before encoding the cardinality constraint, we sort data literals using the best literal sorting found in recent work [25]. This step improves the default solver performance, creating a better baseline for partitioning.

We filter out problems with a CaDiCaL solving time of less than $500$ seconds, leaving five benchmark families: judgment aggregation (judge) [17], model-based diagnosis (mbd) [21], approximately propagation complete CNF for an all-different encoding of pigeon hole (optic) [2], user query authorization (uaq) [2], and minimum rule set for labeling data (mindset) [2]. For each family, we selected the hardest problem for CaDiCaL to solve, and present the results at the top of Table 2.

Proofix outperforms the other techniques in both single and $32$ core performance on the majority of the problems. Totalizer split performs adequately, which is notable due to its lack of preprocessing time other than time (less than a second) required to encode the cardinality constraint into CNF. Of all the selected problems, only mindset is not successfully partitioned by any technique, with totalizer split producing the best $32$ core speedup of only $2\times$.

The preprocessing time of Proofix is consistent across problems because there is only minor variation in the time it takes for the solver instances to produce $100,000$ proof steps. On the other hand, March has a large range of preprocessing times. For example, in mbd March spends as much time in preprocessing as totalizer split spends solving the problem on $32$ cores.

In addition, we examined the splitting variables selected by Proofix to find out if it used any auxiliary variables from the totalizer encoding. Proofix used some auxiliary variables for optic and mbd, a single auxiliary variable for judge, and no auxiliary variables in the other problems. This suggests that Proofix can discover auxiliary variables when they are more useful, as is the case for mbd based on the superior performance of totalizer split. Furthermore, Proofix achieves this without any additional insight into the problem or variable semantics. Many of the other problems can be effectively partitioned by either auxiliary variables or data variables, as seen by the similar performance of Proofix and totalizer split.

Next we discuss three additional hard combinatorial problems to test the limits of these splitting techniques. We describe the problems and their encodings at a high level below.

The Max Squares problem [36] asks whether you can set $m$ cells to true in an $n\times n$ grid such that no set of four true cells form the corners of a square. Problem variables denote whether a cell is in the solution. The problem is encoded with clauses containing $4$ literals blocking the $4$ corners of each possible square on the grid and one cardinality constraint over all of the problem variables. For a $10\times 10$ grid the optimal value is $61$, so a bound of $62$ on the cardinality constraint makes the formula unsatisfiable.

The crossing number $cr(G)$ of a graph $G$ is the lowest number of edge crossings of a plane drawing of the graph $G$. In 1960, Guy conjectured that the crossing number of the complete graph is $cr(K_n)=\frac{1}{4}\cdot \lfloor \frac{n}{2}\rfloor \cdot \lfloor \frac{n-1}{2}\rfloor \cdot \lfloor \frac{n-2}{2}\rfloor \cdot \lfloor \frac{n-3}{2}\rfloor$ [28]. It is known that $cr(K_{13})=225$. The benchmark cross13 asks whether there is a $K_{13}$ drawing with 224 crossings.

On the max$10$ problem, March exhibits good single-core performance but cannot match the improved $32$ core times from both of our techniques. Likewise, March fails to solve the cross$13$ problem with a $10,000$ second cube timeout. For each of these problems Proofix produces a partition with the best $32$ core performance, and it does so without using the auxiliary variables from the totalizer encoding. The totalizer split can approximate the performance of Proofix with slightly worse performance on each of the problems. Notably, the preprocessing time for Proofix on the much harder cross$13$ is lower than for ${\mu }_5(13)$, displaying the potential of a static splitting technique to scale and achieve a good partitioning with relatively low preprocessing overhead.

To measure the generalizability of Proofix, we compared it to both CaDiCaL [4] and March on SAT competition formulas from the years 2022, 2023, and 2024. We considered problems which were both UNSAT and took CaDiCaL more than $1,000$ seconds.

Proofix was used with settings where it learned the first ${10}^5$ clauses of the proof and generated a static partition of depth $10$, resulting in $2^{10}$ subprobems. Comparing Proofix to CaDiCaL directly, as shown in Figure 6, we see that $63\%$ of competition formulas perform better when first split and run on $32$ cores than when run with CaDiCaL alone, including the preprocessing time for splitting. If we disregard preprocessing time, this number increases to $75\%$. Including preprocessing, there are $26$ problems where Proofix performed more than $10\times$ better than CaDiCaL, and even one which performed $100\times$ better.

Unfortunately, March timed out or crashed while generating the cubes on multiple instances. We suspect that this is due to March learning a lot of “local” clauses and exceeding the available memory on formulas with many small clauses. To ensure a fair comparison, and to eliminate many additional cases where March failed to generate a partition before timing out, it was limited to a split of depth at most $10$.

As can be seen in Figure 7, Proofix performs favorably compared to March on many problems. Considering only problems where March did not segfault, Proofix performed better than March on $53\%$ of problems, and considering problems where March failed for any reason, that number increases to $61\%$. While there are a couple of cases where March beats Proofix by a large margin, there are far more where the opposite is true, and even two cases where Proofix produces a partition which is over $1,000\times$ better than March.

Although Proofix always succeeds in generating the cubes, there are $10$ cases where at least one cube takes more than $10,000$ seconds. This is in contrast to March, where a cube times out in $5$ cases, March itself times out in generating cubes in $8$ cases, and it segfaults while generating cubes in $35$ cases. The segfaults persisted across multiple compiled March binaries and multiple computers. In addition, it is worth noting that segfaults seem to be roughly correlated with partitioning difficulty, as $6$ of the $10$ instances for which Proofix times out on a cube also cause segfaults in March.

It can also be seen that while both tools can fail to find a good split in some cases, the amount that Proofix can fail by is far less than March. In the worst case, March’s 32 core time is $55,000$ seconds slower than CaDiCaL, whereas Proofix’s 32 core time is at most $21,800$ seconds worse. Moreover, there are $9$ problems where March produces a partition that has a time on 32 cores worse than CaDiCaL, compared to Proofix for which there are only $4$ (conditioned on March generating a partition at all).