Blog

This is the fourth post in my series about refactoring varisat. In the last post we saw how conflict driven clause learning works, in this post we’re going to make it fast. To get there we add several smaller features that were already present in varisat 0.1. While there are still some things missing that varisat 0.1 supports, these are features like proof generation or incremental solving that don’t affect the solving performance.

This means you can solve some non-trivial instances using varisat 0.2 today. I haven’t made a new release on crates.io yet, but you can install it directly from github (replacing any previous version installed):

cargo install --force --git https://github.com/jix/varisat
varisat some_non_trivial_input_formula.cnf

One part of making the solver faster were low-level optimizations in the unit-propagation implementation. I won’t go into the details of that, but you can look at the new code. The bigger part were several heuristics that play a big role in making CDCL perform well. Below I will explain each implemented in varisat so far.

This is the third post in my series about refactoring varisat. In this post the new code base turns into a working SAT solver. While you can use the command line tool or the library to solve some small and easy SAT problems now, there is still a lot ahead to gain feature and performance parity with varisat 0.1.

In the last post we saw how unit propagation is implemented. When some variables are known, unit propagation allows us to derive the values of new variables or finds a clause that cannot be satisfied. Unit propagation alone isn’t enough though, as there is no guarantee to make progress. To continue the search for a satisfying solution after propagating all assignments, it is necessary to make a guess. A natural way to handle this would be recursion and backtracking. This would give us a variant of the DPLL algorithm from which conflict driven clause learning evolved.

This is the second post in my series about refactoring varisat. Since the last post I started implementing some of the core data structures and algorithms of a CDCL based SAT solver: clause storage and unit propagation. In this post I will explain how the these parts work and the rationale behind some of the decisions I made.

This is the first post in a series of posts I plan to write while refactoring my SAT solver varisat. In the progress of developing varisat into a SAT solver that can compete with some well known SAT solvers like minisat or glucose, it accumulated quite a bit of technical debt. Varisat is the first larger project I’ve written in rust and there a lot of things I’d do differently now. Before I can turn varisat into a solver that competes with the fastest solvers out there, I need to do some refactoring.

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.

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.

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.

Earlier this year, in October, a new widespread cryptography vulnerability was announced. The initial announcement didn’t contain details about the vulnerability or much details on how to attack it (updated by now). It did state the affected systems though: RSA keys generated using smartcards and similar devices that use Infineon’s RSALib. The announcement came with obfuscated code that would check whether a public key is affected. Also, the name chosen by the researchers was a small hint on how to attack it: “Return of Coppersmith’s Attack”.

I decided to try and figure out the details before the conference paper describing them would be released. By the time the paper was released, I had reverse engineered the vulnerability and implemented my own attack, which did not use Coppersmith’s method at all. This post explains how I figured out what’s wrong with the affected RSA-keys and how I used that information to factor affected 512-bit RSA-keys.

This is a write-up of the polygon renderer used for the Mega Drive demo “Overdrive 2” by Titan, released at the Revision 2017 Demoparty. As the Mega Drive can only display tilemaps, not bitmaps, and does not have the video memory mapped into the CPU address space, this turned out to be an interesting problem. If you have not seen the demo yet, I recommend watching it before continuing. You can find a hardware capture on YouTube: