summaryrefslogtreecommitdiffstats
path: root/content/zettel/2e1c4a.md
diff options
context:
space:
mode:
Diffstat (limited to 'content/zettel/2e1c4a.md')
-rw-r--r--content/zettel/2e1c4a.md22
1 files changed, 22 insertions, 0 deletions
diff --git a/content/zettel/2e1c4a.md b/content/zettel/2e1c4a.md
new file mode 100644
index 0000000..af35c95
--- /dev/null
+++ b/content/zettel/2e1c4a.md
@@ -0,0 +1,22 @@
++++
+title = "Special SAT solving of the predicates"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["2e1c4"]
+forwardlinks = ["2e1c4b"]
+zettelid = "2e1c4a"
++++
+
+The predicates cannot be turned on and off that easily, as these are
+formulas, and not simple predicate values. There are multiple solutions
+to this. First, I could use some kind of data-structure such as a list
+to keep track of the values assigned to the predicates, and do a
+structural equality check to see if the current predicate being examined
+is part of the list. However, this is quite inefficient, as negated
+predicates will be handled as separate values to non-negated predicates,
+even though the values could be inferred from either. Doing it the
+proper SAT solving way would also make it possible to change the
+predicates that are being examined in the case that they can be
+simplified, although it's not something that is really planned, so this
+might not be too bad of a limitation.