blob: 1467cdae4550b158762dcd4831747c5675e1fdaf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
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
|
