# proofmin

`proofmin` computes short resolution refutations for UNSAT formulas and reports the best proof found with a lower bound on its length. If the search terminates before the time budget is exhausted, the lower bound and the length of the returned proof coincide, and the proof is *certified optimal*.

This repository is the code artifact accompanying the JAIR submission containing:

- `proofmin/`: the main Rust crate and CLI (`proofmin`).
- `lrat-score/`: a companion CLI (`lrat-score`) parsing an LRAT proof and reporting its length (axioms and derived lemmas), duplicate-derivation counts, and RAT-step counts. Used to compute the reference proof lengths used in the paper comparisons.
- `rustsat-cadical/`: a vendored and patched copy of the `rustsat-cadical` crate bundling CaDiCaL 2.0.0 source, used by `proofmin --cadical` to complete partial derivations with CaDiCaL instead of the built-in resolution engine.
- `data/`: a handful of small synthetic instances (`rsmu_*.cnf`, `ssmu_*.cnf`) used as development examples.
- `benchmark/`, `experiments/` — the scripts, `gourd` job configs and R scripts used to generate the paper's benchmark sets and figures on our cluster. These are included for reproducibility/transparency; they reference cluster-specific paths and external tools (`cnfgen`, `muser2`, `drat-trim`, `lrat-trim`, `gourd`) and are not required to build or run `proofmin` itself.

## Building

Requires a recent stable Rust toolchain (`cargo`) and a C/C++ compiler for `rustsat-cadical` to compile the vendored CaDiCaL sources:

```sh
cargo build --release --workspace
```

Binaries are produced at `target/release/proofmin` and `target/release/lrat-score`. `.cargo/config.toml` sets `-Ctarget-cpu=native`; if you plan to run the binary on a different machine than the one it was built on, override this.

### Optional: Forqes

By default (i.e. unless `--trivial-bounding` is passed), `proofmin` uses [Forqes](https://alexeyignatiev.github.io/) to compute smallest-MUS lower bounds for subproblems larger than `--max-brute-force` clauses (32 by default). Forqes is a separate binary that is **not** built by this repository and must be obtained separately (a Linux x86-64 build is linked from `proofmin --help`) and placed on your `PATH`, or pointed to with `--forqes-binary`. If it isn't available, `proofmin` will warn on startup but continue, and fall back on brute-force bounder.

## Quick start

```sh
target/release/proofmin data/rsmu_4_6_1.cnf
```

This writes the best discovered proof, in `tracecheck` format, to stdout (use `-o proof.tracecheck` to write it to a file instead), and logs the proof length and lower bound to stderr (`RUST_LOG=info` for progress logging during the search).

## ⚠️ Runtime: the default mode is a complete, unbounded search

`proofmin`'s default configuration performs a complete branch-and-bound search: it keeps splitting the formula into subproblems and improving its bound until it can *prove* the returned proof is shortest possible. This binary does not stop early unless you tell it to; there is no default time
limit (`--time-limit-seconds`/`-t`), no cap on the number of subproblems explored (`--max-subproblems-per-step`, `--max-total-subproblems`), and the non-trivial SMUS bounder (`Forqes`/branch-and-bound) is used unless `--trivial-bounding` is given. This is intentional, because the point of the paper is to describe a complete optimization strategy, but it also means that
on non-trivial inputs, a default run can legitimately take a very long time. `test/cnf/full6.cnf` from the CaDiCaL regression suite (6 variables, 64 clauses, essentially the full truth table over 6 variables restricted to one polarity) is one such adversarial case for the branch-and-bound bounder, which is why a default run on it can take hours; this is expected behavior, not a bug or a hang.

For a quick look at the tool, use one of:

- **Anytime mode**: add `-t SECONDS` (`--time-limit-seconds`). `proofmin` will return the best proof found within the budget and report the best lower bound established so far; the proof may then not be certified optimal.
- **Incomplete mode**: add `--trivial-bounding` (skip the Forqes-based SMUS bounder in favor of cheap bounds only) together with `--max-subproblems-per-step` and `--max-total-subproblems` to cap the branching factor and total search size. This is the configuration we used for the larger, real-world SAT Competition-scale instances in the paper:

  ```sh
  target/release/proofmin -t 3600 --seed 0 -s --cadical --trivial-bounding \
    --max-subproblems-per-step 10 --max-total-subproblems 10000 formula.cnf
  ```

  (see `experiments/run/scripts/proofmin-competition.sh`). `--cadical` also
  helps: it completes partial derivations with CaDiCaL instead of the
  built-in resolution engine, which is generally faster.

## CLI reference

Run `proofmin --help` for the authoritative, up-to-date list. Summary:

| Flag | Effect |
|---|---|
| `formula_path` | Unsatisfiable CNF in DIMACS format (`.cnf`, or `.cnf.xz` for xz-compressed input). |
| `-t`, `--time-limit-seconds` | Wall-clock budget; without it the search runs to completion. |
| `--trivial-bounding` | Disable the Forqes-based SMUS bounder; use only cheap, search-free bounds. Faster but weaker pruning. |
| `--use-cover-bound` | Use assignment-cover strengthening for the search-less (trivial) bounds. |
| `--max-brute-force N` (default 32) | Formulas with at most `N` clauses use a brute-force SMUS bounder instead of Forqes. |
| `--max-subproblems-per-step N` | Cap subproblems created per branch-and-bound step (makes the algorithm incomplete). |
| `--max-total-subproblems N` | Cap the total subproblem queue size (reduces OOM risk, also makes the algorithm incomplete). |
| `--forqes-binary PATH` | Path to the Forqes executable (default: look up `forqes` on `PATH`). |
| `--forqes-no-file-io` | Feed Forqes via stdin instead of temp files (faster, but can trigger a Forqes stdio bug). |
| `-s`, `--shuffle-sat` | Randomize variable order in completion (SAT-solver) calls. |
| `--cadical` | Use CaDiCaL (rather than the built-in resolution engine) to complete partial derivations. |
| `--seed N` | Random seed. |
| `--ascending-length-partition`, `--ascending-frequency` | Alternative clause orderings used when partitioning subproblems. |
| `--complete-backoff-base X` (default 1.0) | Multiplicatively back off the interval between completion calls after each one. |
| `--bounding-time-limit-ms N` (default 1000) | Time budget for a single bounding call. |
| `-o`, `--output-file PATH` | Write the best proof (tracecheck format) here instead of stdout. |

## `lrat-score`

```sh
target/release/lrat-score formula.cnf proof.lrat [-d]
```

Parses an LRAT proof against its CNF, reports the number of axioms, derived lemmas and RAT steps, and (with `-d`) a JSON breakdown of duplicate clause derivations. We used this to compute the reference proof lengths that `proofmin`'s output is compared against in the paper.
