XNF solver evaluation

7530 solver runs over 1695 instances in 13 benchmark families · AMD EPYC 7763 64-Core Processor, 15 GB RAM · generated 2026-09-13

Solvers

Four solvers, each given the encoding it is designed for (Tseitin excepted, which is CNF for all of them). CryptoMiniSat is a CNF-XOR CDCL solver; Xorcle and Xorricane are XNF CDCL solvers (disjunctions of parity constraints); Bosphorus combines algebraic and logical reasoning over ANF.

What CryptoMiniSat needed

CryptoMiniSat’s defaults are tuned for general CNF, and on these families they discard almost all of the linear structure before search begins: --maxnummatrices defaults to 5 where lifted pebbling builds 11476 simultaneous matrices, and --maxmatrixrows defaults to 2000 where a single Bivium matrix is 10809 rows. The command line above lifts those cutoffs, which is what makes this a measurement of the CNF-XOR path rather than the plain CNF one.

Lifting them was not enough on its own — the solver had not been run in that regime before, and three changes were required. All are in the pinned revision used here:

Commit	Change	Needed for
068a3fd79	fix crash when --maxnummatrices exceeds 1000	lifted pebbling
bef479cef	avoid O(num_matrices) per-literal work in Gauss-Jordan elimination	lifted pebbling
3970aaf24	raise MAX_XOR_RECOVER_SIZE from 8 to 12	Tseitin at k = 9, 10

The last one mattered because a Tseitin formula on a k-regular graph has one parity constraint of degree exactly k, and the compile-time ceiling of 8 put k = 9 and k = 10 out of reach at any runtime setting. With it raised, CryptoMiniSat solves 75/75 of that family instead of 60/75.

The improved CryptoMiniSat

cms-improved is b79d6193a, 70 commits after the 3970aaf24 used for cms. It runs with no options, as 4b82356e7 made the settings above its defaults. Beyond that, Gauss-Jordan elimination was made cheaper, much of CaDiCaL’s search was brought across, and local search was replaced by xnfSAT, which uses the XOR structure.

Bugs found in the XNF solvers

We wrote xnf_fuzzer.py, which extends CryptoMiniSat’s CNF fuzzers, among them Brummayer’s FuzzSAT (Brummayer, Lonsing and Biere, SAT 2010), to XNF and 2-XNF. Each instance goes to Xorcle (and Xorricane on 2-XNF) and, as CNF-XOR, to CryptoMiniSat: SAT answers are checked by substitution, UNSAT ones by CryptoMiniSat’s proof in cake_xlrup. We also fuzzed UBSan and ASan builds of both solvers, and tried a few hand-written edge cases. Most of what turned up is minor: crashes on degenerate inputs, assertions that only fire in Debug builds, and issues behind non-default options. Two change the answer, both on unusual input: a variable repeated inside a lineral, and tab-separated input. CryptoMiniSat gave no wrong answers on the same instances; its own problems in this regime, listed above, were a crash and a slowdown with many matrices. Each fix is one patch, whose commit message is the bug report.

Xorcle: bugs-xorcle/

Patch	Bug	Impact
patch-1.diff	a repeated variable in a lineral is OR-ed, not XOR-ed	wrong answer, on inputs that repeat a variable
patch-2.diff	an empty input clause segfaults instead of giving UNSAT	crash on a degenerate input
patch-3.diff	the proof checker rejects the p xnf header	proof checker script only
patch-4.diff	the proof checker has the same OR/XOR parsing bug	proof checker script only

Xorricane: bugs-xorricane/

Patch	Bug	Impact
patch-1.diff	util clause deletion writes out of bounds: segfault	crash, non-default -delh util only
patch-2.diff	avg_util clause deletion (the default) reads uninitialised memory	undefined behaviour; no wrong answer seen
patch-3.diff	every UNSAT answer calls back() on an empty list	undefined behaviour; aborts in Debug builds only
patch-4.diff	an assertion dereferences a null pointer with -no-lgj	Debug builds with -no-lgj only
patch-5.diff	Gauss elimination (-il) never reads the first matrix row	missed propagations; same answers
patch-6.diff	the parser splits on spaces only: wrong answer on tabs, CRLF rejected	wrong answer on tab-separated input
patch-7.diff	a late equivalence overwrites an existing one	assertion in Debug builds; release answer correct
patch-8.diff	the empty XOR line x 0 overflows the heap	crash on a degenerate input
patch-9.diff	an assertion fails with -rh lbd when a learnt clause has LBD 0	Debug builds only; release answer correct

Benchmarks

Encodings and conversion

The same formula appears in several formats; each solver reads the one it supports. Conversions were done with these tools:

Extension	Format	Produced by
.cnf	plain CNF, XORs blasted	shipped with the benchmark
.xcnf / .cnf-xor	CNF-XOR	shipped, or xnf_to_xcnf.py
.2xcnf	CNF-XOR built from the 2-XNF	xnf_to_xcnf.py
.xnf	XNF, + linerals	shipped
.2xnf	2-XNF, at most two linerals per clause	shipped with the benchmark
.anf	algebraic normal form	shipped with the benchmark

The CNF-XOR encodings a benchmark does not ship were generated to match the one the Xorricane paper uses, and reproduce all 200 shipped .xcnf files exactly — variable, clause and xor-line counts all agree.

Overall results

PAR2 is the SAT-competition penalised average runtime: the mean over attempted instances of the solve time, with unsolved instances charged twice the timeout. Lower is better. The attempted column makes the denominator explicit, since not every solver ran on every family.

CDF of solving time over all families. Bosphorus is excluded here because it was only run on the Ascon and Xorricane-paper suites. CryptoMiniSat appears twice: cms is the older build with the options above, cms-improved the newer build with none. Where cms was also run on a CNF-XOR encoding (Type I quadratic systems), this plot uses its plain CNF run. Every line covers all 1695 instances.

Per-family results

2xnf-ascon — Ascon-128 (2-Xornado suite)

2xnf-rand — Random 2-XNF (unsat-mixed)

2xnf-rand_sat — Random 2-XNF (satisfiable)

tseitin_n_k — Tseitin formulas in CNF

ascon — Ascon (Xorricane suite, Benchmark 6.5)

bivium — Bivium (Xorricane Benchmark 6.6)

ctc — CTC2 (Xorricane Benchmark 6.7)

rand_l2xnf_ld — Random linear system with 2-XNF constraints (Benchmark 6.3)

rand_qp_type_I — Multivariate quadratic, Type I (Benchmark 6.4)

rand_qp_type_IV — Multivariate quadratic, Type IV (Benchmark 6.4)

pebbling_lifted_h_k — Pebbling formulas lifted by k-XORs

random_kxnf_n — Random k-XNFs

restricted_kxnf_n — Restricted random k-XNFs

Caveats