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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
+++
title = "Problem with SAT verification "
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3a8g5g"]
forwardlinks = ["3a8g5h1", "3a8g5h2", "4e1", "3a8g5h3", "3a8g5h4", "3a8g5i"]
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.
{{< transclude-1 zettel="3a8g5h1" >}}
The first solution to this problem would be to add quantifiers to the
atoms that cannot always be evaluated at the current spot. However, this
would significantly increase the complexity of the Sat solver, as well
as make predicates unevaluatable in general, because it might contain
quantifiers that don't evaluate to one specific value.
However, with a suitably strong SAT solver, it should be possible to
show the independence between the different predicates. However, the
correctness property should probably be correct as well and should be
checkable with the SAT solver.
{{< /transclude-1 >}}
{{< transclude-1 zettel="3a8g5h2" >}}
The second possible solution could be to use Craig interpolation
([\#4e1]), which was a suggestion by John. This is close to what we
currently already do, however a bit more sound (replacing positive
literals by T and replacing negative literals by $\perp$). This does not
seem to completely solve the problem, because it only really works for
implication, and for the independence property that's not enough.
{{< /transclude-1 >}}
{{< transclude-1 zettel="3a8g5h3" >}}
Tri-state logic is also an interesting solution and it goes back to what
we had initially thought about implementing, however, the problem with
that is again the SAT solver, as we want to be able to assume that we do
get an answer out of it. However, maybe it's possible to use the SAT
solver natively on 3-state logic. We would then be able to construct the
evaluation rules for our gates so that they follow the correctness
property that we are hoping for.
{{< /transclude-1 >}}
{{< transclude-1 zettel="3a8g5h4" >}}
Finally, the fourth solution could be to have lazy evaluation of the
expressions, and order the predicates so that the more general property
comes first, followed by the more specific properties. However, the main
problem with this is that we don't really know which predicate came from
which node, and what the order should be for those predicates.
{{< /transclude-1 >}}
[1]: attachment:gsa-simplification-problem.png
[\#4e1]: /zettel/4e1
|
