Mycielski

Mycielski graph formulas, PR proofs, and the code accompanying the SAT 2020 paper Mycielski graphs and PR proofs.

cnf/ includes the formulas. Mk.cnf and Mk+.cnf encode the colorability of Mₖ with k-1 colors and k colors, respectively.
proof/ includes the PR proofs. Mk.dpr and Mk.pr are with and without deletion, respectively.
partial/ includes the formulas extended with clauses from parts of the proofs as described in the paper.
incr/ includes the code for the experiments described in Section 5.3 of the paper.
incr/icnf/ includes the MYCₖ+PR formulas with negations of the clauses in R2 included as assumptions for incremental solving.
icadical/ includes a modified version of CaDiCaL for incremental SAT solving. Thanks to Armin Biere for his implementation.

Instructions

Make sure to have the following in your path.

Requirements: Julia (v1.3), dpr-trim, allsat, CaDiCaL (commit 92d7289), YalSAT, ICaDiCaL (included in this repository).

[optional] ./proof.sh to generate the proofs from scratch.
./verify.sh to check both sets of proofs against the formulas for k from 3 to 10.

[optional] ./partial.sh to generate the extended formulas from scratch.
./count.sh k to count the number of satisfying assignments for formulas extended from MYCₖ.
./cadical.sh k t to test CaDiCaL on these formulas with a timeout of t seconds.

Change the directory to incr.
[optional] ./gen_all.sh to generate the cubes from scratch. By default this script uses 20 workers, you may change the fourth argument it passes to generate.sh to use a different number.
./run_all.sh to perform the experiments for the configurations described in the paper.
./report.sh to generate a summary of the results.