This variant of CaDiCaL 1.8.0 SAT Solver has SHA-256 cryptanalysis routines embedded. The purpose of this project is to find SHA-256 semi-free-start collisions more efficiently than a pure CaDiCaL approach.
Please note that this solver is designed to only work with specific SAT encodings, specifically the SHA-256 Collision Encoder by Saeed Nejati.
By default, the programmatic techniques are turned off and the encoding type isn't specified. To provide the information, please edit the pre-processor directives in the src/sha256/types.hpp file.
To build the project, you can use CMake (recommended) or the original CaDiCaL build scripts.
If you want to build through CMake, run the following command in the root of this project:
cmake -Bbuild . && cmake --build buildIf you want to build using the original CaDiCaL way, run the following command in the root of this project:
./configure && makeThe SAT solutions can be verified from the log file of the solver (and the
encoding) using a Python
script.
For example, if you have a log file log.txt and an encoding file
encoding.cnf, the following command can verify the solution:
python verify_from_log.py encoding.cnf < log.txtExisting benchmarks with and without the programmatic techniques are available in this GitHub repository. The programmatic SAT results should be reproducible with this variant of the programmatic SAT solver with the respective configurations.