blob: 05ce6aef2a202846cfdec3dd84541ec97b8d8976 (
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
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.
|
