+++
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.