FRAT-XOR

This repository contains the frat-xor tool for elaborating unsatisfiability proofs for formulas from FRAT-XOR to XLRUP format.

The latter format is supported by a formally verified proof checker cake_xlrup, whose verified binary implementation can be found in its own directory. The format description is here.

This repository was created as a fork of FRAT-rs which is available here.

Proofs in FRAT-XOR format can be generated by the CryptoMiniSat SAT solver which is available here.

Build

You must have the rust toolchain, including cargo, installed. Then you can build with:

cargo clean
cargo build --release

You can find the compiled tool at ./target/release/frat-xor. In case you need a static compilation, build with:

cargo clean
rustup target add x86_64-unknown-linux-musl
cargo build --release --target=x86_64-unknown-linux-musl

The compiled tool is at ./target/x86_64-unknown-linux-musl/release/frat-xor.

Usage

The following command elaborates the unsatisfiability proof in FRAT-XOR format (xfrat_file) of the input formula (input_file) and produces the proof in XLRUP format (xlrup_file).

frat-xor elab xfrat_file input_file xlrup_file

You can find an example below.

frat-xor elab ./example/test_1.xfrat ./example/test_1.xnf ./example/test_1.xlrup

The elaborated proof can be checked with cake_xlrup.

cake_xlrup ./example/test_1.xnf ./example/test_1.xlrup

References

frat-xor and cake_xlrup were built to support certified approximate counting but can also be used as a standalone UNSAT proof checking pipeline.

• Support for CNF-XOR proofs is described in our CAV'24 paper.

• Extension with support for BNN constraints is in our SAT'25 paper (to appear).