Biomedical Engineering Reference
In-Depth Information
An extension of the SAT problem, in which the goal is to find
all
satisfying
assignments is called
All-SAT
.
Definition I.13:
All-SAT
. Given a Boolean formula
S
(on a set of binary variables
X
) expressed in CNF, the objective of All-SAT is to find all assignments of the binary
variables in
X
that satisfies
S
, if such an assignment exists.
One simple algorithm for All-SAT is to perform SAT on the formula
S
, express
the satisfying assignment as a cube
k
, complement
k
to get a clause
c
, add
c
asanew
clause of the formula
S
, and perform SAT again repeatedly until an UNSAT result
is obtained. The inclusion of
c
in
S
ensures that the same cube
k
cannot be found as
a satisfying assignment again. The process continues until no new solutions can be
found.
To
d
emonstrate All-SAT, we refer back to the previous e
xam
ple,
S
(
a
,
b
,
c
)
=
(
a
abc
. We perform an
All-SAT by first taking the satisfying cube and complementing it (using DeMorgan's
law) to form a new clause
c
to be added to
S
:
+
b
)
·
(
a
+
b
+
c
) where we found a satisfying cube
k
=
c
=
k
=
(
abc
)
=
(
a
+
b
+
c
)
The new clause
c
is then appended to the original formula to obtain
S
=
S
·
c
:
=
+
·
+
+
·
+
+
S
(
a
b
)
(
a
b
c
)
(
a
b
c
)
Note that the new clause
c
is unsatisfiable using the variables from
k
, ensuring that
the next iteration of SAT will find a different satisfying cube. Th
e
new CNF
S
is
solved by SAT again to obtain a new satisfying cube, for example
abc
. The steps are
repeated until no new satisfying assignments are found.
Another useful extension of SAT is
Weighted partial Max-SAT
(WPMS) which
aims to satisfy a subset of the clauses. In WPMS, each clause in the CNF is iden-
tified as a
hard clause
or
soft clause
. Each soft clause is associated with a weight.
The problem then is to identify an assignment that satisfies
all
hard clauses while
maximizing the total weight of the satisfied soft clauses.
Definition I.14:
Weighted partial Max-SAT
(WPMS). Given a Boolean formula
S
(on a set of binary variables
X
) expressed in CNF, where each clause is identified
hard clause
or
soft clause
, the objective of WPMS is to identify an assignment of
the binary variables in
X
that satisfies all hard clauses in
S
and maximizes the total
weigh of all satisfied soft clauses, if such an assignment exists.
To give an example of WPMS, consider the following CNF:
S
(
x
,
y
,
z
)
=
(
x
+
y
)
·
(
x
+
z
)
·
(
y
+
z
)
·
(
x
)
·
(
y
)
·
(
z
)
In this CNF, we are given that the first three clauses (
x
z
) are hard
clauses, while the last three clauses are soft clauses (
x
), (
y
), (
z
). Furthermore, the
soft clauses (
x
), (
y
), (
z
) are assigned weights of 3, 7, and 6 respectively.
For WPMS, an assignment of (
x
,
y
,
z
) must satisfy all the hard clauses and max-
imize the total weight of the satisfied soft clauses. In this example, each soft clause
+
y
), (
x
+
z
), (
y
+
