SAT Solving Project 3: CDCL Solver

Required Python package: seaborn

---

• cdcl_solver.cpp

  cdcl_solver.cpp implements a CDCL SAT solver with watched literals and 1UIP clause learning. It has the following features:

  • The VSIDS and VMTF branching heuristics: For VSIDS, we have two variants. The first variant is by-the-book: new occurrences in conflict clauses don't directly affect the variable ordering, which are instead resorted from time to time. We still use the heap-based priority queue from our DPLL solver. Our second variant of VSIDS updates the score and position in the heap directly. For VMTF, we also make use of the heap. Instead of actually maintaining a list of variables, we simulate the move-to-front of VMTF by assigning the moved variables a bigger score than all other variables.
  • Clause Deletion: We implemented a deletion strategy based on a growing budget of learned clauses. We select the clauses to be delted based on their size and their number of unassigned literals.
  • Restarts: We implemented a fixed and a geometric restart policy. We also do phase-saving both for restars and for normal backtracking.
  • Learned clauses are minimized by self-subsuming resolution with reason clauses.
  • Preprocessing techniques: equivalence substitution, NiVER, subsumption testing and self-subsuming resolution. For satisfiable formulas we reconstruct the satisfying assignments from the sequence of eliminated variables and clauses.
  • Certificates for unsatisfiable instances in DRAT format. This also works with our preprocessing techniques.

  To compile cdcl_solver.cpp:

  clang++ -std=c++17 -O3 -DNDEBUG -o cdcl_solver cdcl_solver.cpp
  

  Then you will find the cdcl_solver executable file in your directory.

  To run cdcl_solver:

  ./cdcl_solver <path to a cnf file> [options]
  

  Branching heuristics: -vsids1 use the VSIDS heuristic (by-the-book implementation) -vsids2 use the VSIDS heuristic (directly update the score in the heap) -vmtf use the VMTF heuristic

  Preprocessing steps, one phase for each passed flag, so order and repetition of the flags matters: -equisub apply equivalence substitution in preprocessing -niver apply NiVER in preprocessing -subs apply subsumption testing in preprocessing -selfsubs apply self-subsuming resolution in preprocessing

  Clause learning parameters: -kept_clauses initial budget of learned clauses to be kept -kept_clauses_growth rate by which kept_clauses grows -kept_clause_unset_lits upper bound of number of unset literals in kept learned clauses independent of budget -kept_clause_width upper bound of width of kept learned clauses independent of budget -unset_lits_weight the weight for kept_clause_unset_lits while computing the scores for learned clauses

  Restart parameters: -restart_inverval the initial interval of restarts -inverval_growth factor by which restart_interval grows -no_phase_saving disable phase saving (also affects normal backtracking)

  Proof logging: -proof writes the proof in DRAT format into a file

  The default setting is equivalent to passing these flags. -vsids2 -restart_interval 200 -interval_growth 1.2 -kept_clauses 100 -kept_clauses_growth 400 -kept_clause_unset_lits 4 -kept_clause_width 5 -unset_lits_weight 5

• record_data.py

  record_data.py records the solving time for a given configuration in a file. The file will not be created if the given filename already exists. All the cnf files that should be used are passed as arguments to the script. Additional parameters (branching heuristics, clause learning parameters etc.) are forwarded to the solver. The script can be run as follows:

  python record_data.py <path to cdcl_solver> <timeout in seconds> <file to write results to> <cnf files> <additional flags passed to the solver>
  

• display_plot.py

  display_plot.py merges multiple files generated using record_data.py and displays them as a cactus plot. The plot shows how many instances a configuration of our solver can solve within a certain amount of time. The script can be run as follows:

  python display_plot <stats files generated by record_data.py> [-logscale]
  

  The -logscale flag changes the time axis to be displayed in logscale.

• Benchmarks

  We measured our solver on the following benchmarks:

  • inputs/{sat,unsat}: The provided benchmarks.

  • tents_puzzles: A selection of tents puzzles we generated for project 1, with sizes ranging from 100x10 to 100x60. We used a 200 seconds timeout.

  • sat_race_2006: The formulas from the SAT Race 2006 competition. We used a 900 seconds timeout. We did not include the formulas in the uploaded files because they are big, but they can be downloaded from http://fmv.jku.at/sat-race-2006/SAT-Race-Benchmarks.tgz

  We have included benchmark results measured using record_data.py and put the results in the same folder as the cnf files. For example, inputs/sat/vsids2_kc100_kcg400_re200_ig1.2_kcul4_kcw5.txt contains the results for all .cnf files in inputs/sat using the default configuration (-vsids2 -kept_clauses 100 -kept_clauses_growth 400 -restart_interval 200 -interval_growth 1.2 -kept_clause_unset_lits 4 -kept_clause_width 5).

  For selected comparisons, we also generated the graphs as image files and put them into the main project folder. Some of the graphs are zoomed in for better readability.

---

Group: Xiao Chen, Yize Sun, Zhu Yang