diff --git a/book.toml b/book.toml index 7f31b03..bcf05fa 100644 --- a/book.toml +++ b/book.toml @@ -7,6 +7,9 @@ title = "Cutting Planes with Lean 4" [output.html] git-repository-url = "https://github.com/bernborgess/lean-cutting-planes" +mathjax-support = true [output.html.playground.boring-prefixes] lean = "# " + +# mdbook serve -p 8000 -n 127.0.0.1 diff --git a/docs/SUMMARY.md b/docs/SUMMARY.md index ffef43b..45053d3 100644 --- a/docs/SUMMARY.md +++ b/docs/SUMMARY.md @@ -4,3 +4,5 @@ [Cutting Planes with Lean 4](title_page.md) - [Introduction](./introduction.md) +- [Pseudo Boolean Rules](./pseudo_boolean_rules.md) +- [Worked Example](./worked_example.md) diff --git a/docs/introduction.md b/docs/introduction.md index 46399ce..1485f9b 100644 --- a/docs/introduction.md +++ b/docs/introduction.md @@ -4,4 +4,20 @@ Introduction Cutting Planes and Lean 4 ----------------------------- -*Cutting Planes* is a formal logic. +*Cutting Planes* is a formal logic used in the context of discrete combinatorial problems, that can be applied in _Software testing_, _Formal verification_ and _Proof logging_. + +Our proofs will consist of _Pseudo-Boolean Constraints_, that are 0-1 integer linear inequalities of the form: +\\[ \sum_i{a_i l_i} \ge A \\] +Where we have: +- constant \\( A \in \mathbb{Z} \\) +- coefficients \\( a_i \in \mathbb{Z} \\) +- literals \\( l_i: x_i\ \text{or}\ \overline{x_i}\ (\text{where } x_i + \overline{x_i} = 1) \\) +- variables \\( x_i \\) take values \\( 0 = false \\) or \\( 1 = true \\) + +Without loss of generality, we will use the [normalized form](Bar95), with all \\( a_i, A\\) non-negative. + +In this regard, _Pseudo-Boolean Reasoning_ works on two axioms and four rules, each of which are formally verified in this project using _Lean 4_ + +Lean 4 is a theorem prover and programming language developed by Leonardo de Moura. In the last years it became proeminent in the mathematics community, after [The Xena Project](https://www.ma.imperial.ac.uk/~buzzard/xena/) of Imperial College London formalized Peter Scholze's proof in the area of condensed mathematics in 2021. In 2023 Terence Tao used Lean to formalize a proof of the _Polynomial Freiman-Ruzsa (PFR) conjecture_, published in the same year. + +Armed with a Lean 4 proof of the reasoning rules, complex proofs that involve these steps can be guaranteed to be correct. diff --git a/docs/pseudo_boolean_rules.md b/docs/pseudo_boolean_rules.md new file mode 100644 index 0000000..c3962c9 --- /dev/null +++ b/docs/pseudo_boolean_rules.md @@ -0,0 +1,49 @@ +Pseudo Boolean Rules +============ + +Input Axioms +----------------------------- + +As a starting point for the pseudo boolean reasoning we will get constraints from the user, which are subject to a normalization process + +Literal Axioms +----------------------------- + +For any literal \\( l_i\\) we can create a constraint: +\\[ \frac{} + {l_i \ge 0} +\\] + +Addition Rule +----------------------------- +Two constraints can be added together, adding the coefficients and the constants. Another behaviour is that \\(x_i\\) and \\(\overline{x_i}\\) that may appear together cancel each other: +\\[ \frac + {{\sum_i{a_i l_i} \ge A}\qquad {\sum_i{b_i l_i} \ge B}} + {\sum_i{(a_i + b_i) l_i} \ge (A+B)} +\\] + +Multiplication Rule +----------------------------- +A constraint can be multiplied by any \\( c \in \mathbb{N}^{+} \\): +\\[ \frac + {\sum_i{a_i l_i} \ge A} + {\sum_i{c a_i l_i} \ge c A} +\\] + +Division Rule +----------------------------- +A constraint can be divided by any \\( c \in \mathbb{N}^{+} \\), and the the ceiling of this division in applied: +\\[ \frac + {\sum_i{a_i l_i} \ge A} + {\sum_i{ \lceil \frac{a_i}{c} \rceil l_i} \ge \lceil \frac{A}{c} \rceil} +\\] + +Saturation Rule +----------------------------- +A constraint can be replace its coefficients by the minimum between them and the constant: +\\[ \frac + {\sum_i{a_i l_i} \ge A} + {\sum_i{ \min(a_i,A)\cdot l_i} \ge A} +\\] + +All these rules can be seen in practice in the Worked Example \ No newline at end of file diff --git a/docs/title_page.md b/docs/title_page.md index a05986f..a696039 100644 --- a/docs/title_page.md +++ b/docs/title_page.md @@ -2,4 +2,6 @@ *by Bernardo Borges* -This book is the official documentation for the usage of the [lean-cutting-planes](https://github.com/bernborgess/lean-cutting-planes) library. It is currently a work in progress, with the goal to provide full expressivity in Lean 4 for the cutting planes formal logic. \ No newline at end of file +This book is the official documentation for the usage of the [lean-cutting-planes](https://github.com/bernborgess/lean-cutting-planes) library. It is currently a work in progress, with the goal to provide full expressivity in Lean 4 for the cutting planes formal logic. + +Future work in this project will aim to verify unsat demonstrations that were produced by solvers suchs as [RoundingSat](https://gitlab.com/MIAOresearch/software/roundingsat) and check that their reasoning was correct. diff --git a/docs/worked_example.md b/docs/worked_example.md new file mode 100644 index 0000000..f6fc4da --- /dev/null +++ b/docs/worked_example.md @@ -0,0 +1,97 @@ +Worked Example +============ + +Input +----------------------------- + +For this example, in constraints over variables \\(w,x,y,z\\) we will have three input axioms: + +1. \\( w + 2x + y \ge 2 \\) +1. \\( w + 2x + 4y + 2z \ge 5 \\) +1. \\( \overline{z} \ge 0 \\) + +```lean +example (xs : Fin 4 → Fin 2) + (c1 : PBIneq ![(1,0),(2,0),(1,0),(0,0)] xs 2) + (c2 : PBIneq ![(1,0),(2,0),(4,0),(2,0)] xs 5) + (c3 : PBIneq ![(0,0),(0,0),(0,0),(0,1)] xs 0) +``` + +Goal +----------------------------- +The objective of this example is to prove: +\\[ w + 2x + 2y \ge 3 \\] + +```lean + : PBIneq ![(1,0),(2,0),(2,0),(0,0)] xs 3 := by +``` + +Execution +----------------------------- +We start by using muliplication of the first constraint by 2: +\\[ \frac + {w + 2x + y \ge 2} + {2w + 4x + 2y \ge 4} + (\text{Multiply by 2}) +\\] +```lean + let t1 : PBIneq ![(2,0),(4,0),(2,0),(0,0)] xs 4 := by apply Multiplication c1 2 +``` + +Now we add this result to constraint 2: +\\[ \frac + {{2w + 4x + 2y \ge 4}\qquad {w + 2x + 4y + 2z \ge 5}} + {3w + 6x + 6y + 2z \ge 9} + (\text{Add}) +\\] +```lean + let t2 : PBIneq ![(3,0),(6,0),(6,0),(2,0)] xs 9 := by apply Addition t1 c2 +``` +At this point we want to remove the variable \\(z\\), as it does not appear in our goal. Then we will introduce a \\(\overline{z} \ge 0\\) by the literal axiom and then multiply it by 2: +\\[ \frac + {\overline{z} \ge 0} + {2\overline{z} \ge 0} + (\text{Multiply by 2}) +\\] +```lean + let t3 : PBIneq ![(0,0),(0,0),(0,0),(0,2)] xs 0 := by apply Multiplication c3 2 +``` +Performing addition will cancel out the \\(z\\) variable: +\\[ \frac + {{3w + 6x + 6y + 2z \ge 9}\qquad {2\overline{z} \ge 0}} + {3w + 6x + 6y \ge 7} + (\text{Add}) +\\] +```lean + let t4 : PBIneq ![(3,0),(6,0),(6,0),(0,0)] xs 7 := by apply Addition t2 t3 +``` +And lastly a division by 3 is performed to arrive at the goal: +\\[ \frac + {3w + 6x + 6y \ge 7} + {w + 2x + 2y \ge 3} + (\text{Divide by 3}) +\\] +```lean + exact Division t4 3 + done +``` + +Summarizing, this is the full proof: + +![toy_example](./assets/toy_example.png) + +```lean +example + (xs : Fin 4 → Fin 2) + (c1 : PBIneq ![(1,0),(2,0),(1,0),(0,0)] xs 2) + (c2 : PBIneq ![(1,0),(2,0),(4,0),(2,0)] xs 5) + (c3 : PBIneq ![(0,0),(0,0),(0,0),(0,1)] xs 0) + : PBIneq ![(1,0),(2,0),(2,0),(0,0)] xs 3 + := by + let t1 : PBIneq ![(2,0),(4,0),(2,0),(0,0)] xs 4 := by apply Multiplication c1 2 + let t2 : PBIneq ![(3,0),(6,0),(6,0),(2,0)] xs 9 := by apply Addition t1 c2 + let t3 : PBIneq ![(0,0),(0,0),(0,0),(0,2)] xs 0 := by apply Multiplication c3 2 + let t4 : PBIneq ![(3,0),(6,0),(6,0),(0,0)] xs 7 := by apply Addition t2 t3 + exact Division t4 3 + done +```