Everything that is needed to build is MIT licensed. The M4RI library (not included) is unfortunately GPL, so in case you have M4RI installed, you must build with -DNOM4RI=ON
or -DMIT=ON
in case you need a pure MIT build.
sudo apt-get install build-essential cmake git
sudo apt-get install zlib1g-dev libsqlite3-dev
sudo apt-get install libboost-program-options-dev
sudo apt-get install python3-pip
sudo pip3 install sklearn pandas numpy lit matplotlib
git clone https://github.com/msoos/cryptominisat
cd cryptominisat
git checkout crystalball
git submodule update --init
mkdir build && cd build
ln -s ../scripts/crystal/* .
ln -s ../scripts/build_scripts/* .
We will train on this CNF
wget https://www.msoos.org/largefiles/goldb-heqc-i10mul.cnf.gz
gunzip goldb-heqc-i10mul.cnf.gz
Gather the data, create labels, create the classifier, generate C++ and build the final SAT solver
./crystalball.sh goldb-heqc-i10mul.cnf
[...compilations and the full data pipeline...]
We are using configuration short:3 long:3
./cryptominisat5 --predshort 3 --predlong 3 goldb-heqc-i10mul.cnf
[ ... ]
s UNSATISFIABLE
cd goldb-heqc-i10mul.cnf-dir
sqlite3 mydata.db
sqlite> select count() from sum_cl_use;
94507