Lecture Notes for
Logic and Computability
Course Number: IND04033UF
Contact
Bettina Könighofer
Institute for Applied Information Processing and Communications (IAIK)
Graz University of Technology, Austria
[Link]@[Link]
Table of Contents
3 Combinational Equivalence Checking 3
3.1 Translation of a Circuit into a Formula . . . . . . . . . . . . . . . 4
3.2 Relations between Satisfiability, Validity, Equivalence and Entail-
ment . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
3.3 Normal Forms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
3.4 Tseitin Encoding . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
3.5 CEC Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1
Combinational Equivalence Checking
3
In this chapter we discuss combinational equivalence checking (CEC) based on
Boolean satisfiability (SAT). CEC plays an important role in the design of elec-
tronic systems such as integrated circuits and printed circuit boards. Its im-
mediate application is verifying functional equivalence of combinational circuits
after the application of synthesis and optimization tools. In a typical scenario,
there are two structurally different implementations of the same design, and the
problem is to prove their functional equivalence.
The standard approach for checking the equivalence of two circuits is to re-
duce the equivalence problem to SAT and using a SAT solver to solve the problem
instance. Though the problem is NP-complete, most verification instances can
be solved in reasonable space and time resources due to the high efficiency of
modern SAT solvers.
Overview of CEC based on Satisfiablilty
In the following, we give the overview of the algorithm to check for the equiva-
lence of two circuits. In the reminder of this chapter, we will discuss the indi-
vidual steps in detail.
Algorithm - Decide equivalence of combinational circuits: Let C1
and C2 denote the two combinational circuits. In order to check whether C1 and
C2 are equivalent, one has to perform the following steps:
1. Encode C1 and C2 into two propositional formulas ϕ1 and ϕ2 .
2. Compute the Conjunctive Normal Form (CNF) of ϕ1 ⊕ ϕ2 , using Tseitin
encoding; i.e., CN F (ϕ1 ⊕ ϕ2 ).
3
4 Chapter 3. Combinational Equivalence Checking
3. Give the formula CN F (ϕ1 ⊕ϕ2 ) to a SAT solver and check for satisfiability.
4. C1 and C2 are equivalent if and only if CN F (ϕ1 ⊕ ϕ2 ) is UNSAT.
3.1 Translation of a Circuit into a Formula
Each gate of the circuit can be represented via a propositional formula over its
inputs and outputs. The following figure lists a summary of the common Boolean
logic gates with their symbols and truth tables.
Figure 3.1: Boolean logic gates.
Example. Translate the following circuit C into a propositional formula.
3.2. Relations between Satisfiability, Validity, Equivalence and Entailment 5
The inputs of C are denoted by a, b, and c and the output is denoted by r.
We assign temporary variable names to the inner wires; in this case we use p
and q. Using these variables, we can create the propositional formula over the
inputs and the output of C.
r =q∧c
= (a ∨ p) ∧ c (3.1)
= (a ∨ ¬b) ∧ c
3.2 Relations between Satisfiability, Validity,
Equivalence and Semantic Entailment
In the first chapter, we discussed the notions of satisfiability, validity, equiva-
lence, and semantic entailment. All of this notions can be reduced to each other.
Therefore, only one decision procedure is needed to decide all notions. This is in
particularly important, since for the question of satisfiability there exists tools
– SAT solvers – that are able to decide most practical instances highly efficient,
even though the problem of deciding satisfiability is NP-complete. Therefore, in
order to answer the questions of validity, semantic entailment, or equivalence,
these questions will be reduced to the question of satisfiability most of the time.
In this section, we discuss the relations between the notions.
Duality of Satisfiability and Validity
A formula ϕ is valid, if and only if, ¬ϕ is not satisfiable.
Consider the formula ϕ = (x ∨ ¬x). This formula is valid, i.e., all rows
in the truth table would evaluate to true. The negation of ϕ is the following:
¬ϕ = ¬(x ∨ ¬x) = ¬x ∧ x, which is not satisfiable, i.e., all rows the truth table
would evaluate to false.
A formula ϕ is satisfiable, if and only if, ¬ϕ is not valid.
If ϕ is satisfiable, there is at least one model that makes the formula true.
If we negate the formula, these models make the negated formula false, and
therefore, the negated formula cannot be valid.
aa
solving ϕ
aa ϕ valid?
using aa
a satisfiable?
¬ϕ not
Satisfiability X
satisfiable?
¬ϕ not
Validity X
valid?
6 Chapter 3. Combinational Equivalence Checking
Overview over all Relations
aa
solving ϕ
aa ϕ valid? ϕ ψ? ϕ ≡ ψ?
using aa
a satisfiable?
¬ϕ not ϕ ∧ ¬ψ not ϕ ⊕ ψ not
Satisfiability X
satisfiable? satisfiable? satisfiable?
¬ϕ not ϕ→ψ ϕ↔ψ
Validity X
valid? valid? valid?
ϕ ψ and
Entailment > 2 ¬ϕ? > ϕ? X
ψ ϕ?
ϕ→ψ≡
Equivalence ϕ 6≡ ⊥? ϕ ≡ >? X
>?
Row 1: Decide semantic entailment using satisfiability. The question
whether ϕ ψ can be decided by checking ϕ ∧ ¬ψ not satisfiable. If there does
not exist a counterexample, i.e., a model that makes ϕ true and makes ψ false,
then we have semantic entailment.
Row 1: Decide equivalence using satisfiability. The question whether
ϕ ≡ ψ can be decided by checking ϕ ⊕ ψ not satisfiable. If there does not exists
a model, that makes one sub-formula true, and the other sub-formula false, then
the two formulas are semantically equivalent.
Row 2: Decide semantic entailment using validity. The question
whether ϕ ψ can be decided by checking ϕ → ψ is valid. For an implication to
hold, all models that satisfy ϕ also have to satisfy ψ. This is also the requirement
for ϕ ψ to be true.
Row 2: Decide equivalence using validity. The question whether ϕ ≡ ψ
can be decided by checking ϕ ↔ ψ is valid. This holds, since the formula ϕ ↔ ψ
only evaluates to true under models that either make both sub-formulas true, or
both false.
Row 3: Decide satisfiability using semantic entailment. The question
whether ϕ is satisfiable can be decided by checking > 2 ¬ϕ. If not all models
satisfy ¬ϕ, then there exists a model that satisfies ϕ, and therefore ϕ must be
satisfiable.
Row 3: Decide validity using semantic entailment. The question
whether ϕ is valid can be decided by checking > ϕ. If all models satisfy ϕ,
then ϕ must be valid.
Row 3: Decide equivalence using entailment. The question whether
ϕ ≡ ψ is valid can be decided by checking ϕ ψ and ψ ϕ. If all models that
satisfy ϕ also satisfy ψ and all models that satisfy ψ also satisfy ϕ, then ϕ and
ψ are satisfied by exactly the same models and are equivalent.
Row 4: Decide satisfiability using equivalence. The question ϕ is
satisfiable can be decided by checking ϕ 6≡ ⊥. If it is not true, that ϕ evaluates
to false under all models, then ϕ is satisfiable.
Row 4: Decide validity using equivalence. The question whether ϕ is
3.3. Normal Forms 7
valid can be decided by checking ϕ ≡ >. If it is true, that ϕ evaluates to true
under all models and is valid.
Row 4: Decide entailment with equivalence. The question whether
ϕ ψ can be decided by checking ϕ → ψ ≡ >. If all models that satisfy ϕ also
satisfy ψ, then we have semantic entailment.
3.3 Normal Forms
For ease of implementation, most SAT solvers operate on formulas given in
conjunctive normal form (CNF). In this section we discuss the two standard
normal forms: the disjunctive normal form (DNF) and the conjunctive normal
form (CNF).
Terminology
Let ϕ be a propositional formula defined over Boolean variables x1 , ..., xn . We
introduce the following symbols and terminology to define CNF and DNF.
• A literal is a variable xi or its negation.
• A literal is called positive if it is just a variable. A literal is called negative
if it is the negation of a variable.
• A clause is a disjunction of literals, e.g., x1 ∨ x2 .
• A cube is a conjunction of literals, e.g., x1 ∧ x2 .
Disjunctive Normal Form (DNF)
A formula in DNF is a disjunction of cubes, e.g., (p ∧ q ∧ r) ∨ (¬p ∧ q ∧ r) ∨ (¬q).
Any formula in propositional logic can be converted to the disjunctive normal
form. One simple way to do so is to use the truth table of the formula. For every
model/line that delivers a 1, a conjunction of all literals of that lines is formed,
i.e., variables which are assigned 1 in the line are not negated and variables
which are assigned 0 are negated. These conjunctions per line form the cubes
of the DNF formula. By connecting all cubes with disjunctions, one obtains the
final DNF formula.
Example. Given the formula ϕ := ¬a ∨ ¬(b → c). Compute its representa-
tion in DNF using its truth table.
8 Chapter 3. Combinational Equivalence Checking
a b c ¬a ∨ ¬(b → c)
F F F T
F F T T
F T F T
F T T T
T F F F
T F T F
T T F T
T T T F
The resulting formula in DNF is
(¬a ∧ ¬b ∧ ¬c) ∨ (¬a ∧ ¬b ∧ c) ∨ (¬a ∧ b ∧ ¬c) ∨ (¬a ∧ b ∧ c) ∨ (a ∧ b ∧ ¬c).
Conjunctive Normal Form (CNF)
A formula in CNF is a conjunction of clauses, e.g., (p ∨ q ∨ r) ∧ (¬p ∨ q ∨ r).
To convert the formula to CNF, we consider the models/lines that make
the formula false. For every line that delivers a 0, a disjunction of the negated
literals of that lines is formed, i.e., variables which are assigned 1 in the line are
negated and variables which are assigned 0 are not negated. These disjunctions
per line form the clauses of the CNF formula. By connecting all clauses with
conjunctions, one obtains the final CNF formula.
Example. Given the formula ϕ := ¬a ∨ ¬(b → c). Compute its representa-
tion in CNF using its truth table.
a b c ¬a ∨ ¬(b → c)
F F F T
F F T T
F T F T
F T T T
T F F F
T F T F
T T F T
T T T F
The resulting formula in DNF is
(¬a ∨ b ∨ c) ∧ (¬a ∨ b ∨ ¬c) ∧ (¬a ∨ ¬b ∨ ¬c).
Example. Provide the formula in CNF and in DNF that is represented by
the following truth table.
3.4. Tseitin Encoding 9
Figure 3.2: DNF/CNF example.1
3.4 Tseitin Encoding
Propositional formulas need to be converted into CNF before they can be given
to a SAT solver. The disadvantage for using truth tables for the conversion is
that for some formulas, the resulting representation in CNF might be exponen-
tially larger than the original formula. Therefore, we do not generate a CNF
that is equivalent, but instead perform a transformation that only preserves sat-
isfiability. We call such a formula that is not equivalent to the original formula
but preserves satisfiability equisatisfiable.
Definition - Equisatisfiability. Two propositional formulas ϕ and ψ are
equisatisfiable if and only if either both are satisfiable or both are unsatisfiable.
One way to perform the conversion of a propositional formula into an equi-
satisfiable formula in CNF is the Tseitin’s method, which only results in a linear
blow-up.
The Tseitin Algorithm
Tseitin’s method takes the syntax tree for a propositional formula ϕ as input. An
internal node in this tree is a Boolean connective while a leaf is a Boolean vari-
able. The algorithm traverses the tree, beginning with the leaves, and associates
a fresh variable – called tseitin variable – to each node, i.e., to each subformula.
By traversing through the tree, the algorithm collects a set of clauses.
1 Taken from [Link]
Datei:Knf+[Link] by JensKhol, licensed under CC-BY-SA-2.0
10 Chapter 3. Combinational Equivalence Checking
We will explain the Tseitin’s method for formulas that are restricted to the
Boolean connectives ∧, ∨, and ¬.
Step 1: Assigning tseitin variables to all nodes in the parse tree /
to each subformula.
Example. Consider the formula ϕ := ((p∨q)∧r)∨¬p. For each sub-formula,
we introduce a tseitin variable.
((p ∨ q ) ∧ r) ∨ ¬p
x1 x3
x2
xϕ
Step 2: Add new clauses for each tseitin variable.
Each new tseitin variable represents either a ¬, ∧, or ∨ node in the parse
tree, i.e., sub-formula of the form ¬ϕ, ϕ ∧ ψ, or ϕ ∨ ψ. The Tseitin-Rewriting
Rules define, which clauses are associated with which type of node / subformula.
Tseitin-Rewrite rules:
For each node, let x be the tseitin tseitin variable, and let p and q be the
new variables for the two subformulas of the node.
• ∧ node: for x ↔ (p∧q) introduce the clauses (¬x∨p)∧(¬x∧q)∧(¬p∨¬q∨x).
• ∨ node: for x ↔ (p∨q) introduce the clauses (¬p∨x)∧(¬q∨x)∧(¬x∨p∨q).
• ¬ node: for x ↔ ¬p introduce the clauses (¬x ∨ ¬p) ∧ (p ∨ x).
Finally, to obtain the final equisatisfiable formula in CNF, we connect the
variable for the top level node of the formula and all generated clauses with
conjunctions.
Example. Using the Tseitin algorithm and its rewriting rules, we would
obtain the following clauses for the example above with ϕ := ((p ∨ q) ∧ r) ∨ ¬p:
CN F (ϕ) = (¬p ∨ x1 ) ∧ (¬q ∨ x1 ) ∧ (¬x1 ∨ p ∨ q)
∧ (¬x2 ∨ x1 ) ∧ (¬x2 ∨ r) ∧ (¬x1 ∨ ¬r ∨ x2 )
∧ (¬x3 ∨ ¬p) ∧ (p ∨ x3 ) (3.2)
∧ (¬x2 ∨ xϕ ) ∧ (¬x3 ∨ xϕ ) ∧ (¬xϕ ∨ x2 ∨ x3 )
∧ xϕ
Derivation of the Tseitin Rewriting Rules
Following we briefly justify the clauses that are generated for ∧, ∨, and ¬ nodes.
• x ↔ (p ∧ q) generates the clauses (¬x ∨ p) ∧ (¬x ∨ q) ∧ (¬p ∨ ¬q ∨ x) because:
3.5. CEC Example 11
x ↔ (p ∧ q)
(x → (p ∧ q)) ∧ ((p ∧ q) → x) | φ ↔ ψ ≡ (φ → ψ) ∧ (ψ → φ)
(x → p) ∧ (x → q) ∧ ((p ∧ q) → x) | φ → (ψ ∧ χ) ≡ (φ → ψ) ∧ (φ → χ)
(¬x ∨ p) ∧ (¬x ∧ q) ∧ (¬(p ∧ q) ∨ x) | φ → ψ ≡ ¬φ ∨ ψ
(¬x ∨ p) ∧ (¬x ∧ q) ∧ (¬p ∨ ¬q ∨ x) | ¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ
• x ↔ (p ∨ q) generates the clauses (¬p ∨ x) ∧ (¬q ∨ x) ∧ (¬x ∨ p ∨ q) because:
x ↔ (p ∨ q)
(x → (p ∨ q)) ∧ ((p ∨ q) → x) | φ ↔ ψ ≡ (φ → ψ) ∧ (ψ → φ)
(x → (p ∨ q)) ∧ (p → x) ∧ (q → x) | ψ ∨ φ → χ ≡ (φ → χ) ∧ (ψ → χ)
(¬x ∨ p ∨ q) ∧ (¬p ∨ x) ∧ (¬q ∨ x) | φ → ψ ≡ ¬φ ∨ ψ
(¬p ∨ x) ∧ (¬q ∨ x) ∧ (¬x ∨ p ∨ q) | rearranging
• x ↔ ¬p generates the clauses (¬x ∨ ¬p) ∧ (p ∨ x) because:
x ↔ ¬p
(x → ¬p) ∧ (¬p → x) | φ ↔ ψ ≡ (φ → ψ) ∧ (ψ → φ)
(¬x ∨ ¬p) ∧ (¬¬p ∨ x) | φ → ψ ≡ ¬φ ∨ ψ
(¬x ∨ ¬p) ∧ (p ∨ x) | ¬¬φ ≡ φ
Summary: Tseitin Rewriting Rules
χ ↔ (ϕ ∨ ψ) ⇔ (¬ϕ ∨ χ) ∧ (¬ψ ∨ χ) ∧ (¬χ ∨ ϕ ∨ ψ)
χ ↔ (ϕ ∧ ψ) ⇔ (¬χ ∨ ϕ) ∧ (¬χ ∨ ψ) ∧ (¬ϕ ∨ ¬ψ ∨ χ)
χ ↔ ¬ϕ ⇔ (¬χ ∨ ¬ϕ) ∧ (ϕ ∨ χ)
Properties of Tseitin Encoding
We make two observations about the set of clauses that is generated by the
Tseitin procedure for a formula ϕ.
1. The number of variables and clauses is linear in the size of ϕ. We have thus
avoided the exponential blowup we would have observed when constructing
an equisatisfiable CNF formula CN F (ϕ).
2. The constructed formula CN F (ϕ) is equisatisfiable to ϕ: CN F (ϕ) has a
satisfying assignment if and only if there is a satisfying assignment for ϕ.
We can obtain a satisfying assignment for ϕ from the satisfying assignment
for CN F (ϕ) by simply dropping the additional variables that the algorithm
has introduced.
3.5 CEC Example
Example. Given are two formulas ϕ1 = ¬a ∧ ¬b and ϕ2 = ¬(a ∨ b). Check
whether ϕ1 and ϕ2 are semantically equivalent using the reduction to satisfia-
bility.
12 Chapter 3. Combinational Equivalence Checking
We need to check, whether ϕ1 ⊕ ϕ2 is not satisfiable, i.e, ϕ1 ≡ ϕ2 if and only
if ϕ1 ⊕ ϕ2 is UNSAT. Therefore, we perform the following steps.
• We construct the formula ϕ:
ϕ = ϕ1 ⊕ ϕ2 = (¬a ∧ ¬b) ⊕ ¬(a ∨ b)
(3.3)
= (¬a ∧ ¬b) ∧ ¬(¬(a ∨ b)) ∨ ¬(¬a ∧ ¬b) ∧ ¬(a ∨ b)
• Next, the formula ϕ has to be transformed into a CNF formula by using
Tseitin encoding.
Tseitin-Step 1: Assigning new varibles to subformulas.
(¬a ∧ ¬b) ∧ ¬(¬(a ∨ b)) ∨ ¬(¬a ∧ ¬b) ∧ ¬(a ∨ b)
x1 x2 x3 x1 x2 x3
x4 x5 x4 x5
x6 x7
x8 x9
xϕ
Tseitin-Step 2: Apply rewriting rules.
CN F (ϕ) = xϕ ∧
(¬x8 ∨ xϕ ) ∧ (¬x9 ∨ xϕ ) ∧ (¬xϕ ∨ x9 ∨ x8 )∧ | rewriting xϕ
(¬x9 ∨ x7 ) ∧ (¬x9 ∨ x5 ) ∧ (¬x7 ∨ ¬x5 ∨ x9 )∧ | rewriting x9
(¬x8 ∨ x4 ) ∧ (¬x8 ∨ x6 ) ∧ (¬x4 ∨ ¬x6 ∨ x8 )∧ | rewriting x8
(¬x7 ∨ ¬x4 ) ∧ (x7 ∨ x4 )∧ | rewriting x7
(¬x6 ∨ ¬x5 ) ∧ (x6 ∨ x5 )∧ | rewriting x6
(¬x5 ∨ ¬x3 ) ∧ (x5 ∨ x3 )∧ | rewriting x5
(¬x4 ∨ x1 ) ∧ (¬x4 ∨ x3 ) ∧ (¬x1 ∨ ¬x3 ∨ x4 )∧ | rewriting x4
(¬a ∨ x3 ) ∧ (¬b ∨ x3 ) ∧ (¬x3 ∨ a ∨ b)∧ | rewriting x3
(¬x2 ∨ ¬b) ∧ (x2 ∨ b)∧ | rewriting x2
(¬x1 ∨ ¬a) ∧ (x1 ∨ a) | rewriting x1
• Finally, the formula CN F (ϕ) is given to a SAT solver. If the SAT solver
determines that CN F (ϕ) is unsatisfiable, then ϕ1 ≡ ϕ2 . If the SAT solver
determines that CN F (ϕ) is satisfiable, then ϕ1 6≡ ϕ2 .