Xorcle

Xorcle is a SAT solver for XNF formulas, where clauses are disjunctions of linear equations modulo 2. It implements CDCL(⊕) as described in Extending CDCL to disjunctions of parity equations by Paul Beame and Glenn Sun. For details, see arXiv:2605.15002. When citing this work, refer to the conference version at https://doi.org/10.4230/LIPIcs.SAT.2026.5.

This repository contains code written by generative AI.

Building

Requires CMake ≥ 3.31 and a C++23 compiler.

cmake -B build -DCMAKE_BUILD_TYPE=Release
cmake --build build -j

You can also compile with -DCMAKE_BUILD_TYPE=Debug to ensure that more debug assertions are checked.

The same three configurations are available as CMake presets, each with its own build directory: cmake --preset release (build/), debug (build-debug/) and profile (build-profile/), then cmake --build --preset <name> -j.

Running

xorcle [options] <instance>

Run xorcle --help to print the full list of options.

Benchmarks

There are 5 synthetic benchmark families (e.g. random formulas, Tseitin formulas) and 8 cryptography-related families from j-danner/2xnf_sat_solving [DOI] and j-danner/Xorricane-paper [DOI]. Generate and download these benchmarks with

pip install cnfgen==0.9.5 networkx==3.6.1
tools/generate_xnf_tests.py
tools/fetch_benchmarks.py

To run these benchmarks, use

tools/compare.py

A small number of files will run on the default configuration and complete within a few seconds. To run other files or configurations, see --help.

Testing

ctest --test-dir build

Two tests are registered: unit tests confirm that individual pieces of the solver are compiled correctly, and proof_roundtrip solves an UNSAT instance and checks the result with tools/check_lrup_parity.py.

Output

Xorcle's output will be in stdout.

c File: benchmarks/generated/random_kxnf_n/random_kxnf_n_n12_k2_s1.xnf
c Variables: 12
c Start clauses: 30
c Final clauses: 62
[... additional stats hidden ...]
c Time: 0.001 s
s SATISFIABLE
v -1 2 -3 -4 -5 -6 -7 8 -9 10 -11 12 0

--stats-file=<path> replaces all of the above with a single CSV row appended to that path, with a header written only if the file is new or empty.

Profiling

Run tools/profile.py [tool options] <instance> [xorcle options] to profile timings using samply and a web browser (macOS and Linux only). Install samply via cargo install samply (Rust's package manager) first. See --help for details.

Run tools/counters.py [tool options] <instance> [xorcle options] to profile hardware counters (cache misses, branch mispredictions, etc.) using Instruments on macOS or perf stat on Linux. On macOS, you may need to provide an initial configuration by open -a Instruments, choose "CPU Counters" in the menu, add events to observe, then File > Save as Template... and provide this template to the script via --template.

File formats

Extended DIMACS/XNF

Xorcle reads an extended DIMACS/XNF format, mirroring 2-Xornado. The file must begin with p cnf <num_vars> <num_clauses> or p xnf <num_vars> <num_clauses>. Comment lines begin with c, and blank lines are ignored; both may appear anywhere.

Each clause line is one clause and must end with a trailing 0. XOR expressions in clauses are written with +-joined variable lists and are taken to be true (= 1) by default. A leading - sign negates the expression (= 0). (Accordingly, any valid DIMACS CNF is automatically a valid XNF file.) For example,

-1+2+5 4+9 3 0

is the linear clause $\lnot (x_1 \oplus x_2 \oplus x_5) \lor (x_4 \oplus x_9) \lor x_3$. The number of clause lines must match the header's count.

LRUP(⊕)

The option --proof=<path> writes a proof in LRUP(⊕), an analogue of LRUP proofs. The syntax is analogous to the input format above.

Assign implicit IDs to input clauses starting from 1, in the order they appear in the input file. An LRUP(⊕) parity proof file contains lines in the following format:

<new id> <xor expr> <xor expr> ... 0 <reason id> <reason id> ... 0

• <new id> continues counting up from the last input clause.
• <xor expr> <xor expr> ... is a learned clause.
• <reason id> <reason id> ... is a list of clause IDs such that the negation of the learned clause propagates contradiction using the mentioned clauses in the specified order.

Lines of the form <reason id> <reason id> ... 0 are also permitted, and indicate that the listed reasons will not be used again and can be deleted for memory efficiency. Xorcle does not yet emit such lines.

Use tools/check_lrup_parity.py to check a proof. (Note that --compact=false is currently required to emit proofs.)

build/xorcle --compact=false --proof=out.lrup instance.xnf
python3 tools/check_lrup_parity.py instance.xnf out.lrup

Tools

The tools/ directory has useful Python scripts. For more information about how to use each script, use --help on each script.

Script	Purpose
generate_xnf_tests.py	Deterministic, seeded generation of test instances
fetch_benchmarks.py	Downloads the external benchmark suites
compare.py	Helpful tools to compare solver configurations
compare_to_release.py	Compares this build against the v0.1 release
check_lrup_parity.py	LRUP(⊕) proof checker
xnf_convert.py	Converts XNF to CNF, CNF-XOR, 2-XNF, or exponential CNF
xnf_lib.py	XNF parsing, writing, and other tools
profile.py	Profile timings with samply
counters.py	Profile hardware counters
profile_common.py	Helper functions for profiling

Repository layout

• src/algebra/ — GF(2) equations and row-echelon matrices, with dense/ and sparse/ representations
• src/core/ — the base algorithms: the CDCL(⊕) loop, clause learning, unit propagation, the trail
• src/heuristics/ — the choices the algorithms leave open (decisions, clause selection, restarts) and the optimizations layered on top (compaction)
• src/io/ — DIMACS/XNF parsing and LRUP(⊕) proof logging
• src/util/ — index sets, the max-heap, print modes, the random source and the statistics record and its CSV writer
• src/cli/ — the option table and the executable
• tools/ — Python tooling: instance generation and fetching, format conversion, the LRUP(⊕) proof checker, and the comparison harness
• benchmarks/ — the instance manifest, and the gitignored trees the generator and the fetcher write to
• tests/ — unit tests

Documentation

The source carries Doxygen comments. To build the HTML reference:

doxygen docs/Doxyfile

Output lands in docs/html/. Open docs/html/index.html afterwards to view documentation.