Biomedical Engineering Reference
In-Depth Information
Often, the AND operator “
·
” is replaced by catenation, for example
a
·
b
is replaced
by
ab
.
For any Boolean function, there are an infinite number of Boolean formulas. Note
that in the previous examples of Boolean formulae above, both
f
and
g
are formulas
that represent the same Boolean function. The goal of logic synthesis is to find the
“best” Boolean formula for a function. In chip design, the utility function for logic
synthesis may include minimizing number of gates (which may be selected from a
standard gate (or cell) library) or minimizing the estimated circuit's delay or power.
1.5.2
Boolean Satisfiability
Boolean satisfiability (SAT) is an NP-complete decision problem. Given a Boolean
formula in CNF form, SAT determines if there is an assignment of the variables
that will satisfy the formula (make the formula evaluate true). Many algorithms in
logic synthesis and electronic design automation (EDA) can be cast as an instance
of Boolean satisfiability. Some examples where SAT is used in logic synthesis and
EDA include functional equivalence checking, automatic test pattern generation
(ATPG), and logic optimization. In addition, the industry and research community
have developed several efficient and scalable SAT engines. In this thesis, we take
advantage of these advancements in SAT solvers, and apply them towards problems
in genomics. We first define basic terms in Boolean satisfiability.
Definition I.12:
Boolean satisfiability (SAT)
. Given a Boolean formula
S
(on a
set of binary variables
X
) expressed in CNF, the objective of SAT is to identify an
assignment of the binary variables in
X
that satisfies
S
, if such an assignment exists.
If no such assignment exists,
S
is concluded to be
unsatisfiable
(UNSAT).
In order to satisfy the formula
S
(i.e. make it evaluate to
true
), each clause of
S
must have at least one literal evaluate to true. Satisfying
S
is equivalent to satisfying
all
c
i
S
. In general, there may exist many satisfying assignments for the formula
in question.
For example, consider the formula:
∈
S
(
a
,
b
,
c
)
=
(
a
+
b
)
·
(
a
+
b
+
c
)
This formula consists of 3 variables, 2 clauses, and 5 literals. To determine if the
formula is satisfiable, we attempt to satisfy all the individual clauses. If all clauses
a
re
s
at
isfied, then the formula
S
is also satisfied. We observe that the fir
st
clause
(
a
+
b
) is satisfied (or evaluates to 1) if either
a
=
0or
b
=
0. In that case,
a
=
1or
b
=
1 respectively, which satisfies the first clause. If
a
=
0 and
b
=
0, the second
+
+
=
clause (
a
1.
Because all its clauses are satisfied, we co
ncl
ude that
S
is satisfiable, and
a
sat-
isfying assignment
is (
a
,
b
,
c
)
b
c
) is satisfied only if
c
=
(0, 0, 1) or
abc
. Note, the cube (product)
abc
is
logically the same as stating that
a
=
0,
b
=
0, and
c
=
1.
