diff options
Diffstat (limited to 'content/zettel/2e1c6b.md')
| -rw-r--r-- | content/zettel/2e1c6b.md | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/content/zettel/2e1c6b.md b/content/zettel/2e1c6b.md new file mode 100644 index 0000000..29c3966 --- /dev/null +++ b/content/zettel/2e1c6b.md @@ -0,0 +1,34 @@ ++++ +title = "Similarity of hashing for SAT and for performance" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["2e1c6a"] +forwardlinks = ["3c3c3"] +zettelid = "2e1c6b" ++++ + +In the case of SAT solving, the expressions actually do need to be +hashed just so that they are evaluatable by the SAT solver. This is +different to doing hash-consing for performance reasons, which is what +Six et al. \[1\] are doing ([\#3c3c3]). In the Six et al. case, you care +a lot about performance, so you want to do the hash-consing in OCaml, +however, in our case you don't care too much about the hash-consing, but +more about the hashing algorithm being unique and "easy" to work with. + +<div id="refs" class="references csl-bib-body" markdown="1"> + +<div id="ref-six21_verif_super_sched_relat_optim" class="csl-entry" +markdown="1"> + +<span class="csl-left-margin">\[1\] +</span><span class="csl-right-inline">C. Six, L. Gourdin, S. Boulmé, and +D. Monniaux, “<span class="nocase">Verified Superblock Scheduling with +Related Optimizations</span>,” Apr. 2021. Available: +<https://hal.archives-ouvertes.fr/hal-03200774></span> + +</div> + +</div> + + [\#3c3c3]: /zettel/3c3c3 |