blob: 31ab96c3634e712206fadc6ad9f9d9ea84ff360f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
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
|
