Skip to content

Latest commit

 

History

History
205 lines (161 loc) · 8.3 KB

README.md

File metadata and controls

205 lines (161 loc) · 8.3 KB
Raw

rate

crates.io CircleCI branch

This is a proof checker that can verify proofs for SAT instances, just like fellow checkers drat-trim, dpr-trim or gratgen. The notable difference is that rate does not ignore deletions of unit clauses by default. You can cite our CPP 2020 conference paper (bibtex record here) which describes the problem that rate tries to solve.

Features

  • check DRAT proofs (default) and DPR proofs (file extension.pr or .dpr)
  • competitive performance (faster than drat-trim and dpr-trim, almost as fast as gratgen)
  • output a trimmed proof as DRAT, DPR, LRAT or GRAT after verifying a proof
  • check and output a SICK certificate of incorrectness after rejecting a proof
  • optionally ignore unit deletions for compatibility with drat-trim (flag --skip-unit-deletions)
  • transparently read compressed input files (Gzip, Zstandard, Bzip2, XZ, LZ4)
  • detect and report many errors like numeric overflows
  • mostly safe Rust, should not have any undefined behavior

Installation

Install Rust. Recent versions of stable Rust are supported (1.36 or later).

Stable version

Releases are hosted on crates.io and can be installed using cargo, Rust's package manager.

$ cargo install rate --force

After this has finished compiling, it will place the rate binary in ~/.cargo/bin/.

Building from source

Alternatively, you can install the development version from a checkout of this repository:

$ git clone https://github.com/krobelus/rate
$ cd rate
$ cargo install --path ./rate --force

Usage

Run the proof checker like this:

$ rate formula.cnf proof.drat

Whenever the proof is accepted, this will exit with code 0 after printing s VERIFIED and some metrics. See rate --help for more options.

SICK certificates

If rate rejects a proof, it checks a certificate of incorrectness that contains information on which proof step failed and why. The certificate can be written to a file with the -S option and checked separately with the sick-check binary which is much faster than a full proof checker (install sick-check using cargo install rate-sick-check for a stable version, or cargo install --path rate-sick-check to install from a local checkout). These certificates are useful to protect against bugs in the checker code.

Other utilities

Install the crate rate-proof-utils (just like rate or rate-sick-check) for some binaries that can be useful when working with clausal proofs:

  • drat2bdrat and bdrat2drat convert a DRAT proof to the Binary DRAT Format and vice versa. Also works for DPR proofs.
  • apply-proof applies a proof up to a given proof step, and outputs the accumulated formula as well as the rest of the proof. This can be very useful for delta-debugging a tool that works with proofs.

Unexpected rejections

If you are using a solver based on MiniSat, then your proof might be rejected by rate while it is accepted by other checkers, like drat-trim. This is because the proof can contain some clause deletions that are ignored by other checkers. There are two options:

  1. Use rate --skip-unit-deletions to make it behave like other checkers.

  2. Alternatively, you can patch your solver to not generate those extra deletions. This will make the proof valid for every checker. Look for reason deletions shrinking trail in the output of rate; this is the number of deletions in the proof that delete information - it should probably be zero, unless you are using certain advanced inprocessing techniques. Example patches that avoid these deletions: MiniSat (1 or 2) and MapleLCMDistChronoBT (1 or 2).

Caveats

Please note that rate accepts proofs that are technically not fully correct. Just like other checkers, we perform some transformations on the proof before actually verifying the proofs steps. This is done to improve performance. These transformations can ignore unnecessary clauses or proof steps. These are effectively removed from the formula or proof, respectively. This means that rate might accept a proof that contains lemmas that are not valid inferences, but this should never happen for satisfiable formulas.

Here are the transformations we do:

  • If --skip-unit-deletions is specified, then deletions of clauses that are unit with respect to the accumulated formula are ignored, as in drat-trim and gratgen.
  • When traversing the proof, we stop as soon as a conflict is inferred. Any proof steps thereafter are ignored. This means that an explicit empty clause at the end of the proof is not required.
  • Clauses and lemmas that are not part of the reason for above conflict are ignored, even if they could be resolution candidates, find an explanation why this is sound here.
  • RAT checks are done upon every possible pivot and not just the first literal in a clause, unless --assume-pivot-is-first is specified.

Tests

Run unit tests and the system test suite, respectively:

cargo test && ./test.py

You can also selectively run tests, for example use ./test.py -k default benchmarks/crafted benchmarks/sadical/add4.cnf to only run test functions matching default on the crafted benchmarks and on add4.{cnf,dpr}. See ./test.py -h for more options.

Above tests require

  • python3 (version 3.6 or above)
  • optionally any of the following executables:
    • lrat-check to validate the produced LRAT proofs.
    • pr2drat to produce DRAT and LRAT proofs from PR proofs.
    • gratchk to validate produced GRAT proofs.
    • If any of drat-trim, rupee, or gratgen are executable they will be run on the benchmarks and their verdicts will be compared to the output of rate.

You can use the docker image used by our CI which contains builds of above dependencies.

Documentation

Refer to our CPP 2020 conference paper or my thesis for some background information.

The source code includes an abundance of doc comments. Use this command to turn them into internal documentation at target/doc/rate*/index.html.

$ cargo doc --document-private-items --no-deps

Contributing

Please let us know if rate behaves in a way that is unexpected to you, or if you need some feature. We currently do not guarantee stability of the library modules in rate-common (only the binaries are considered an API), but we can integrate more tools that work on proofs in this repository.

Roadmap

Some possible improvements:

  • expose a Rust (and possibly C) API
  • support other clausal proof formats
  • compute other features about clausal proofs (e.g. the lifespan of clauses)
  • speed up handling of reason clause deletions that do not shrink the trail
  • speed up RAT checks by caching resolution candidates