Companion page for the paper "Optimizing a Verified SAT Solver"

Table of Contents

The draft can be found at https://people.mpi-inf.mpg.de/~mfleury/paper/optimised_isasat.pdf.

1 IsaSAT

Please refer to the README https://bitbucket.org/isafol/isafol/src/master/Weidenbach_Book.

2 Link between Article and Formalization

2.1 Section 3, IsaSAT

  • The CDCL layer corresponds to the file CDCL_W.thy. The locales are instantiatied in CDCL_W_Abstract_State.thy.
  • TWL is in Watchel_Literals_Transition_System.thy. The Ignore rule can be found is the file under the name delete_from_working.
  • The third layer is in Watchel_Literals_Algorithm.thy.
  • Lists are introduced in Watchel_Literals_List.thy.
  • Watch lists are introduced in Watchel_Literals_Watch_List.thy and the domain is introduced in Watchel_Literals_Watch_Domain_List.thy.
  • The heuristics are defined and added in the files IsaSAT_*.thy and Watchel_Literals_VMTF.

2.2 Section 4, Refactoring IsaSAT

  • The explore tactic can be found in ../lib/Explorer.thy

2.3 Section 5, Adding Blocking Literals

  • The invariant is called twl_lazy_update in Watchel_Literals_Transition_System.thy. It is a bit stronger than the version mentionned in the paper.

2.4 Section 6, Arena Module

  • The module is defined is IsaSAT_Arena.thy.
  • The function find_inwatched in IsaSAT_Inner_Propagation.thy shows the abstract behaviour with the switch when to use position saving. It is the refined to the function isa_find_unwatched that is synthesized under the name isa_find_unwatched_between_code and later exported.

2.5 Section 7, Restarts and Forget

  • The restart and forget follow the same structure as the refinement, but contain _Restart in the file name.
  • In the file Watched_Literals_Watch_List_Restart.thy, the functions containing GC have not yet been refined to code.

2.6 Section 8, Machine Words

  • In IsaSAT_Restart, cdcl_twl_stgy_restart_prog_early_wl_heur is the function with the switch,
  • In the same file, cdcl_twl_stgy_restart_prog_wl_heur_fast_code and cdcl_twl_stgy_restart_prog_wl_heur_code correspond to the two version of the SAT solver.
  • The 5 headers are:
    • the saved position;
    • the status;
    • the activity and a boolean indicating whether the clause was used (the activity is used for ties of the LBD);
    • the LBD;
    • the size.

2.7 Section 9, Evaluation

  • See below for the detailed results.
  • Some variations can be tested by switching the options --nobounded, --norestart, and --noreduction can deactivate the mode the use of 64 words, restarts, and reduction. For other versions, the formalization must be changed.

2.8 Section 10, Discussion and Related Work

  • The encoding uint64 * uint32 * bool to uint64 * uint64 can be found in the theory IsaSAT_Watch_List.thy (and in the conflict analyses, where it, howevere, did not have an impact).
  • To try the profiling:
mlton -verbose 1 -default-type int64 -output IsaSAT -profile alloc -profile-branch true -codegen native -inline 700 -cc-opt -O3 IsaSAT.mlb

3 Benchmarks

The results can be downloaded below with some additional statistics on the runs.

3.1 Preprocessing

  • cryptominisat was used with the default options, e.g.:
./cryptominisat5 -p1 input.cnf simplified.cnf

3.2 Optimisation Benchmark

Reduction Restart Position Saving Machine words Results
        ./v30_nopos_nobound_nored_nores.csv
      ✔ ./v30_nopos_nobound_nores.csv
    ✔   ./v30_nobounded_nored_nores.csv
    ✔ ✔ ./v30_nored_nores.csv
  ✔     ./v30_nopossaving_nobounded.csv
  ✔   ✔ ./v30_nopossaving_nored.csv
  ✔ ✔   ./v30_nobounded_nored.csv
  ✔ ✔ ✔ ./v30_nored.csv
        ./v30_nopos_nobounded_nores.csv
✔     ✔ ./v30_nopossaving_nores.csv
✔   ✔   ./v30_nobounded_nores.csv
✔   ✔ ✔ ./v30_nores.csv
✔ ✔     ./v30_nopos.csv
✔ ✔   ✔ ./v30_nopossaving.csv
✔ ✔ ✔   ./v30_nobounded.csv
✔ ✔ ✔ ✔ ./v30.csv

3.3 Comparison with other solvers

Solver Results Results without simplification
Glucose ./glucose.csv ./glucose_nosimp.csv
CaDiCaL ./cadical.csv ./cadical_nosimp.csv
MiniSAT ./minisat.csv ./minisat_nosimp.csv
MicroSAT ./microsat.csv  
IsaSAT-30, fixed heuristic ./v32_fixed_heuristic.csv  
IsaSAT-17 ./v17.csv  
versat ./versat.csv  

The options for the version without simplification are:

  • Glucose:
-no-pre -no-elim -no-rcheck -no-asymm
  • MiniSAT:
-no-pre -no-elim -no-rcheck -no-asymm
  • CaDiCaL:
--no-vivify --no-transred --no-subsume --no-simplify --no-strengthen --no-probe --no-hbr --no-decompose --no-elim
  • CryptoMiniSAT:
--transred 0 --probe 0 --schedsimp 0 --distill 0

3.4 Other Benchmarks

Imprint / Data Protection