span=2>
Analysis of Search Based Algorithms for Satisability of Quantied
Analysis of Search Based Algorithms for Satisability of Quantied
Boolean Formulas Arising from Circuit State Space Diameter
Problems
Daijue Tang, Yinlei Yu, Darsh Ranjan, and Sharad Malik
Princeton University
{
dtang,yyu,dranjan,malik
}
@Princeton.EDU
Abstract.
The sequential circuit state space diameter problem is an important problem in sequential
verication. Bounded model checking is complete if the state space diameter of the system is known. By
unrolling the transition relation, the sequential circuit state space diameter problem can be formulated
as an evaluation for satisability of a Quantied Boolean Formula (QBF). This has prompted research
in QBFs in the verication community. Most of existing QBF algorithms, such as those based on the
DPLL SAT algorithm, are search based. We show that using search based QBF algorithms to calculate
the state space diameter of sequential circuits with existing problem formulations is no better than an
explicit state space enumeration method. This result holds independent of the representation of the QBF
formula. This result is important as it highlights the need to explore non-search based or hybrid of search
and non-search based QBF algorithms for the sequential circuit state space diameter problem.
1
Introduction
A quantied Boolean formula (QBF) is a Boolean formula with its variables quantied by either universal or existential
quantiers. The problem of deciding whether a quantied Boolean formula evaluates to true
or false is also referred to as the QBF problem. Theoretically, QBF problems belong to the class of P-SPACE
complete problems, widely considered harder than NP-complete problems like Boolean Satisability (SAT)
Problems.
Many problems in AI planning [1] and sequential circuit verication [2] [3] can be formulated as QBF
instances. In recent years, there has been an increasing interest within the verication community in ex-
ploring QBF based sequential verication as an alternative to Binary Decision Diagram (BDD) based tech-
niques. Therefore, nding efcient QBF evaluation algorithms is gaining interest in sequential verication.
Like SAT evaluation, QBF evaluation can be search based and does not suffer from the potential space
explosion problem of BDDs. This makes it attractive to use QBF over BDD based algorithms since the
problem of QBF evaluation is known to have polynomial space complexity. An obvious linear space al-
gorithm to decide QBF assigns Boolean values to the variables and recursively evaluates the truth of the
formula. The recursion depth is at most the number of variables. Since we need to store only one value of
the variable at each level, the total space required is
O
(n) where n is the number of variables.
Many complete QBF evaluation algorithms have been developed and several complete QBF solvers
have been implemented. In [4], a resolution based QBF evaluation algorithm is presented. But like most
resolution based decision methods, this algorithm has a potential memory blow up problem. In [5], the
authors propose a decision procedure that achieves the effect of resolving multiple variables at one time by
enumerating conicts of cut variables. Besides the potential memory blow up problem, this method is likely
to be inefcient for problems without small cuts. In practice, for many QBF instances, during the execution
of this method, the variables will be so much interleaved that it is impossible to nd a small cut. Partly due
to its success in SAT solvers, the Davis Logemann Loveland (DPLL) algorithm [6] has been adapted to
many QBF evaluation procedures [7][8][9] [10][11] [12][13][14]. Although DPLL based QBF solvers do
not blow up in space, they consume signicant CPU time and are unable to handle practical sized problems
as of now.
In sequential verication, symbolic model checking is a powerful technique and has been used widely.
Traditional symbolic model checking uses BDDs to represent sequential systems. With the development of
many efcient SAT solvers, bounded model checking (BMC) [3] has emerged as an alternative approach
to perform model checking. Although BMC uses fast SAT solvers and may be able to quickly nd counter
examples, it is incomplete in the sense that it can not determine when to stop the incremental unrolling of Search Algorithms on QBFs Arising from Circuit State Space Diameter Problems
215
the transition relation. The maximum number of unrollings needed to complete BMC is the diameter of the
corresponding sequential circuit state space. Therefore, determining sequential circuit state space diameters
is crucial for the completeness of BMC and its solution will have practical signicance. Existing methods
for computing the sequential circuit state space diameters [15] [16] search for new states at every step of
time frame expansion. The search can be done by multiple calls to the SAT procedure or with a combination
of BDD methods.
The sequential circuit state space diameter problem can also be tackled by formulating it as instances
of QBFs and using QBF solvers to solve them. But currently this approach lags behind other methods. The
immaturity of QBF evaluation techniques is often considered as the major reason for this. In this paper, we
show that for the existing QBF formulations of the circuit diameter problem, search based QBF algorithms
(this includes all DPLL based solvers) have no hope to outperform algorithms based on explicit reachable
state space enumeration. This result is important as it underscores the need to explore non-search based or
possibly hybrids of search and non-search based techniques.
2
The Sequential Circuit State Space Diameter Problem and Its QBF
Formulations
A QBF is of the form
Q
1
x
1
Q
n
x
n
, where Q
i
(i = 1
n
) is either an existential quantier or
a universal quantier
. is a propositional formula with x
1
x
n
as its variables. Adjacent variables
quantied by the same quantier in the prex can be grouped together to form a quantication set. The
order of the variables in the same quantication set can be exchanged without changing the QBF evaluation
result (true or false). Variables in the outermost quantication set are said to have quantication level
1, and
so on.
The propositional part
in a QBF is usually expressed in the Conjunctive Normal Form (CNF). If of
a QBF is in CNF, the innermost quantier of this QBF is existential because the innermost universal quan-
tier can always be dropped by removing all the occurrences of the variables quantied by this universal
quantier in the CNF. The innermost quantier can be a universal quantier if
is not in CNF. Converting
to CNF needs to introduce new variables and quantify these new variables with existential quantiers put
inside the originally innermost quantier. The number of quantication levels of a QBF may change if the
representation of
of this QBF changes. When is in CNF, the QBF having k levels of quantication is
called
kQBF. Most practical QBF instances are
2QBF or 3QBF. In the rest of the paper, when we talk about
kQBF, k is the number of quantication levels when is in CNF.
Many problems in hardware verication concern verifying certain properties of logic circuits. For com-
binational circuits, we can formulate such problems as QBF instances by introducing one variable for each
circuit node. A circuit node is either a primary input or a gate output. The propositional part is usually
written as = S P , where S represents the consistency condition of combinational circuit C and P is the
conjunction of the properties of
C that need to be veried. Each logic gate in C can be represented as either
a Boolean formula directly translated from the gate operation or a set of clauses that capture the consistent
logic conditions associated with that gate.
S is the conjunction of the Boolean representation for each logic
gate.
The behavior of a sequential circuit over a number of time frames can be modeled using the conventional
time frame expansion approach, which creates a combinational circuit by unrolling the next state function
of the sequential circuit. The sequential circuit state space diameter problem can be formulated as a QBF by
unrolling the next state function. The shortest path from one state
s
i
of a sequential circuit to another state
s
j
is dened as the minimum number of steps to go from
s
i
to
s
j
in the corresponding state transition graph.
Clearly, every state on a shortest path appears at most once, which means that a shortest path has no loop.
The state space diameter of a sequential circuit is the longest shortest path from one of the original states
of this sequential circuit to any other reachable state. Figure 1 shows the combinational circuit constructed
at each step of the circuit state space diameter calculation. We have two expansions of the combinational
logic, one for
n
+ 1 time frames and the other for n time frames. I
i
and
I
i
(i = 1, 2,
) are sets of
primary inputs,
O
i
and
O
i
(i = 1, 2,
) are sets of primary outputs and S
i
and
S
i
(i = 0, 1,
) are
sets of state variables. Let
C
1
denote the
n
+ 1 time frame expansion part and C
2
denote the
n time
frame expansion part. Let
F
(C
1
) and F (C
2
) be the Boolean functions representing the logic consistencies
of
C
1
and
C
2
respectively. If
I
(S) is the characteristic function of the initial states, T (I, S, S ) is the
characteristic function of the state transition relation, then
F
(C
1
) = I(S
0
)
n
i=0
T
(I
i
, S
i
, S
i+1
) and 216
Daijue Tang et al.
Combinational
Logic
I
1
O
1
1
s
0
s
Combinational
Logic
I
n
O
n
n
s
1 n
s
Combinational
Logic
I
n+1
O
n+1
1
+
n
s
Combinational
Log