1 files changed, 17 insertions, 0 deletions
diff --git a/content/zettel/2e1c5.md b/content/zettel/2e1c5.md
new file mode 100644
index 0000000..dcfaffd
--- /dev/null
+++ b/content/zettel/2e1c5.md
@@ -0,0 +1,17 @@
++++
+title = "Proper SAT solution"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["2e1c4", "2e1c3a"]
+forwardlinks = ["2e1c6"]
+zettelid = "2e1c5"
++++
+
+One could also encode the following SAT query, which should be
+*unsatisfiable*, in the case where the SAT solver supports simple
+arithmetic.
+
+$$(P \rightarrow x = 1) \land (\neg P \land Q \rightarrow x = 2) \land (\neg P\land \neg Q \land R \rightarrow x = 3) \land (\neg P \land \neg Q \land \neg R\rightarrow x = 4) \land (Q \rightarrow x' = 2) \land (\neg Q \land P\rightarrow x' = 1) \land (\neg Q \land \neg P \land R \rightarrow x' = 3) \land(\neg Q \land \neg P \land \neg R \rightarrow x' = 4) \land \neg (x = x') $$
+
+This solution was proposed by George during the group meeting.