From 563367467ec3a4fa35dec84405c33052d738aa91 Mon Sep 17 00:00:00 2001 From: James Date: Sun, 9 Jun 2024 00:33:56 -0400 Subject: [PATCH 1/8] add discussion --- ITP/symmetry-breaking.tex | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/ITP/symmetry-breaking.tex b/ITP/symmetry-breaking.tex index 3f4e757..0f2dd16 100644 --- a/ITP/symmetry-breaking.tex +++ b/ITP/symmetry-breaking.tex @@ -130,3 +130,15 @@ \end{align*} This concludes the proof. \end{proof} + +We had quite some difficulty formalizing the symmetry-breaking argument. +We spent many hours around a whiteboard, +simplifying the argument to minimize the amount of theory we would need to develop. +The projective transformation in Step 3 was particularly difficult to wrangle. +This step, and those after it, requires careful bookkeeping around the distinguished point $p_1$. + +Once these details were worked out, +the proof was relatively straightforward, albeit long and tedious. +Each step of the proof justifies not only that a new property is achieved, +but also that all properties from previous steps are preserved. +As a result, the proof burden was substantial. From 1d4680cf78469b425cbed2d61ab3fb3bfb07ab2e Mon Sep 17 00:00:00 2001 From: James Date: Sun, 9 Jun 2024 12:54:25 -0400 Subject: [PATCH 2/8] small edits --- ITP/encoding.tex | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/ITP/encoding.tex b/ITP/encoding.tex index 1e18466..943e612 100644 --- a/ITP/encoding.tex +++ b/ITP/encoding.tex @@ -105,7 +105,7 @@ which can be assembled into a $6$-hole $ap'ed'cb'$. Justifying this formally turned out to be complex, -requring a fair bit of reasoning about point \lstinline|Arc|s +requiring a fair bit of reasoning about point \lstinline|Arc|s and \lstinline|σCCWPoints|: lists of points winding around a convex polygon. Luckily, the main argument can be summarized in terms of two facts: (a) any triangle $abc$ contains an empty triangle $ab'c$; and @@ -164,14 +164,15 @@ we partition the problem into 312\,418 subproblems. Each of these subproblems was solved using {\tt CaDiCaL} version 1.9.5. -The solver produced an LRAT proof for each execution, +{\tt CaDiCaL} produced an LRAT proof for each execution, which was validated using the {\tt cake\_lpr} verified checker on-the-fly in order to avoid writing/storing/reading large files. The total runtime was 25\,876.5 CPU hours, or roughly 3 CPU years. The difference in runtime relative to Heule and Scheucher's original run is purely due to the difference in hardware. Additionally, -we validated that the subproblems cover the entire search space as Heule and Scheucher did~\cite[Section 7.3]{emptyHexagonNumber}. +we validated that the subproblems cover the entire search space +as Heule and Scheucher did~\cite[Section 7.3]{emptyHexagonNumber}. This was done by verifying the unsatisfiability of another formula that took 20 seconds to solve. From a3092273f80693148dfc62c082db455272c4a30f Mon Sep 17 00:00:00 2001 From: James Date: Sun, 9 Jun 2024 13:54:01 -0400 Subject: [PATCH 3/8] validating the run --- ITP/encoding.tex | 11 +++++++++++ ITP/main.bib | 18 ++++++++++++++++++ 2 files changed, 29 insertions(+) diff --git a/ITP/encoding.tex b/ITP/encoding.tex index 943e612..fdd8e1e 100644 --- a/ITP/encoding.tex +++ b/ITP/encoding.tex @@ -176,6 +176,17 @@ This was done by verifying the unsatisfiability of another formula that took 20 seconds to solve. +The artifact for this paper includes scripts to validate any individual subproblem, +as well as the summary proof that the subproblems cover the search space. +However, the unsatisfiability of $\phi_{30}$ depends on +the unsatisfiability of \textit{all} (hundreds of thousands of) subproblems. +A skeptical reader might wish to examine the proof files for all subproblems, +but we estimated the total proof size to be tens or hundreds of terabytes, +far too much to reasonably store and distribute. +So, the skeptical reader must run the entire 3 CPU year computation. +We believe this trust story can be somewhat improved, +but leave such a challenge as future work. + % file-local attic: % By using the triangulation lemma repeatedly, diff --git a/ITP/main.bib b/ITP/main.bib index bd34c0e..53681cd 100644 --- a/ITP/main.bib +++ b/ITP/main.bib @@ -671,3 +671,21 @@ @InProceedings{sbva IGNOREURN = {urn:nbn:de:0030-drops-184736}, doi = {10.4230/LIPIcs.SAT.2023.11}, } + +@InProceedings{cube_and_conquer, +author="Heule, Marijn J. H. +and Kullmann, Oliver +and Wieringa, Siert +and Biere, Armin", +editor="Eder, Kerstin +and Louren{\c{c}}o, Jo{\~a}o +and Shehory, Onn", +title="Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads", +booktitle="Hardware and Software: Verification and Testing", +year="2012", +publisher="Springer Berlin Heidelberg", +address="Berlin, Heidelberg", +pages="50--65", +abstract="Satisfiability (SAT) is considered as one of the most important core technologies in formal verification and related areas. Even though there is steady progress in improving practical SAT solving, there are limits on scalability of SAT solvers. We address this issue and present a new approach, called cube-and-conquer, targeted at reducing solving time on hard instances. This two-phase approach partitions a problem into many thousands (or millions) of cubes using lookahead techniques. Afterwards, a conflict-driven solver tackles the problem, using the cubes to guide the search. On several hard competition benchmarks, our hybrid approach outperforms both lookahead and conflict-driven solvers. Moreover, because cube-and-conquer is natural to parallelize, it is a competitive alternative for solving SAT problems in parallel.", +isbn="978-3-642-34188-5" +} From 29ccadd2c6f7abd3efe4169844921375b74778e7 Mon Sep 17 00:00:00 2001 From: James Date: Sun, 9 Jun 2024 14:27:19 -0400 Subject: [PATCH 4/8] future work discussion --- ITP/conclusions.tex | 12 +++++++----- ITP/encoding.tex | 3 ++- ITP/triple-orientations.tex | 2 +- 3 files changed, 10 insertions(+), 7 deletions(-) diff --git a/ITP/conclusions.tex b/ITP/conclusions.tex index 70fd7ec..262df19 100644 --- a/ITP/conclusions.tex +++ b/ITP/conclusions.tex @@ -35,12 +35,14 @@ that did not match the (correct) code of Heule and Scheucher. Our formalization corrects this. -In terms of future work, -we hope to formally verify the result $h(7) = \infty$ due to Horton~\cite{hortonSetsNoEmpty1983}, +\subsection*{Future Work} +We hope to formally verify the result $h(7) = \infty$ due to Horton~\cite{hortonSetsNoEmpty1983}, and other results in Erd\H{o}s-Szekeres style problems. -A key challenge for the community -is to improve the connection between verified SAT tools and ITPs. + +We also see a key challenge for the community, +to improve trust when importing ``cube and conquer'' style results to an ITP. This presents a significant engineering task -for proofs that are hundreds of terabytes long (as in this result). +when the proof certificate is hundreds of terabytes, +as in this result (see \Cref{sec:running_cnf}). Although we are confident that our results are correct, the trust story at this connection point has room for improvement. diff --git a/ITP/encoding.tex b/ITP/encoding.tex index fdd8e1e..f51534d 100644 --- a/ITP/encoding.tex +++ b/ITP/encoding.tex @@ -154,7 +154,8 @@ are both empty shapes in $P$, then $S$ is an empty shape in $P$. -\subparagraph*{Running the CNF.} +\subsection*{Running the CNF.} +\label{sec:running_cnf} Having now shown that our main result follows if $\phi_{30}$ is unsatisfiable, we run a distributed computation to check its unsatisfiability. We solve the SAT formula~$\phi_{30}$ produced by Lean using the same setup as diff --git a/ITP/triple-orientations.tex b/ITP/triple-orientations.tex index a000063..3d851f7 100644 --- a/ITP/triple-orientations.tex +++ b/ITP/triple-orientations.tex @@ -222,7 +222,7 @@ $\left(\mathbb{R}^2\right)^n$. This is the key idea that will allow us to transition from the finitely-verifiable statement ``\emph{no set of triple orientations over $n$ points satisfies property $\pi_k$}'' to the desired statement ``\emph{no set of $n$ points satisfies property $\pi_k$}.'' -\subsection{Properties of orientations}\label{sec:sigma-props} +\subsection*{Properties of orientations}\label{sec:sigma-props} We now prove, assuming points are sorted left-to-right (which is justified in~\Cref{sec:symmetry-breaking}), From e6ee94372722a3a9f3d158c5d2660394f22037c8 Mon Sep 17 00:00:00 2001 From: Cayden Codel Date: Sun, 9 Jun 2024 13:52:43 -0700 Subject: [PATCH 5/8] Small rewording --- ITP/encoding.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ITP/encoding.tex b/ITP/encoding.tex index f51534d..df25392 100644 --- a/ITP/encoding.tex +++ b/ITP/encoding.tex @@ -184,9 +184,9 @@ \subsection*{Running the CNF.} A skeptical reader might wish to examine the proof files for all subproblems, but we estimated the total proof size to be tens or hundreds of terabytes, far too much to reasonably store and distribute. -So, the skeptical reader must run the entire 3 CPU year computation. +Instead, the skeptical reader must run the entire 3 CPU year computation. We believe this trust story can be somewhat improved, -but leave such a challenge as future work. +but we leave such a challenge to future work. % file-local attic: From f2e5892b15e472b500ee9695b5e21e912ee792ca Mon Sep 17 00:00:00 2001 From: Cayden Codel Date: Sun, 9 Jun 2024 13:53:06 -0700 Subject: [PATCH 6/8] Rephrase ending paragraph --- ITP/conclusions.tex | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/ITP/conclusions.tex b/ITP/conclusions.tex index 262df19..ca5123c 100644 --- a/ITP/conclusions.tex +++ b/ITP/conclusions.tex @@ -39,10 +39,9 @@ \subsection*{Future Work} We hope to formally verify the result $h(7) = \infty$ due to Horton~\cite{hortonSetsNoEmpty1983}, and other results in Erd\H{o}s-Szekeres style problems. -We also see a key challenge for the community, -to improve trust when importing ``cube and conquer'' style results to an ITP. -This presents a significant engineering task -when the proof certificate is hundreds of terabytes, -as in this result (see \Cref{sec:running_cnf}). +We also want to improve the trust story of importing ``cube and conquer''-style results into an ITP. +Importing these kinds of proofs is a significant engineering task +when the proof certificate is hundreds of terabytes in size, +as it was for this result (see \Cref{sec:running_cnf}). Although we are confident that our results are correct, -the trust story at this connection point has room for improvement. +more work needs to be done to strengthen the trust in this connection point. From 6b6875b31c24541dae97fe6bc960baf8fa3b2364 Mon Sep 17 00:00:00 2001 From: Cayden Codel Date: Sun, 9 Jun 2024 22:38:38 -0700 Subject: [PATCH 7/8] Rewrite ending paragraph of symm breaking section --- ITP/symmetry-breaking.tex | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) diff --git a/ITP/symmetry-breaking.tex b/ITP/symmetry-breaking.tex index 0f2dd16..e3d634d 100644 --- a/ITP/symmetry-breaking.tex +++ b/ITP/symmetry-breaking.tex @@ -131,14 +131,9 @@ This concludes the proof. \end{proof} -We had quite some difficulty formalizing the symmetry-breaking argument. -We spent many hours around a whiteboard, -simplifying the argument to minimize the amount of theory we would need to develop. -The projective transformation in Step 3 was particularly difficult to wrangle. -This step, and those after it, requires careful bookkeeping around the distinguished point $p_1$. - -Once these details were worked out, -the proof was relatively straightforward, albeit long and tedious. -Each step of the proof justifies not only that a new property is achieved, -but also that all properties from previous steps are preserved. -As a result, the proof burden was substantial. +Compared to the symmetry-breaking transformation described by Heule and Scheucher, +our transformation is simpler. +Nonetheless, proving the above theorem in Lean was tedious, +as we had to show that the properties from the previous steps were preserved at each new step, +which carried substantial proof burden. +In particular, steps 3 through 6 required careful bookkeeping and special handling of the distinguished point~$p_1$. From 4551f83f6ac1df9de1bec91eeb2c3b9dd85585c7 Mon Sep 17 00:00:00 2001 From: James Date: Mon, 10 Jun 2024 23:53:57 -0400 Subject: [PATCH 8/8] Section headers must be numbered --- ITP/conclusions.tex | 2 +- ITP/encoding.tex | 2 +- ITP/triple-orientations.tex | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/ITP/conclusions.tex b/ITP/conclusions.tex index ca5123c..f1fbef6 100644 --- a/ITP/conclusions.tex +++ b/ITP/conclusions.tex @@ -35,7 +35,7 @@ that did not match the (correct) code of Heule and Scheucher. Our formalization corrects this. -\subsection*{Future Work} +\subparagraph*{Future Work} We hope to formally verify the result $h(7) = \infty$ due to Horton~\cite{hortonSetsNoEmpty1983}, and other results in Erd\H{o}s-Szekeres style problems. diff --git a/ITP/encoding.tex b/ITP/encoding.tex index df25392..44121c5 100644 --- a/ITP/encoding.tex +++ b/ITP/encoding.tex @@ -154,7 +154,7 @@ are both empty shapes in $P$, then $S$ is an empty shape in $P$. -\subsection*{Running the CNF.} +\subsection{Running the CNF.} \label{sec:running_cnf} Having now shown that our main result follows if $\phi_{30}$ is unsatisfiable, we run a distributed computation to check its unsatisfiability. diff --git a/ITP/triple-orientations.tex b/ITP/triple-orientations.tex index 3d851f7..a000063 100644 --- a/ITP/triple-orientations.tex +++ b/ITP/triple-orientations.tex @@ -222,7 +222,7 @@ $\left(\mathbb{R}^2\right)^n$. This is the key idea that will allow us to transition from the finitely-verifiable statement ``\emph{no set of triple orientations over $n$ points satisfies property $\pi_k$}'' to the desired statement ``\emph{no set of $n$ points satisfies property $\pi_k$}.'' -\subsection*{Properties of orientations}\label{sec:sigma-props} +\subsection{Properties of orientations}\label{sec:sigma-props} We now prove, assuming points are sorted left-to-right (which is justified in~\Cref{sec:symmetry-breaking}),