1 files changed, 34 insertions, 0 deletions
diff --git a/content/zettel/3a8g5h.md b/content/zettel/3a8g5h.md
new file mode 100644
index 0000000..31ab96c
--- /dev/null
+++ b/content/zettel/3a8g5h.md
@@ -0,0 +1,34 @@
++++
+title = "Problem with SAT verification "
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a8g5g"]
+forwardlinks = ["3a8g5i", "3a8g5h1"]
+zettelid = "3a8g5h"
++++
+
+In the current implementation, instead of changing the GSA semantics to
+match the SSA semantics for the γ-function, I have added validation that
+the predicates are indeed independent (if one predicate is true, all the
+others should be false) in `check_pred_independent` which should then
+prove that `pred_independent` holds.
+
+However, this actually discovered a bug in the compilation of
+`knucleotide.c`, where the simplification of predicates according to the
+dominance of the definition of the variables is actually not correct.
+One ends up having predicates that can both be true at the same time:
+
+![][1]
+
+The example above goes over this, and it is similar to the examples we
+discussed before, but we thought that dominance of variables was
+conservative enough, which actually isn't the case. In the example, `x2`
+is defined under the false branch, but is necessary to correctly
+identify the difference between the two predicates
+$1 \lor (\neg 1 \land 2)$ and $\neg 1 \land \neg 2$, which are logically
+independent before the simplification to $1 \lor \neg 1$ and
+$\neg1 \land \neg 2$, where the left hand branch will actually always be
+true.
+
+  [1]: attachment:gsa-simplification-problem.png