diff options
Diffstat (limited to 'content/zettel/3c3l1.md')
| -rw-r--r-- | content/zettel/3c3l1.md | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/content/zettel/3c3l1.md b/content/zettel/3c3l1.md new file mode 100644 index 0000000..05ce6ae --- /dev/null +++ b/content/zettel/3c3l1.md @@ -0,0 +1,25 @@ ++++ +title = "Initial SAT algorithm was not terminating" +date = "2023-04-28" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["3c3l"] +forwardlinks = [] +zettelid = "3c3l1" ++++ + +One interesting property of the initial SAT algorithm was that it was +not actually terminating in some cases, and would therefore hit the +bound limit. This was because of `setFormula` in the case where +`unitPropagation` failed. The root cause of this was because if +`unitPropagation` failed, it would pick the first clause and propagate +the first variable that occurs inside of it. However, when it could not +find a variable, it would instead return a default variable to +propagate, which might not actually be present in the formula. This +would lead to the size of variables not actually reducing on every +recursive call. + +The solution to this is to abort the algorithm early if there are any +empty clauses in the formula. This means that the formula is +unsatisfiable, so there is not need to continue the analysis. |