Skip to content


Switch branches/tags

Name already in use

A tag already exists with the provided branch name. Many Git commands accept both tag and branch names, so creating this branch may cause unexpected behavior. Are you sure you want to create this branch?

Latest commit


Git stats


Failed to load latest commit information.
Latest commit message
Commit time

sha1-sat -- SAT instance generator for SHA-1


To compile, you first need to make sure you have the Boost libraries installed. When you do, simply run



To generate a CNF instance encoding a preimage attack on the full SHA-1 algorithm, run:

./main --cnf --rounds=80 --hash-bits=160 > instance.cnf

To look at the possible options, run:

./main --help

The program can also generate OPB instances (pseudo-boolean constraints) if you specify --opb instead of --cnf.

Verifying solutions

To verify that the solution output by the solver is actually correct, run:

perl verify-preimage instance.cnf solution | ./verify-preimage

Here, 'solution' is the file output e.g. by minisat or the 'v'-line for other popular solvers like CryptoMiniSAT or PrecoSAT. The program returns an error code of 0 if and only if the solution is correct.

Using espresso

Part of the encoding used by this program is generated using the logic minimiser espresso. In particular, it is used to minimise the truth tables for half-adders.

You used to be able to obtain espresso from, but it is no longer available there. As a consequence, I have decided to move the dependency on espresso "out of line" and provide the precomputed output tables (see the data/ subdirectory).

If you wish to regenerate these tables (or if you would like to encode them for adders with different number of operands), this is how you would use espresso:

tar xzvf espresso-ab-1.0.tar.gz
(cd espresso-ab-1.0 && ./configure && make)

g++ -std=c++ -o mkhalfadder
./mkhalfadder 2 2 | espresso-ab-1.0/src/espresso > data/halfadder-2-2.out.txt


I developed this program as part of my master thesis. You can find it here:

The program creates the smallest and easiest-to-solve instances that I know about; in particular, it uses a novel encoding of adders which is described in more detail in my short benchmark description "Instance generator for encoding preimage, second-preimage, and collision attacks on SHA-1", which you can find on page 119 of the SAT Competition 2013 proceedings:

Please e-mail comments, suggestions, etc. to me at

If you use the program in your research, please make a note of this in your acknowledgements and let me know about your paper/thesis/etc.!


SAT instance generator for SHA-1







No releases published


No packages published