Satsuma CNF preprocessing

Satsuma optionally preprocesses STP’s complete CNF before it is loaded into the SAT backend. It uses an output callback inside the process, with no temporary DIMACS file or preprocessing subprocess. The same adapter supports CaDiCaL, CryptoMiniSat and Kissat. Both the build option and runtime option are off by default; this is an experimental pipeline.

Build and use

cmake -S . -B build -DENABLE_AUTO_DOWNLOAD=ON -DUSE_SATSUMA=ON
cmake --build build --parallel
build/stp --satsuma=lex problem.smt2
build/stp --satsuma=fix problem.smt2

USE_SATSUMA requires a C++20 compiler for the SAT adapter. CMake builds the pinned stp/satsuma dependency through Satsuma-EP and installs its header API and pinned Dejavu headers into STP_DEP_DIR. The revision is in cmake/FindSatsuma.cmake. Dependency changes are commits in the fork; STP does not apply patches during its build. A separately installed copy can be selected with -DSATSUMA_DIR=/path/to/prefix. An ordinary Satsuma installation without the CNF output API is rejected during configuration.

The runtime option is satsuma=off|lex|fix. API clients can set it through options.set("satsuma", "lex") before their first check. Explicit backend selection is supported: --cadical, --cryptominisat or --kissat on the CLI, and options.set("sat-backend", "kissat") in the C++ API. Enable -DUSE_KISSAT=ON together with -DUSE_SATSUMA=ON to use the two features together.

Lex uses unit propagation, removed-variable units, a component limit of 500,000, an order-model budget of 750,000, and a dense-model budget of 20,000,000. Fix additionally enables iterative orbitopal, Schreier, and negation fixing, with pure-literal preprocessing. Cliquer is disabled. The output contains the simplified formula and symmetry-breaking clauses; its size can grow, and solving it can be slower than solving the original.

Model preservation and supported queries

Original variable numbers are retained, extension variables are allocated before clauses are loaded, and removed assignments are restored as unit clauses using set_add_reduced_as_unit(true), the API equivalent of --add-reduced-as-unit. This is required because STP reads the original CNF variables directly from the backend model rather than running Satsuma model reconstruction. STP can therefore read a model of its original encoding.

Preprocessing is restricted to a complete batch encoding on a fresh SAT backend. Incremental sessions, assumptions, auxiliary solvers, and queries requiring array, BV, FP, UF, or LRA refinement bypass it. An abstraction’s symmetry may be invalidated by later refinement clauses. Merely freezing variables would not make permanent symmetry breaking sound in that case. Surviving array operations or an active equality registry also force bypass. Formulas with at least five million variables, or beyond integer arena size limits, use ordinary clause loading.

Eligibility depends on the encoding path, rather than the declared SMT logic. QF_ABV and QF_ABVFP queries can use Satsuma when the early eager array pass removes their array operations, floating-point operations are encoded exactly, and no other refinement source is active. Queries using lazy array reads, lazy array equality, or FP abstraction bypass it. This restriction applies regardless of the SAT backend. With -s, the satsuma: mode=... or satsuma: skipped ... line reports whether preprocessing ran when CNF reached clause loading.

STP polls its preparation budget while translating and loading clauses and before and after Satsuma. Satsuma’s core currently has no cooperative wall-clock cancellation hook. An external process watchdog is needed to enforce a strict complete-process cutoff. Large formulas can exhaust memory; Dejavu’s allocation handling can crash under an address-space limit. Proof production and a combined STP/Satsuma proof are not supported here.

Testing and performance

cmake -S . -B build -DENABLE_AUTO_DOWNLOAD=ON -DUSE_SATSUMA=ON \
  -DENABLE_TESTING=ON -DUSE_CADICAL=ON -DUSE_CRYPTOMINISAT=ON -DUSE_KISSAT=ON
cmake --build build --parallel
ctest --test-dir build -L satsuma --output-on-failure

The tests run each enabled backend through off, lex, and fix modes. They include exhaustive Boolean oracles, pigeonhole symmetry, original-model checking, floating-point arithmetic, refinement bypass, incremental push/pop, and a standalone public C++ API client. CI covers all three backends with assertions enabled and disabled, and also builds Satsuma with Kissat as the only backend. The fork separately compares callback output byte for byte against its original DIMACS output path.

The prototype experiment on 63,441 non-incremental QF_BV/QF_BVFP files, using CaDiCaL 3.0.1, had the following PAR2 at a 60-second end-to-end cutoff and a 10 GiB virtual-address-space limit. Every unsuccessful run cost 120 seconds, and each configuration ran once per file.

Prototype experiment

Configuration	Solved	PAR2 seconds
off	62526	2.217422
lex	62438	2.431454
fix	62294	2.971489

These are measurements of the prototype revision, not a benchmark of this upstream integration branch. They motivate keeping the feature optional; they do not establish a useful policy for automatically selecting it.