Jix' Site

Sat

Varisat 0.1.3: LRAT Generation and Proof Trimming

I’ve released a new version of my SAT solver Varisat. It is now split across two crates: one for library usage and one for command line usage.

The major new features in this release concern the genration of unsatisfiability proofs. Varisat is now able to directly generate proofs in the LRAT format in addition to the DRAT format. The binary versions of both formats are supported too. Varisat is also able to do on the fly proof trimming now. This is similar to running DRAT-trim but processes the proof while the solver runs.

[Read More]

Introducing Varisat

I’ve been interested in SAT solvers for quite some time. These are programs that take a boolean formula and either find a variable assignment that makes the formula true or find a proof that this is impossible. As many difficult problems can be rephrased as the satisfiability of a suitable boolean formula, SAT solvers are incredibly versatile und useful. I’ve recently finished and now released a first version of my SAT solver, Varisat, on crates.io.

[Read More]