Varisat is a CDCL based SAT solver written in rust. Given a boolean formula in conjunctive normal form, it either finds a variable assignment that makes the formula true or finds a proof that this is impossible.

Varisat is open source software. You can find the Varisat project on GitHub.

Varisat is available as a rust library (varisat on crates.io) and as a command line solver (varisat-cli on crates.io).

In addition to this user manual, Varisat comes with an API documentation.

The command line solver can be installed or updated using cargo install --force varisat-cli. Cargo can be installed using rustup.

The command line solver is also available as a pre-compiled binary for Linux and Windows.

Varisat follows the basic conventions used by most other SAT solvers. If you've used a SAT solver before, you'll likely know how to use varisat. If you haven't, you can read the next chapter to learn how to use varisat. In any case make sure to check out the built in command line help using varisat --help.

The command line solver reads and solves a single formula. The file name of the formula to solve is passed as an argument on the command line. If no file is specified, Varisat will read a formula from the standard input. The formula is parsed as a DIMACS CNF file.

During the solving process, Varisat will print some statistics on lines starting with c. In general it is not possible to infer the solving process from these statistics and it is not necessary to understand them to use a SAT solver. They are intended for the expert user and solver developers who are familiar with the solver's internals.

Solving an instance can take from milliseconds to forever and anything in between. There is no known algorithm that will efficiently solve all possible SAT formulas. Nevertheless the algorithms and heuristics used by SAT solvers are often successful. Most of the time it's not possible to tell whether they are effective for a given formula.

If Varisat is able to find a satisfying assignment or is able to determine that there is no such assignment, it will print a solution line. This is either s SATISFIABLE or s UNSATISFIABLE depending on the verdict.

If there is a satisfying assignment it will be output on lines starting with v, followed by a list of literals. Assigning these literals to true will make the input formula true.

The exit code of the solver will also indicate the solver's verdict. When the formula is satisfiable, the exit code 10 will be returned. When it is unsatisfiable the exit code will be 20.

In the next chapter we will see how to generate a proof of unsatisfiability in case no satisfying assignment exists.

This shows an example run for the satisfiable formula sgen1_sat_90_0.cnf:

$ varisat sgen1_sat_90_0.cnf
c This is varisat [...]
c   release build - rustc [...]
c Reading file 'sgen1_sat_90_0.cnf'
c Parsed formula with 90 variables and 216 clauses
c [...]
s SATISFIABLE
v 1 -2 -3 -4 -5 -6 -7 8 -9 -10 11 -12 -13 -14 -15 -16 17 -18 -19 -20 -21 22 -23 -24 -25 -26 -27 -28 29 -30 -31 32 -33 -34 -35 -36 -37 -38 -39 40 -41 -42 43 -44 -45 46 -47 -48 -49 -50 -51 52 -53 -54 -55 -56 -57 -58 -59 60 -61 62 -63 -64 -65 -66 -67 68 -69 -70 -71 -72 -73 -74 75 -76 -77 78 -79 -80 -81 -82 -83 84 -85 -86 -87 -88 89 -90 0

This shows an example run for the unsatisfiable formula sgen1_unsat_57_0.cnf:

$ varisat sgen1_unsat_57_0.cnf
c This is varisat [...]
c   release build - rustc [...]
c Reading file 'sgen1_unsat_57_0.cnf'
c Parsed formula with 57 variables and 124 clauses
c [...]
s UNSATISFIABLE

SAT solvers are often used to for problems where correctness is critical. For this reason SAT solvers are expected to produce proofs of unsatisfiability. Such proofs allow us to independently check the solver's result.

Varisat allows generating proofs in three different formats:

To generate a proof, invoke Varisat with the --proof option followed by a target file name. By default Varisat generates proofs in its own custom proof format. This can be changed by using the --proof-format option followed by one of varisat, drat, binary-drat, lrat or clrat (binary variant of lrat).

Varisat has a built in checker for its own proof format. For the other formats see the chapters linked from the overview table. While the proof checker is built-in, it shares very little code with the solver. This makes it unlikely for the same bug to affect checker and solver. The proof format is not stable between version. Thus a proof produced by a sufficiently different version of Varisat will most likely be rejected as invalid.

The builtin proof checker is available using the --check subcommand. Subcommands have to be the first argument passed on the command line. The input formula and proof file are specified in the same way used for solving, except that the proof parameter is required for checking.

If the proof checker is able to successfully verify the proof, it will print the line s VERIFEID. Otherwise an error will be printed and a non-zero exit code returned.

The proof checker also has a a built in command line help that can be accessed using varisat --check --help.

Varisat can run its built in checker concurrently with the solver. This avoids the storage requirements for a proof file, which can become prohibitive for long running instances. It also allows aborting a solve as soon as an error occurred, producing relevant debugging information. This is enabled by passing the --self-check option to the solver.

Varisat proof files can be converted into the LRAT format during checking. In fact, internally, if LRAT proofs are generated during solving, they are generated by enabling self checking and conversion into LRAT. With this a verified LRAT proof checker can be used.

To the author's knowledge besides Varisat the only other way of producing LRAT proofs is by generating DRAT proofs. Converting DRAT proofs into LRAT proofs often takes longer than solving the instance in the first place. Conversion from Varisat proof files to LRAT is very efficient and much faster than the alternative.

To convert a Varisat proof, when invoking varisat --check, simply pass the --write-lrat or --write-clrat option followed by a target file name.

This shows an example run for the unsatisfiable formula sgen1_unsat_57_0.cnf:

$ varisat sgen1_unsat_57_0.cnf --proof sgen1_unsat_57_0.varisat
c This is varisat [...]
c   release build - rustc [...]
c Reading file 'sgen1_unsat_57_0.cnf'
c Writing varisat proof to file 'sgen1_unsat_57_0.varisat'
c [...]
s UNSATISFIABLE

Checking the proof:

$ varisat --check sgen1_unsat_57_0.cnf --proof sgen1_unsat_57_0.varisat
c This is varisat [...]
c   release build - rustc [...]
c Reading file 'sgen1_unsat_57_0.cnf'
c Parsed formula with 57 variables and 124 clauses
c Checking proof file 'sgen1_unsat_57_0.varisat'
c checking step 100k
s VERIFIED

This section of the manual assumes basic familiarity with SAT solving. If you're new to SAT solving, familiarizing yourself with the command line solver, described in the previous section, is recommended.

The Varisat library is available on crates.io as the varisat crate. The API documentation can be viewed on docs.rs.

SAT solvers operate on formulas in conjunctive normal form (CNF). The Varisat library comes with types to efficiently store CNF formulas. This is independent from loading a formula into the solver. This is useful for writing custom code that processes CNF formulas. It also simplifies writing code that generates a formula to either directly solve it or alternatively write it to a file.

To build formulas in conjunctive normal form, we need to start with variables and literals. For this Varisat provides the types Var and Lit.

A variable is identified by an integer. The convention used for input and output of variables follows the DIMACS CNF format and is 1-based. A literal is a variable or a negated variable. In the DIMACS format negative literals are represented by negative integers.

Internally variables are numbered starting with zero. This matches the array indexing convention used by Rust. The 0-based number of a variable is called index, while the 1-based number is called dimacs. Literals are also represented by a non-negative number called the code. A literal's code is the corresponding variable's index shifted to the left by one. The least significant bit is set if the literal is negative.

The Var and Lit types come with methods to convert between the representations. Note that Lit::index returns the corresponding variable's index, not the literal's code.

# #![allow(unused_variables)]
#fn main() {
# extern crate varisat;
use varisat::lit::{Var, Lit};

let x = Var::from_index(0);

assert_eq!(x, Var::from_dimacs(1));
assert_eq!(x.index(), 0);
assert_eq!(x.to_dimacs(), 1);

assert!(Lit::from_dimacs(2).is_positive());
assert!(Lit::from_dimacs(-3).is_negative());

assert_eq!(Lit::positive(x), Lit::from_var(x, false));
assert_eq!(Lit::negative(x), Lit::from_var(x, true));

assert_eq!(Lit::negative(x), !Lit::positive(x));

assert_eq!(Lit::from_index(6, false).code(), 12);
assert_eq!(Lit::from_index(6, true).code(), 13);

assert_eq!(Lit::from_code(13).var(), Var::from_dimacs(7));
assert_eq!(Lit::from_code(13).index(), 6);
#}

When formatting variables or literals the DIMACS convention is used.

# #![allow(unused_variables)]
#fn main() {
# extern crate varisat;
# use varisat::lit::{Var, Lit};

let fmt_display = format!("{}, {}", Var::from_dimacs(5), Lit::from_dimacs(-1));
let fmt_debug = format!("{:?}, {:?}", Var::from_dimacs(5), Lit::from_dimacs(-1));

assert_eq!(fmt_display, "5, -1");
assert_eq!(fmt_debug, "5, -1");
#}

A CNF formula is a conjunction of clauses and a clause a disjunction of literals. This means we can represent a formula as a set of sets of literals.

By arbitrarily ordering the elements of the sets, we could use a Vec<Vec<Lit>> to represent a formula. Such a representation has too much memory overhead per clause though. Each clause requires a separate allocation, which also hurts cache locality when iterating over the clauses of a large formula.

Instead Varisat provides the CnfFormula type, which stores all literals in a single Vec. When iterating over a CnfFormula the clauses can be accessed as slices.

# #![allow(unused_variables)]
#fn main() {
# extern crate varisat;
# use varisat::lit::{Var, Lit};
use varisat::cnf::CnfFormula;

let mut formula = CnfFormula::new();

let (a, b, c) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));

formula.add_clause(&[a, b, c]);
formula.add_clause(&[!a, !b]);
formula.add_clause(&[!b, !c]);
formula.add_clause(&[!a, !c]);

assert_eq!(formula.iter().last().unwrap(), &[!a, !c]);
#}

Varisat provides routines for parsing and writing Formulas in the DIMACS CNF format.

# #![allow(unused_variables)]
#fn main() {
# extern crate varisat;
# use varisat::lit::{Var, Lit};
use varisat::dimacs::{DimacsParser, write_dimacs};

let input = b"p cnf 3 2\n1 2 3 0\n-1 -3 0\n";

let implements_read = &input[..];

let mut formula = DimacsParser::parse(implements_read).expect("parse error");

formula.add_clause(&[Lit::from_dimacs(2)]);

let mut implements_write = vec![];

write_dimacs(&mut implements_write, &formula);

assert_eq!(implements_write, b"p cnf 3 3\n1 2 3 0\n-1 -3 0\n2 0\n");
#}

To solve a formula, we start with creating a SAT solver object.

# #![allow(unused_variables)]
#fn main() {
# extern crate varisat;
use varisat::solver::Solver;

let mut solver = Solver::new();
#}

We can load a formula by adding individual clauses:

# #![allow(unused_variables)]
#fn main() {
# extern crate varisat;
# use varisat::solver::Solver;
# let mut solver = Solver::new();
use varisat::lit::Lit;

let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));

solver.add_clause(&[x, y, z]);
solver.add_clause(&[!x, !y]);
solver.add_clause(&[!y, !z]);
#}

By adding a formula:

# #![allow(unused_variables)]
#fn main() {
# extern crate varisat;
# use varisat::solver::Solver;
# use varisat::lit::Lit;
# let mut solver = Solver::new();
# let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));
use varisat::cnf::CnfFormula;
let mut formula = CnfFormula::new();
formula.add_clause(&[x, y, z]);
formula.add_clause(&[!x, !y]);
formula.add_clause(&[!y, !z]);

solver.add_formula(&formula);
#}

Or by directly loading a DIMACS CNF from anything that implements std::io::Read. This uses incremental parsing, making it more efficient than reading the whole formula into a CnfFormula.

# #![allow(unused_variables)]
#fn main() {
# extern crate varisat;
# use varisat::solver::Solver;
# let mut solver = Solver::new();
let dimacs_cnf = b"1 2 3 0\n-1 -2 0\n-2 -3 0\n";

solver.add_dimacs_cnf(&dimacs_cnf[..]).expect("parse error");
#}

After loading a formula, we can ask the solver to find a solution:

# #![allow(unused_variables)]
#fn main() {
# extern crate varisat;
# use varisat::solver::Solver;
# let mut solver = Solver::new();
# let dimacs_cnf = b"1 2 3 0\n-1 -2 0\n-2 -3 0\n";
# solver.add_dimacs_cnf(&dimacs_cnf[..]).expect("parse error");
let solution = solver.solve().unwrap();

assert_eq!(solution, true); // satisfiable
#}

While the solve method returns a Result, in the default configuration it cannot fail. This means it is safe to unwrap the result here.

We might not only be interested in whether the formula is satisfiable, but also want to know a satisfying assignment. With the Solver::model method, we can query the solver for a set of assignments that make all clauses true.

# #![allow(unused_variables)]
#fn main() {
# extern crate varisat;
# use varisat::solver::Solver;
# use varisat::lit::Lit;
# let mut solver = Solver::new();
# let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));
# let dimacs_cnf = b"1 2 3 0\n-1 -2 0\n-2 -3 0\n";
# solver.add_dimacs_cnf(&dimacs_cnf[..]).expect("parse error");
# let solution = solver.solve().unwrap();
let model = solver.model().unwrap(); // None if solve didn't return Ok(true)

assert!(model.contains(&x) || model.contains(&y) || model.contains(&z));
assert!(model.contains(&!x) || model.contains(&!y));
assert!(model.contains(&!y) || model.contains(&!z));
#}

Incremental solving means changing and re-solving a formula multiple times, without starting the search from scratch. This can save a lot of time, when many related formulas that differ only slightly have to be solved.

Varisat supports two features that enable incremental solving. These are incremental clause additions and solving under assumptions.

Incremental clause additions simply means that further calls to Solver::add_clause, Solver::add_formula or Solver::add_dimacs_cnf are allowed after Solver::solve returned. The new clauses are added to the clauses that were already present prior to the last solve call.

# #![allow(unused_variables)]
#fn main() {
# extern crate varisat;
use varisat::solver::Solver;
use varisat::lit::Lit;

let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));

let mut solver = Solver::new();
solver.add_clause(&[!x, y]);
solver.add_clause(&[!y, z]);
assert_eq!(solver.solve().unwrap(), true);

solver.add_clause(&[!z, x]);
assert_eq!(solver.solve().unwrap(), true);

solver.add_clause(&[!z, !y]);
solver.add_clause(&[z, y]);
assert_eq!(solver.solve().unwrap(), false);
#}

Once clauses are added to the solver they cannot be removed anymore. Instead assumptions can be used to limit the search to a subset of solutions. Assumptions fix the values of certain variables. This is equivalent to adding some unit clauses to the formula, with the difference that assumptions can be removed again.

Assumptions are set by calling Solver::assume, which replaces any previous assumptions.

Using additional helper variables, assumptions can be used to emulate removable clauses:

# #![allow(unused_variables)]
#fn main() {
# extern crate varisat;
use varisat::solver::Solver;
use varisat::lit::Lit;

let (x, y, z) = (Lit::from_dimacs(1), Lit::from_dimacs(2), Lit::from_dimacs(3));
let ignore_clauses = Lit::from_dimacs(4);

let mut solver = Solver::new();
solver.add_clause(&[!x, y]);
solver.add_clause(&[!y, z]);
assert_eq!(solver.solve().unwrap(), true);

solver.add_clause(&[!z, x]);
assert_eq!(solver.solve().unwrap(), true);

solver.add_clause(&[ignore_clauses, !z, !y]);
solver.add_clause(&[ignore_clauses, z, y]);

solver.assume(&[!ignore_clauses]);
assert_eq!(solver.solve().unwrap(), false);

solver.assume(&[]); // Clears assumptions
solver.add_clause(&[ignore_clauses]);

assert_eq!(solver.solve().unwrap(), true);
#}

When a formula is unsatisfiable under multiple assumptions, Varisat may be able to find a smaller set of assumptions that is sufficient for unsatisfiability. Such a sufficient subset of assumptions can be retrieved using Solver::failed_core.

This section contains descriptions of the file formats used by Varisat.

The DIMACS CNF format is a textual representation of a formula in conjunctive normal form. A formula in conjunctive normal form is a conjunction (logical and) of a set of clauses. Each clause is a disjunction (logical or) of a set of literals. A literal is a variable or a negation of a variable. DIMACS CNF uses positive integers to represent variables and their negation to represent the corresponding negated variable. This convention is also used for all textual input and output in Varisat.

There are several variations and extensions of the DIMACS CNF format. Varisat tries to accept any variation commonly found. Currently no extensions are supported.

DIMACS CNF is a textual format. Any line that begins with the character c is considered a comment. Some other parsers require comments to start with c and/or support comments only at the beginning of a file. Varisat supports them anywhere in the file.

A DIMACS file begins with a header line of the form p cnf <variables> <clauses>. Where <variables> and <clauses> are replaced with decimal numbers indicating the number of variables and clauses in the formula.

Varisat does not require a header line. If it is missing, it will infer the number of clauses and variables. If a header line is present, though, the formula must have the exact number of clauses and may not use variables represented by a number larger than indicated.

Following the header line are the clauses of the formula. The clauses are encoded as a sequence of decimal numbers separated by spaces and newlines. For each clause the contained literals are listed followed by a 0. Usually each clause is listed on a separate line, using spaces between each of the literals and the final zero. Sometimes long clauses use multiple lines. Varisat will accept any combination of spaces and newlines as separators, including multiple clauses on the same line.

As an example the formula (x ∨ y ∨ ¬z) ∧ (¬y ∨ z) could be encoded as this:

p cnf 3 2
1 2 -3 0
-2 3 0

The simplified DIMACS CNF format used by the yearly SAT competitions is a subset of the format parsed by Varisat.

Varisat has its own custom proof format. The format is not documented and may change from version to version. Varisat comes with a built in checker for this format (command line and library).

The format is inspired by the LRAT format but replaces clause ids by clause hashes. This makes it simpler to generate and avoids any memory overhead during proof generation. More details can be found in this blog-post about Varisat proofs.

DRAT is the de-facto standard format for unsatisfiability proofs. It is required for solvers taking part in the yearly SAT competition. It is a minimal clausal proof format, that lists additions and removals of clauses. It does not contain any justification for clause additions. This makes DRAT proofs easy and efficient to generate, comparatively compact, but involves more work during checking.

DRAT has an ASCII and a binary encoding, both are supported by Varisat.

More information about it as well as proof checker can be found on the DRAT-trim page.

LRAT is a proof format that extends DRAT with additional information to simplify the checking of clause additions. This makes it possible to write efficient formally verified proof checkers.

LRAT is described in the paper "Efficient Certified RAT Verification" by Cruz-Filipe, Heule, Hunt, Kaufmann and Schneider-Kamp. The authors suggested generating LRAT proofs from DRAT proofs. Such a conversion requires checking the DRAT proof which is often very time consuming.

Varisat allows generating LRAT proofs starting from its own proof format. As Varisat's proof format is based on LRAT with modifications that allow simpler and faster proof generation, such a conversion is much faster. For the same solver and parameters, this results in a significant reduction in the overall time required for a formally verified unsatisfiability proof.

LRAT also has a more compact binary variant called CLRAT, both are supported by Varisat.

The ACL2 programming language and theorem prover distribution comes with an efficient formally verified CLRAT proof checker. It can be found in the subdirectory books/projects/sat/lrat/incremental.