Merge pull request #7 from bsubercaseaux/cube_check

Scripts and README for verification

.gitignore

@@ -1,8 +1,15 @@
 .DS_Store/
 .DS_Store
 *.cnf
+*.icnf
 .direnv/
 utils/HoleComputation.js
+*.drat
+*.lrat
+cube_checking/cube_gen
+
+## Nix flake uses .venv directory to set up python stuff
+.venv
 
 ## Core latex/pdflatex auxiliary files:
 *.aux

utils/6hole.c → Heule_Scheucher.c

@@ -1,3 +1,8 @@
+/*
+ * Encoding used by Heule and Scheucher.
+ *  We sourced this C file directly from them.
+ */
+
 #include <stdio.h>
 #include <stdlib.h>
 #include <assert.h>

README.md

@@ -1,12 +1,14 @@
 # EmptyHexagonLean
 A Lean verification of the _Empty Hexagon Number_, obtained by a [recent breakthrough of Heule and Scheucher](https://arxiv.org/abs/2403.00737).
-The main theorem is that every finite set of 30 or more points must contain a convex and empty 6-gon. The proof is based on generating a CNF formula whose unsatisfiability is formally proved to imply the theorem. This repository contains the formalization code, and it allows the generation of the associated CNF.
+The main theorem is that every finite set of 30 or more points must contain a convex, empty 6-gon. The proof is based on generating a CNF formula whose unsatisfiability is formally proved to imply the theorem. This repository contains the formalization code, and it allows the generation of the associated CNF.
 
 
 
 ## Installing Lean
 
-See the [quickstart](https://lean-lang.org/lean4/doc/quickstart.html) guide from the Lean manual,
+The main part of this repository is a mathematical formalization written in the Lean 4 theorem prover.
+To install Lean on your machine,
+see the [quickstart](https://lean-lang.org/lean4/doc/quickstart.html) guide from the Lean manual,
 or [the extended setup instructions](https://lean-lang.org/lean4/doc/setup.html).
 
 
@@ -34,17 +36,17 @@ Overall structure:
 
 ## Generating CNFs
 
-The project includes scripts for generating the CNFs we formalized against.
+The project includes scripts for generating the CNFs we formalized against. These must be run inside the `Lean` subfolder.
 
 #### Convex 6-gon
-For `n` points:
+For `n` points, in the `Lake/` directory, run:
 ```
 lake exe encode gon 6 <n>
 ```
 With `n = 17` this CNF can be solved in under a minute on most machines.
 
 #### Convex `k`-hole
-For convex `k`-hole in `n` points:
+For convex `k`-hole in `n` points, in the `Lake/` directory, run:
 ```
 lake exe encode hole <k> <n>
 ```
@@ -54,9 +56,78 @@ the CNFs produced can be shown UNSAT instantly.
 
 For `k = 6`, `n = 30`, the CNF takes on the order of 17,000 CPU hours to show UNSAT when parallelized using cube&conquer.
 
-The script in `utils/6hole-cube.c` outputs the list of cubes we used to solve `k = 6`, `n = 30`.
-We will add scripts soon for reproducing the entire parallel computation.
+# Cube and Conquer verification
 
+In order to verify that the resulting formula $F$ is indeed UNSAT, two things ought to be checked:
+
+ 1) **(Tautology proof)** The formula $F$ is UNSAT iff $F \land C_i$ is UNSAT for every $i$.
+ 2) **(UNSAT proof)** For each cube $C_i$, the formula $F \land C_i$ is UNSAT.
+
+This repository contains scripts that allow you to check these two proofs.
+
+The **tautology proof** is implied by checking that $F \land (\bigwedge_i \neg C_i)$ is UNSAT, as per Section 7.3 of [Heule and Scheucher](https://arxiv.org/abs/2403.00737).
+
+As a first step, install the required dependencies:
+1) Clone and compile the SAT solver `cadical` from [its GitHub repository](https://github.com/arminbiere/cadical). Add the `cadical` executable to your `PATH`.
+2) Clone and compile the verified proof checker `cake_lpr` from [its GitHub repository](https://github.com/tanyongkiam/cake_lpr). Add the `cake_lpr` executable to your `PATH`.
+3) Install the `eznf` and `lark` python libraries with `pip install eznf` and `pip install lark`.
+
+Next, generate the main CNF by running:
+```
+cd Lean
+lake exe encode hole 6 30 ../cube_checking/vars.out > ../cube_checking/6-30.cnf
+```
+
+The **tautology proof** can be verified by navigating to the `cube_checking/` directory and running 
+```
+./verify_tautology.sh
+```
+which boils down to:
+```
+gcc 6hole-cube.c -o cube_gen
+./cube_gen 0 vars.out > cubes.icnf
+python3 cube_join.py -f 6-30.cnf -c cubes.icnf --tautcheck -o taut_if_unsat.cnf
+cadical taut_if_unsat.cnf tautology_proof.lrat --lrat # this should take around 30 seconds
+cake_lpr taut_if_unsat.cnf tautology_proof.lrat
+```
+If proof checking succeeds, you should see the following output:
+
+```
+s VERIFIED UNSAT
+```
+
+Moreover, if you do not have the `cadical` and `cake_lpr` executables on your path, you can pass them to the script as:
+```
+env CADICAL=<path to cadical> CAKELPR=<path to cake_lpr> ./verify_tautology.sh 
+```
+
+Because verifying the **UNSAT proof** requires many thousands of CPU hours,
+we provide a simple way to verify that any single cube is UNSAT.
+To generate the formula + cube number $i$ (assuming the steps for the **tautology proof** have been followed), run `./solve_cube.sh` script in the `cube_checking/` directory, which essentially runs:
+```
+./cube_gen <i> vars.out > .tmp_cube_<i>
+python3 cube_join.py -f 6-30.cnf -c .tmp_cube_<i> -o with_cube_<i>.cnf
+cadical with_cube_<i>.cnf proof_cube_<i>.lrat --lrat # this should take a few seconds
+cake_lpr with_cube_<i>.cnf proof_cube_<i>.lrat
+```
+For example, to solve cube number 42, run:
+
+```
+./solve_cube.sh 42
+```
+The cubes are indexed from 1 to 312418.
+
+We **DO NOT RECOMMEND** that the casual verifier runs all cubes,
+as doing so would take many thousands of CPU hours.
+Our verification was completed in a semi-efficient manner using parallel computation,
+which required some custom scripting.
+However, the skeptical reviewer with *lots of computation to spare* can replicate our results.
+To generate the formula and all cubes for incremental solving, run:
+```
+./cube_gen 0 vars.out > cubes.icnf
+python3 cube_join.py -f 6-30.cnf -c cubes.icnf --inccnf -o full_computation.icnf
+cadical full_computation.icnf # this should take a while :P
+```
 
 ## Authors
 - [Bernardo Subercaseaux](https://bsubercaseaux.github.io/) (Carnegie Mellon University)

cube_checking/cube_join.py

@@ -0,0 +1,77 @@
+from eznf import modeler
+import argparse
+
+argparser = argparse.ArgumentParser()
+argparser.add_argument(
+    "-f", "--formula", required=True, type=str, help="CNF Formula file"
+)
+argparser.add_argument("-c", "--cubes", required=True, type=str, help="Cube file")
+argparser.add_argument("-o", "--output", required=False, type=str, help="Output file")
+argparser.add_argument(
+    "--tautcheck", action="store_true", help="Checks for a tautology"
+)
+argparser.add_argument('--inccnf', action="store_true", help="Creates a .icnf file with the formula + cubes")
+
+
+args = argparser.parse_args()
+
+formula_file = args.formula
+cube_file = args.cubes
+output_file = args.output
+tautcheck = args.tautcheck
+icnf = args.inccnf
+
+encoding = modeler.Modeler()
+
+def itokenize(line):
+    """
+    takes a line as a string, coming from either a `p cnf` or a `p inccnf` file
+    returns array of ints without 0
+    ignores lines starting with c or p
+    """
+    if len(line) == 0:
+        return []
+    if line[0] == "c" or line[0] == "p":
+        return []
+    if line[:-1] == "\n":
+        line = line[:-1]
+    tokens = line.split(" ")
+    ans = []
+    for t in tokens:
+        try:
+            t = int(t)
+            if t != 0:
+                ans.append(t)
+        except ValueError:
+            continue
+    return ans
+
+
+with open(formula_file, 'r', encoding='utf-8') as sb_file:
+    for line in sb_file.readlines():
+        tkns = itokenize(line)
+        if len(tkns) > 0:
+            encoding.add_clause(tkns)
+
+
+cubes = []
+with open(cube_file, 'r', encoding='utf-8') as cb_file:
+    for line in cb_file.readlines():
+        tkns = itokenize(line)
+        if len(tkns) == 0:
+            continue
+        if tautcheck:
+            encoding.add_clause([-t for t in tkns])
+        else:
+            cubes.append(tkns)
+
+if tautcheck:
+    encoding.serialize(output_file)
+elif icnf:
+    encoding.cube_and_conquer(lambda: cubes, output_file)
+else:
+    assert len(cubes) == 1
+    cube = cubes[0]
+    for lit in cube:
+        encoding.add_clause([lit])
+    encoding.serialize(output_file)

cube_checking/solve_cube.sh

@@ -0,0 +1,9 @@
+#!/bin/sh
+# Receives the desired cube number as $1
+gcc 6hole-cube.c -o cube_gen
+./cube_gen $1 vars.out > .tmp_cube_$1
+python3 cube_join.py -f 6-30.cnf -c .tmp_cube_$1 -o with_cube_$1.cnf
+${CADICAL:-cadical} with_cube_$1.cnf proof_cube_$1.lrat --lrat
+${CAKELPR:-cake_lpr} with_cube_$1.cnf proof_cube_$1.lrat
+
+rm with_cube_$1.cnf proof_cube_$1.lrat .tmp_cube_$1

cube_checking/verify_tautology.sh

@@ -0,0 +1,7 @@
+#!/bin/sh 
+
+gcc 6hole-cube.c -o cube_gen
+./cube_gen 0 vars.out > cubes.icnf
+python3 cube_join.py -f 6-30.cnf -c cubes.icnf --tautcheck -o taut_if_unsat.cnf
+${CADICAL:-cadical} taut_if_unsat.cnf tautology_proof.lrat --lrat
+${CAKELPR:-cake_lpr} taut_if_unsat.cnf tautology_proof.lrat

flake.nix

@@ -14,6 +14,8 @@
           texlive.combined.scheme-full
           texlab
           fontconfig
+          gcc
+          python3
         ];
 
         FONTCONFIG_FILE = pkgs.makeFontsConf { fontDirectories = [
@@ -23,6 +25,18 @@
             pkgs.iosevka
           ];
         };
+
+        # Create a python virtual environment with eznf and lark
+        venvDir = "./.venv";
+        buildInputs = with pkgs.python3Packages; [
+          python
+          venvShellHook
+        ];
+
+        postVenvCreation = ''
+          unset SOURCE_DATE_EPOCH
+          pip install eznf lark
+        '';
       };
     });
 }