I saw an impressive plot at the recent SAT'25 conference:
Two CaDiCaLs are plotted against each other. The one on the bottom recieves instances just in their original form, while the left one recives them reencoded in some clever new way, developed by Aeacus Sheng, Joseph E. Reeves and Marijn Heule.
This reencoding scheme detects Unique Literal Clauses (ULCs), and rewrites them.
Take the clause
$$ C_1 = (l_1 \, l_2 \, l_3 \, l_4 \, l_5)$$If all the literals $l_1 … l_5$ don’t occur anywhere else in the formula $F$, then $C_1$ is a ULC (the negated literals $\bar l_1, \bar l_2$ etc. can still occur somewhere else). An interesting property is now that if there exists some satisfying assignment of $F$, then there also exist one where only a single of the literals in $C_1$ is set to true.
Aeacus et al. exploit this by enforcing an ExactlyOne-constraint on $l_1 … l_5$ (via some sequential counters, or order variables). Satisfiability is conserved, because if there exists a satisfying model with say both $l_1$ and $l_2$ true, we can always flip $l_2$ to be false without hurting $C_1$. And in the remaining formula we flipped at most some $\bar l_2$ to true, so we never make any other clause “less” satisfied.
Looking at the plot, this search space pruning seems to be especially efficient on UNSAT formulas.
Alignment
One nice trick is that the sequential counter variables are furthermore sorted in a certain way to “align” them. This alignment seems to be the real secret sauce to this whole enterprise. It can be calculated in linear time, in ca. 1-4 seconds on average, which given the plot above seems well worth the investment.
And what I find most elegant: The alignment is apparently also a really good predictor on whether the whole reencoding should be done or not.
- Alignment possible $\quad \ \Rightarrow$ Do ULC reencoding
- Alignment not possible $\Rightarrow$ Skip
That is really helpful! The scheme detects by itself whether it should be applied or not. So how often do we find alignment? Among the 5355 SAT Anniversary Track, alignment was found for 459 times, i.e. in ca. ~9% of cases. Those are the instances plotted above. About the other instanes we don’t need to care because they are filtered out automatically (and I suppose a failed alignment is detected much earlier than the given 1-4 seconds, though I couldn’t find that in the paper).
Against SBVA
The paper also provides a comparison against SBVA, which is a similar preprocessing step in that it also adds new variables and clauses instead of deleting some. Also, SBVA_CaDiCaL was the winner of the 2023 SAT Competition, so this seems like a good ground for comparison.
This looks like ULC beats SBVA on alignable formulas. Nice!
I wonder whether people will just include this ULC encoding in their next years’ solvers for the competition, or if there exists some hidden cost that I haven’t spotted yet.
PS: Aeacus also published a 2-page extended abstract, which might offer some more condensed overview by the original authors. (local copy)