Jix' Site


Encoding Matrix Rank for SAT Solvers

I’m working on a problem where I want to use a SAT solver to check that a property $P(v_1, \ldots, v_n)$ holds for a bunch of vectors $v_1, \ldots, v_n$, but I don’t care about the basis choice. In other words I want to check whether an arbitrary invertible linear transform $T$ exists so that the transformed vectors have a certain property, i.e. $P(T(v_1), \ldots, T(v_n))$. I solved this by finding an encoding for constraining the rank of a matrix. With that I can simply encode $P(M v_1, \ldots, M v_2)$ where $M$ is a square matrix constrained to have full rank and which therefore is invertible.

[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]