Jix' Site


Introducing partial_ref

Recently there has been some discussion about interprocedural borrowing conflicts in rust. This is something I’ve been fighting with a lot, especially while working on my SAT solver varisat. Around the time Niko Matsakis published his blog post about this, I realized that the existing workarounds I’ve been using in varisat have become a maintenance nightmare. Making simple changes to the code required lots of changes in the boilerplate needed to thread various references to the places where they’re needed.
[Read More]

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]