1 files changed, 24 insertions, 0 deletions
diff --git a/content/zettel/2e1c6.md b/content/zettel/2e1c6.md
new file mode 100644
index 0000000..1467cda
--- /dev/null
+++ b/content/zettel/2e1c6.md
@@ -0,0 +1,24 @@
++++
+title = "Using SAT with hashed expressions"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["2e1c5"]
+forwardlinks = ["3a7", "2e1c7", "2e1c6a"]
+zettelid = "2e1c6"
++++
+
+The pure SAT solution is the nicest, as it just has to be passed to a
+SAT solver, however, this SAT solver needs to support features such as
+arithmetic. However, comparisons in the translation validation of
+scheduling ([\#3a7]) can also be done using hash-consed terms, which
+reduces the structural comparison of the objects by pointer equality
+checks. The assumption is made that if the pointer equality succeeds,
+that value of the pointers are structurally equal.
+
+Because only a comparison of numbers is needed for this, it is possible
+to do this comparison quite simply using a standard SAT problem. For
+this I will have to look into how hash-consing is actually performed and
+how the behaviour can be expressed from it.
+
+  [\#3a7]: /zettel/3a7