diff options
Diffstat (limited to 'content/zettel/3a8g5h.md')
| -rw-r--r-- | content/zettel/3a8g5h.md | 51 |
1 files changed, 50 insertions, 1 deletions
diff --git a/content/zettel/3a8g5h.md b/content/zettel/3a8g5h.md index 31ab96c..86f9892 100644 --- a/content/zettel/3a8g5h.md +++ b/content/zettel/3a8g5h.md @@ -4,7 +4,7 @@ author = "Yann Herklotz" tags = [] categories = [] backlinks = ["3a8g5g"] -forwardlinks = ["3a8g5i", "3a8g5h1"] +forwardlinks = ["3a8g5h1", "3a8g5h2", "4e1", "3a8g5h3", "3a8g5h4", "3a8g5i"] zettelid = "3a8g5h" +++ @@ -31,4 +31,53 @@ 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 |