QBF with Soft Variables

Electronic Communications of the EASST
Volume 70 (2014)

Proceedings of the
14th International Workshop on

Automated Verification of Critical Systems (AVoCS 2014)

QBF with Soft Variables

Sven Reimer, Matthias Sauer, Paolo Marin, Bernd Becker

15 pages

Guest Editors: Marieke Huisman, Jaco van de Pol
Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer
ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122

http://www.easst.org/eceasst/

QBF with Soft Variables

Sven Reimer, Matthias Sauer, Paolo Marin, Bernd Becker

Institute of Computer Science, Albert-Ludwigs-Universität Freiburg
Georges-Köhler-Allee 051, D-79110 Freiburg, Germany
{reimer | sauerm | marin | becker}@informatik.uni-freiburg.de

Abstract: QBF formulae are usually considered in prenex form, i.e. the quantifier
block is completely separated from the propositional part of the QBF. Among others,
the semantics of the QBF is defined by the sequence of the variables within the prefix,
where existentially quantified variables depend on all universally quantified variables
stated to the left.

In this paper we extend that classical definition and consider a new quantification type
which we call soft variable. The idea is to allow a flexible position and quantifier type
for these variables. Hence the type of quantifier of the soft variable can also be altered.
Based on this concept, we present an optimization problem seeking an optimal prefix as
defined by user-given preferences. We state an algorithm based on MaxQBF, and present
several applications – mainly from verification area – which can be naturally translated
into the optimization problem for QBF with soft variables. We further implemented a
prototype solver for this formalism, and compare our approach to previous work, that
differently from ours does not guarantee optimality and completeness.

Keywords: QBF, MaxQBF, prefix, dependency, optimization problem

1 Introduction

For design automation tasks in safety-critical or other domains where precise answers are necessary,
applications employing quantified Boolean formulae (QBF) logic have been demonstrated to be
an effective solution: In contrast to the traditional SAT-based 01X-encoding [JBM+00], QBF
delivers accurate answers by accurately considering unknown and unspecified signals [SB01], which
is also named Zi-encoding [HB07]. In particular universally quantified variables in QBF are used
to accurately model the behavior of unknown circuit lines. The encoding of such problems is often
not trivial and the effort required to solve them strongly depends on the prefix order, i. e. the
user-given dependencies between the existential and universal variables. Additionally, there is
an increasing interest for optimization problems with QBF [BLV08, IJM13] in the game theory
domain [CP04]. However, in the classical definition of a QBF, the prefix is known and fixed.
Research interests considering the possibility of changing the given prefix structure is focused
on simplifying the solving to a given QBF without changing its meaning, e.g. by optimizing
decision strategies in search-based solving [GNT07]. More generalized approaches apply so-called
dependency schemes [Sam08] focusing on tractable algorithms, i. e. heuristics with polynomial
complexity, optimizing the prefix order wrt. the dependencies between the variables.

As we will show in this paper, there is a relation between the prefix order and the optimization
problem for maximizing unknown values within a circuit [RS04, NSB07, PR00]. E. g., one seeks
for a maximum number of don’t care signals at the input of a circuit in order to generalize a found
solution [RS04]. Since in QBF these don’t care or unknown values are modeled by universally
quantified variables, one needs the possibility to change the quantifier for a particular variable
from existential to universal and vice versa in order to optimize the number of unknowns. In pure
QBF, quantifiers have to be given a-priori and cannot be changed.

This work was partly supported by the German Research Council (DFG) as part of the Transregional Collaborative
Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS).

In this paper we present a new formalism based on QBF supporting a dynamic prefix using
so-called soft variables. In contrast to previous perceptions, our approach allows to change the
prefix position of such soft variables dynamically. In particular, the quantifier from existential to
universal can be altered and vice versa. Technically the mechanism provides a set of possible QBF
prefixes. The challenge is to find a satisfiability preserving prefix such that the soft variables are
quantified following an ordering as close as possible to user-given preferences.

We define an optimization problem for QBF with soft variables and an algorithm returning the
optimal prefix. The algorithm is based on the optimization problem called MaxQBF [CFLS93].
We highlight the importance of our formalism by showing applications from different verification
areas, which are naturally covered by our formalism. Previous work on these applications has two
main disadvantages:

• Most approaches use a SAT-based encoding, which is less precise than a QBF represenation
(with soft variables).

• Applications using QBF formulations usually need more encoding effort than approximate
SAT encodings. As we will show, the optimization problem for solving QBF with soft
variables is PSPACE-complete (as QBF), but allows a more compact and in many cases
“easier” representation of the problem statement than pure QBF.

We developed a prototype solver for solving both: 1) MaxQBF based on [IJM13] and 2) QBF
with soft variables based on MaxQBF. First experimental results demonstrate the applicability of
our implementation and the advantage of the solution compared to heuristic approaches.

The paper is structured as follows: In §2 we introduce basic information, terminology, and
notation used throughout the paper. In §3 the concept of QBF with soft variables is introduced as
well as an algorithm to solve the problem. We introduce applications for the formalism and first
experimental results for some of those in §4. Lastly, §5 concludes the paper and discusses future
work on this topic.

2 Preliminaries

In this section we introduce the notation and some background on solving techniques, and some
further details necessary for a good comprehension of this paper. We assume that propositional
logic and the SAT problem is familiar to the reader. The interested reader is referred to [BHMW09]
for further insight in optimization problems in propositional logic and QBF.

2.1 QBF

The logic of quantified Boolean formulae (QBF) is an extension of SAT by bounding the variables to
quantifiers Q∈{∃,∀}. In the following, we will consider prenex conjunctive normal form formulae
(PCNF) ψ = Q1X1 ...QnXn.ϕ, where ϕ is a quantifier free matrix in CNF. We denote with V the
set of variables occurring in ϕ. We call P = Q1X1 ...QnXn the prefix of ψ. W.l.o.g. Qi 6= Qi+1 for
all i∈{1,...,n−1}, i. e. the existential and universal quantifiers have an alternating order, and
X1,...,Xn are disjoint sets of variables with X1

⋃
...
⋃
Xn := X.1

We define a quantifier level function δ : X → N for a variable x as δ(x) = i for x∈Xi. In the
following, w.l.o.g. we set Q1 = ∃, in particular, variables on odd quantification levels are always
existentially quantified and on even levels universally quantified. We say that an existential variable
x∈Xi depends on all universal variables y ∈Xj with j < i and Qj = ∀, i. e. the assignment of x
depends on the assignment of y.

A variable x∈W = V\X is not bound by any quantifier and is called free variable. If ψ contains
free variables, then ψ is an open QBF, otherwise it is a closed formula. Given a set of variables V
1 Note that Xi = ∅ or X 6= V may hold

and an open QBF ψ, we say that some variable valuation f ∈ (W →B) is a model of ψ iff ψ(f) = >,
and ψ(W ) is satisfiability equivalent to the closed QBF where the free variables W are existentially
quantified at level 1.

The co-factor of a propositional formula is defined as ϕ|x = ϕ[x = >] and ϕ|x = ϕ[x = ⊥]
respectively, where ϕ[x = c] denotes a propositional formula with every occurrence of x replaced
by the value c∈{>,⊥}. Similarly, ψ|x is defined as the QBF where the matrix ϕ is replaced by
ϕ|x and all superfluous quantifications are excluded from the prefix (and analogously for ψ|x). We
define the semantics of QBF recursively as follows:

Qx ψ =
{
ψ|x∧ ψ|x if Q = ∀
ψ|x∨ ψ|x if Q = ∃

If ϕ does contain an empty clause, ψ is unsatisfied, otherwise satisfied in case no variable is left
unassigned.

2.2 MaxQBF

MaxQBF (also referred to as MaxQSAT in the literature) is an extension of QBF for optimization
problems [CFLS93]. The semantics is similar to the analogous optimization problem for SAT,
called MaxSAT. A MaxSAT procedure tries to satisfy as many clauses of a propositional formula
as possible. We denote these clauses as soft clauses. The optimization problem for QBF ensures
that these soft clauses have to be satisfied for every branch of the universal variables. There are
some extensions of MaxSAT which can be adapted quite naturally to MaxQBF:

• Weighted MaxSAT/QBF: Each soft clause c is associated with a non-negative integer
weight ω(c). If a clause is satisfied, the clause gains ω(c) as score, otherwise the score
of the clause is 0. The objective is to maximize the sum of the scores.

• Partial MaxSAT/QBF: There are two types of clauses: hard clauses and soft clauses. Hard
clauses must be satisfied, while soft clauses may be satisfied. The objective is to maximize
the number of satisfied soft clauses.

• Weighted Partial MaxSAT/QBF: Combination of the two concepts stated above.

To the best of our knowledge there exist only two references proposing exact algorithms to
solve optimization problems over quantified formulae: [BLV08] considers quantified constraint
optimization problems (QCOP) as extension of constraint optimization problems (COP). In [IJM13]
the authors propose two algorithms for solving the related QMaxSAT problem: Given a QBF
instead of optimizing the number of satisfied soft clauses, the goal is to maximize a linear pseudo-
Boolean cost function. The MaxQBF problem can be easily expressed by this formalism and vice
versa.

3 QBF with Soft Variables

In this section we describe the concept of soft variables in QBF, as well as an algorithmic approach
for solving this formalism using MaxQBF, and an algorithm for solving MaxQBF problems. Finally,
we state some details of our implementations.

3.1 Soft Variables

The syntax of soft variables in the context of a QBF is defined as follows.

Definition 1 Consider a QBF ψ = P.ϕ, a Boolean variable s∈V and a set of natural numbers
L. We call s a soft variable iff the following properties hold:

1. s does not occur in P , and

2. L is a set of quantification levels on which s is designated to be quantified, also called the
quantification set of s.

We denote with

Ls a soft variable s, where L contains all possible prefix positions. Furthermore
we write ψ(

L1s1,...,

Lnsn), indicating that s1,...,sn are soft variables of ψ with possible prefix
positions Lj, for each j ∈{1,...,n}. We write Sψ indicating the set of all soft variables in ψ.

Moreover, we allow soft variable groups S, written

LS. We write ψ(

L1S1,...,

LnSn) for a
QBF ψ with different groups of soft variables Sj. We also allow combinations of soft variables
and groups of soft variables within a QBF. In the following we distinguish the two cases by using
capital letters for groups and small letters for variables.

Definition 2 Let ψ(

L1s1,...,

Lnsn) be a QBF with soft variables. We call Λ : Sψ → N the
level function of ψ which maps each variable sj to a quantification level l∈Lj. Given such a level
function Λ we denote ψ(

L1s1,...,

Lnsn)Λ as the QBF where every soft variable is mapped to
one possible quantification level within P of ψ according to Λ. For each soft variable of one soft
variable group sj ∈S the level function has to be same value, i. e. sj = l for a fixed level l and for
all sj ∈S.

Intuitively ψ(

L1s1,...,

Lnsn) is a set of QBF with different prefixes for the soft variables, to
be more precise every QBF resulting from every possible level function Λ of ψ.

Example 1 Consider the QBF with soft variables ψ1 with a matrix ϕ1 = (s1 ∨y)∧(s1 ∨z)∧(y∨
z)∧(s1 ∨y), where s1 is a soft variable in the scope of all existential levels:

ψ1(

{1,3}s1) = ∀y∃z.(s1 ∨y)∧(s1 ∨z)∧(y∨z)∧(s1 ∨y)

By definition we are allowed to set s1 either to the first or third (i. e. an existential) level,
resulting in the two possible level functions with Λ1(s1) = 1 and Λ2(s1) = 3, and therefore in two
possible prefixes P1 =∃s1∀y∃z and P2 =∀y∃z∃s1. The QBF ψ1(

{1,3}s1)Λ1 = P1.ϕ1 is unsatisfiable,
whereas ψ1(

{1,3}s1)Λ2 = P2.ϕ1 results in a satisfied matrix for all branches of the universal variable
y, i. e. is satisfied.

Now consider the formula ψ2 with a matrix ϕ2 = (y∨z)∧(s2 ∨z)∧(s2 ∨y∨z) where s2 is a soft
variable with level 2 and 3 as possible prefix positions:

ψ2(

{2,3}s2) = ∀y∃z.(y∨z)∧(s2 ∨z)∧(s2 ∨y∨z)

By applying the soft variable concept we obtain two possible level functions with Λ3(s2) = 2 and
Λ4(s2) = 3 and the respective prefixes P3 =∀y∀s2∃z and P4 =∀y∃z∃s2. Both ψ2(

{2,3}s2)Λ3 = P3.ϕ2
and ψ2(

{2,3}s2)Λ4 = P4.ϕ2 are satisfiable.

Based on this syntax we briefly define the semantics of a QBF with soft variables.

Definition 3 A QBF with soft variables ψ(

L1s1,...,

Lnsn) is satisfied iff there exists a level
function Λ such that ψ(

L1s1,...,

Lnsn)Λ is satisfied. If for all possible level functions the
resulting QBF is unsatisfied, we say ψ(

L1s1,...,

Lnsn) is unsatisfiable.

We want to consider an optimization problem for QBF with soft variables. To do so, we first
define a score function σ as follows:

Definition 4 Let ψ(

L1s1,...,

Lnsn) be a QBF with soft variables s1,...,sn. The score function
σ : (Sψ×N) →N is defined for each variable sj as σ(sj,l) = χsj,l, where χsj,l is a user-given score

and lj the corresponding level with Λ(sj) = lj. The overall score χΛ is the sum of all scores for one
level function Λ: χΛ =

∑n
j=1 χsj,lj .

The score function allows to define the optimization problem Ω(ψ(

L1s1,...,

Lnsn)) as follows:

Definition 5 Given a QBF with soft variables ψ(

L1s1,...,

Lnsn) and a score function σ of
ψ, the optimization problem Ω(ψ(

L1s1,...,

Lnsn)) is to find a level function Λ maximizing the
score χΛ such that ψ(

L1s1,...,

Lnsn)Λ is satisfied, i. e. Ω(ψ(

L1s1,...,

Lnsn)) = max
Λ

χΛ. If

ψ(

L1s1,...,

Lnsn)Λ is unsatisfied, the score is χΛ = 0.

Example 2 Consider the QBF ψ1 of Example 1. We chose the following scores: σ(s1,1) = 2
and σ(s1,3) = 1. The QBF ψ1(

{1,3}s1)Λ1 is unsatisfied, and therefore the score evaluates to
χΛ1 = χs1,1 = 0. Since ψ1(

{1,3}s1)Λ2 is satisfied, we yield the score χΛ2 = χs1,3 = 1, which is also
the maximum score over all possible level functions Λ of ψ1 and thus the result of the maximization
problem Ω(ψ(

{1,3}s1)) is 1 with Λ2.
Considering ψ2 from Example 1, we chose the scores σ(s,2) = 2 and σ(s,3) = 1. ψ2(

{2,3}s2)Λ3 as
well as ψ2(

{2,3}s2)Λ4 are satisfied and gain the scores χΛ3 = χs2,2 = 2 and χΛ4 = χs2,3 = 1. Hence,
we obtain Ω(ψ2(

{2,3}s2)) = 2 with level function Λ3 as solution to the optimization problem.
Please note, in this example we chose the weights for both formulae in a meaningful way: The

QBF where the soft variable is quantified on a level which is more likely to be unsatisfiable gets
the higher score.

Proposition 1 Solving the optimization problem Ω(ψ(

L1s1,...,

Lnsn)) is PSPACE-complete.

Proof. (Sketch) To decide the optimization problem we need to solve a QBF problem for each
possible level function. QBF is in PSPACE [SM73] and since we only need to store the currently
optimal level function and its score, which needs polynomial space, the optimization problem for
QBF with soft variables is also in PSPACE.

For PSPACE-hardness we reduce from QBF which is PSPACE-hard [SM73]. Let ψ be a QBF
ψ = Q1X1 ...QnXn.ϕ. Let m be a new existential level with m > n. We define a QBF with
soft variables: ψ′(

{1,m}X1,...,

{n,m}Xn) = ϕ, i. e. ψ′ is obtained from ψ by eliminating P and
declaring each variable in X as part of a soft variable group Xi. The possible prefix positions are
chosen such that the whole group Xi is either quantified at level i as in ψ, or at the new level m.
We define the score function σ such that for each soft variable group Xi both σ(Xi,m) = 0 and
σ(Xi,i) = 1 holds, i. e. the preference is to set the group to the level it belonged to in ψ. The
maximization problem for QBF with soft variables tries to set all groups of ψ′ to the corresponding
position in ψ. From the result of the QBF with soft variables problem Ω(ψ′) = max

Λ
χΛ we directly

obtain the satisfiability value of ψ: If at least one soft variable group is not set at level i < m in λ
of ψ′ or max

Λ
χΛ = 0 holds, the QBF ψ is unsatisfiable. Otherwise, if all groups Xi are set to level

i, the QBF ψ is satisfiable.

3.2 Algorithm

In this section we describe an algorithm to solve the optimization problem for QBF with soft
variables which is based on Weighted Partial MaxQBF. To do so, we present an approach for
solving MaxQBF (and its extensions) based on iterative MaxSAT algorithms.

3.2.1 Solving QBF with Soft Variables

Let ψ(

L1s1,...,

Lnsn) = P.ϕ be a QBF with soft variables s1,...,sn, P a prefix over the variables
X, and ϕ a quantifier free matrix over the variables V. In the following we show how to transform

this problem into a Weighted Partial MaxQBF problem. Therefore, we need to transform our
formalism into a QBF without any soft variables.

We denote emax of ψ as the innermost existential level with no further (existential or universal)
quantification level right of emax. Hence, emax is the right-most existential level wrt. the current
prefix P and all levels l∈Lj for all j ∈{1,...,n}.

The following extensions/modifications have to be applied for each soft variable sj, j ∈{1,...,n}:
We quantify sj on level emax existentially such that the appearances of sj in the matrix is well-

defined. For each level l∈Lj we introduce a new quantification of a helper variable slj on level l
and a new free variable flj of ψ. These helper variables allows us to alter the quantification levels by

setting flj appropriately. Therefore, we connect these variables to ϕ by the constraint f
l
j ⇒ (s

l
j ≡sj)

for each l∈Lj, i. e. we set sj to slj (and hence sj quantified on level emax semantically “behaves”
like the variable slj quantified on level l) if the free variable f

l
j is set to >. We have to ensure that

exactly one flj for all l ∈L
j is set to > and all other fkj , k 6= l are set to ⊥, which is also known

as an exactly-one constraint. We add the encoding of such a constraint for each new free variable
of every soft variable to ϕ. We declare every clause of ϕ as well as every additional constraint we
introduced so far as hard clause of the Weighted Partial MaxQBF instance. Finally, we add an
additional unit clause for each free variable flj, declared as soft clause with weight σ(sj,l).

A Weighted Partial MaxQBF solver maximizes these weights, i. e. the score function σ is directly
mapped to a the maximum number of satisfied unit soft clauses triggering a soft variable to be
set on the corresponding position in the prefix. For the free variables flj we obtain a model from

which we can extract the level function Λ: if flj is set to >, Λ(sj) = l holds. By construction, χΛ is
the maximum score of ψ(

L1s1,...,

Lnsn).

Remark 1 Handling groups S of soft variables is analogous to the method described above. Instead
of introducing a free variable flj for each variable and level, we only have to introduce one f

l
S for

each level and group, i. e. every variable of a group S is either quantified simultaneously on l or
not. The additionally introduced constraint is flS ⇒ (s

l
j ≡sj) for each sj ∈S.

Example 3 Consider ψ1 from our running example. First, we introduce the soft variable

{1,3}s1
into P by introducing an existential quantification ∃s1 on level emax = 3. By definition,

{1,3}s1
can be quantified on both existential levels 1 and 3, therefore we introduce two existential helper
variables s11 and s

3
1 as well as two new free variables f

1
1 and f

3
1 . Moreover, we introduce a CNF

representation for the constraints f11 ⇒ (s11 ≡ s1) and f31 ⇒ (s31 ≡ s1), the constraints for the
exactly-one-constraint, and the unit clauses for the free variables into ϕ1, resulting in:

∃s11∀y∃s
3
1∃z∃s1.

original ϕ1︷ ︸︸ ︷
(s1 ∨y)∧(s1 ∨z)∧(y∨z)∧(s1 ∨y)∧
(f11 ∨s

1
1 ∨s1)∧(f11 ∨s11 ∨s1)︸ ︷︷ ︸
f11⇒(s

1
1≡s1)

∧(f31 ∨s
3
1 ∨s1)∧(f31 ∨s31 ∨s1)︸ ︷︷ ︸
f31⇒(s

3
1≡s1)

∧

(f11 ∨f31 )∧(f
1
1 ∨f

3
1 )︸ ︷︷ ︸

exactly-one

∧(f11 )∧(f
3
1 )︸ ︷︷ ︸

soft clauses

This instance is passed to a Weighted Partial MaxQBF solver, where (f11 ) and (f31 ) are declared
as soft clauses with weight 2 and 1 respectively. All other clauses are declared as hard clauses.

Analogously we obtain for ψ2 the following Weighted Partial MaxQBF instance:

∀s22∀y∃s
3
2∃z∃s2. (y∨z)∧(s2 ∨z)∧(s2 ∨y∨z)∧

(f22 ∨s
2
2 ∨s2)∧(f22 ∨s22 ∨s2)∧(f32 ∨s

3
2 ∨s2)∧(f32 ∨s32 ∨s2)∧

(f22 ∨f32 )∧(f
2
2 ∨f

3
2 )∧(f22 )∧(f32 )

with the soft clauses (f22 ) and (f32 ) and weights 2 and 1, respectively.

3.2.2 Solving MaxQBF

In this section we present an approach for solving MaxQBF and its extensions based on iterative
methods from MaxSAT [ZSM03]. The method is also mentioned in [IJM13], but we present some
further details. First, we describe the iterative approach in MaxSAT and then we introduce how
to adapt this technique for MaxQBF.

Iterative MaxSAT solvers as introduced in [ZSM03] add a new relaxation literal r to each soft
clause. If r is set to ⊥, the corresponding soft clause has to be satisfied, otherwise (r = >) the
clause is relaxed, i. e., it is satisfied by the relaxation literal and hence, the (original) soft clause
does not have to be satisfied by the set of variables belonging to the original CNF. Let ϕ be the
original MaxSAT instance with m soft clauses including a unique relaxation literal (r1,...,rm)
for each soft clause. In an iterative approach the relaxation literals are connected to the inputs
of a cardinality network [Sin05] and the instance ϕ∧β(r1,...,rm)∧(oi) is handed over to a SAT
solver, where β(r1,...,rm) is the CNF encoding for such a cardinality network, with r1,...,rm
as inputs and o1,...,om as outputs. The additional unit clause (oi) demands at least i arbitrary
inputs of the network to be set to ⊥, therefore i soft clauses have to be satisfied. If this SAT
instance is satisfiable, there are at least i simultaneously satisfied soft clauses, otherwise there
exists no solution with i satisfied soft clauses. The solution is narrowed by the incremental
usage of the underlying SAT solver until a value k is identified with ϕ∧β(r1,...,rm)∧(ok) being
satisfiable and ϕ∧β(r1,...,rm)∧(ok+1) being unsatisfiable. This value k is the maximum number
of simultaneously satisfied soft clauses.

This procedure can be easily extended to the Partial MaxSAT and Weighted MaxSAT concepts:
In Partial MaxSAT, hard clauses are not connected to the network, and in Weighted MaxSAT
a soft clause c is connected ω(c) times into the network, where ω(c) is the weight of the clause
c. The algorithm for Weighted Partial MaxSAT is obtained by a straight-forward combination of
both methods.

We adapt this concept for MaxQBF by using an incremental QBF solver. The cardinality
network and the relaxation variables are encoded as in MaxSAT. The variables for the encoding
are added as free variables of the QBF, since a soft clause has to be satisfied for every branch
of the universal variables and we are able to obtain a model for these variables as a result from
solving the open QBF. Likewise to MaxSAT we call the QBF solver incrementally in order to find
a value k such that the QBF with k satisfied soft clauses is satisfied, but unsatisfied with k + 1
clauses. The extension for Partial MaxQBF, Weighted MaxQBF and Weighted Partial MaxQBF
is done in the same manner as for the MaxSAT extension.

3.2.3 Implementation Details

We implemented a Weighted Partial MaxQBF solver as well as the algorithm for solving QBF with
soft variables.

For the MaxQBF solver we used the QBF solver quantom [RPSB12] and implemented incremental
functionality based on [MMB12]. For the model of the free variables (representing the level function
Λ) we adapt techniques of [BELM12]. For scalability reasons we also use a preprocessor for QBF.
The preprocessor is implemented for incremental usage (see also [MMLB12]) as well as model
preservation techniques known from SAT [EB05] adapted to QBF. All variables which are introduced
in context of a soft variable are set as “Don’t touch”[KLSB11] in the preprocessor, i. e. these
variable are excluded from several preprocessing techniques, among others variable elimination and
pure literal detection.

For an exactly-one-constraint with more than 5 possible levels (i. e. |Lj|> 5), we use the encoding
for LT

n,1
SEQ as presented in [Sin05] using O(|L

j|) clauses and O(|Lj|) additional auxiliary variables

only. Otherwise we introduce a standard one-hot encoding using O(|Lj|2) additional clauses.2
For some instances (cf. §4.1) the encoding can be simplified to a pure Partial MaxQBF problem

if the following requirements hold: 1) the soft variables are only defined over two different levels
and 2) for all soft variables the weight function assigns for one level 0 and for the other level a
constant value c > 0. If this is the case we can add just one free variable per soft variable with the
constraints: flj ⇒ (s

l
j ≡sj) and flj ⇒ (s

k
j ≡sj), where l is the preferred level with weight c and k is

the level with weight 0. Moreover, just one soft clause (flj) for each soft variable is added.

4 Applications

In this section we present several applications, mainly from verification and testing of circuits,
covered by QBF with soft variables. In §4.1 we present optimization problems considering unknowns
in a circuit, and in §4.2 we present further applications, for example optimal solutions for dependency
schemes.

The measurements for all case studies were performed on a machine using one core of a 3.3 GHz
Intel Xeon, and limiting the memory to 4 GB.

4.1 Maximizing Unknowns in a Circuit

There are plenty of applications which ask for maximizing or optimizing unknown values within
a circuit. There are two general problem statements, given a circuit together with a property
which has to hold, we want to optimize: 1) The solution by introducing unknown values for the
internal circuit lines or the inputs, and 2) secondary objectives in presence of unspecified values
such that the property still holds. In the first case the unknown values generalize (or uniform)
the solution, whereas in the second case some parts of the circuit are abstracted by introducing
universal quantifications in an appropriate QBF and we want to optimize further objectives in
presence of these unknowns.

In the following part of this section we briefly review classical algorithms discussing differences to
the QBF with soft variable formulation. Finally, we introduce specific problem statements as well
as first case studies for some application with our prototype solver. We define a metric representing
the quality loss of heuristic methods compared to our approach as: loss(Method) = 1− XM ethod

XQBF
where XMethod is the number of maximized unknowns computed by an approximate method, and
XQBF is the value computed by QBF using soft variables.

4.1.1 Comparison to Previous Work

To model unknown values in a circuit, commonly 01X-encoding [JBM+00] applying SAT-based
methods is used. Another popular SAT-based heuristic is lifting [RS04] which was introduced for
minimal counterexamples (cf. §4.1.6). This method does not need any 01X-encoding, instead the
optimization is done directly on the extracted model of a satisfied SAT instance.

However, 01X-logic is a pessimistic abstraction. In many applications, more precise solutions
which then need a QBF formulation for the unknown values [SB01] are preferred. And although in
an optimal case the lifting technique yields solutions as exact as a QBF formulation, it does not
guarantee optimal ones due to its heuristic methodology. In QBF each unknown value is associated
to a universally quantified variable. In contrast to SAT-based methods, the maximization with
classical QBF-based methods is a harder problem, since the semantics of QBF binds each variable
to its quantifier, i. e. the quantifier is statically declared and cannot be changed to the purpose of
optimizing over unknown lines.

2 As shown in [Sin05] the encoding for LT
n,1
SEQ

is superior to the näıve encoding for n > 5.

QBF with soft variables overcomes this issue. For any line which is part of the unknown
maximization a soft variable is introduced, and this allows to switch between existential (known)
and universal (unknown) quantification (values). Shortly, the QBF with soft variables concept
provides a compact representation for modelling unknowns, which is more precise than classical
01X-based approaches and guarantees optimal solution in general. More details of the encoding
are presented in the following subsections.

4.1.2 Uniform Counterexamples

Exploiting partial designs is useful e. g. in the following cases: 1) Abstraction of complex parts of
the system, 2) early step of the design process where not all parts are done, and 3) for diagnosis –
in case a bug is present in the design and it is still present while parts are removed, there must
be errors outside the black boxes. There exist different encoding methods for these hidden parts
(usually called black boxes ) [SB01], and the approach for using them in a BMC context [NSB07] is
the so-called Black Box Bounded Model Checking (BBBMC).

One question in BBBMC is whether a property of the system is satisfied for each possible
realization of the black boxes. A BBBMC can be written as the following QBF problem: ψ =
∃X1∀Z1∃X2∀Z2 ...∃Xk∀Zk.I0 ∧T0,1 ...∧Tk−1,k ∧¬Pk, where Xi are the inputs of the transition
relation and Zi are the outputs of the black box at depth i. If the property cannot be fulfilled, it is
interesting to obtain a counterexample for the inputs Xi. Using this encoding, only the assignments
for the inputs X1 are the same for each possible black box implementation – all other inputs
may differ depending on the black box implementation. To overcome this issue one can define a
uniform QBF prefix as follows: ψuni = ∃X1 ...∃Xk∀Z1 ...∀Zk.I0 ∧T0,1 ...∧Tk−1,k∧¬Pk. Note that
these two representations are not equivalent: ψ ensures that the primary inputs of each unrolling
depth can “react” to the black box output, whereas in ψuni the inputs are independent from the
black box implementation. Hence, ψ is more accurate than ψuni, nonetheless ψuni returns a more
general counterexample. In [NSB07] the authors specify partially uniform QBF, i. e., parts of a
counterexample which can be generalized without losing accuracy are identified. The proposed
method uses symbolic model checking modelling the unknown values with the pessimistic 01X-logic.

QBF with Soft Variables Formulation The uniform counterexample problem can be solved
optimally in the number of inputs which are uniform by applying QBF with soft variables. Let
xij ∈Xi and |Xi| be the number of variables in Xi. We state the QBF with soft variables prob-
lem as follows: ψ(

{1,3}x
3
1,...,

{1,3}x
3
|X3|,...,

{1,k}x
k
|Xk|

) = ∃X1∀Z1∃∅∀Z1 ...∃∅∀Zk.I0∧T0,1 ...∧
Tk−1,k∧¬Pk, i. e. for each input variable at level i we introduce a soft variable trying to shift the
quantifier to the first level. Once a variable is quantified at the first level and the QBF is still
satisfied, this input is independent from every black box and therefore uniform. We choose the
score function σ such that level 1 is more advisable than level i, the solution of the QBF with soft
variables problem is the optimal uniform counterexample.

For this and all upcoming applications in §4.1, the score function assigns the same score for each
variable, e. g. 1 for the preferred level and 0 for the non-preferred (cf. §3.2.3). In this case, we
obtain a globally optimal result. But it would be also possible to prefer particular variables by
assigning larger scores.

4.1.3 Diagnosis

As described in §4.1.2, black boxes can be used for diagnosis tasks: If a property of the system
is violated regardless of the excluded parts, the failure has to occur in the non-excluded part.
A challenge is to identify the black boxed part automatically, such that the remaining sub-circuit is
as small as possible. In this case already the non-abstracted circuit is sufficient for the violation of

the property which would simplify the diagnosis task. To the best of our knowledge this problem
statement is not tackled so far, even with pessimistic 01X-encoding.

Using QBF with Soft Variables Using the standard Tseitin-encoding [Tse68] to produce a
propositional formula, every line li is associated to a Boolean variable. Hence we can define a soft
variable for each line3 obtaining the following QBF with soft variables: ψ(

{2,3}l1,...,

{2,3}lk) =
∃∅∀∅∃x1 ...∃xn.ϕ∧¬P, where xi are inputs of the circuit, ϕ its encoding, and ¬P the violated
property. By preferring universal quantification in the score function, the result of the optimization
problem indicates a maximal number of lines, which can be excluded such that the bug is still
present. Note, that this result is not accurate anymore in this scenario as discussed in §5. In
order to reduce the complexity one may not consider every line but only specific ones, or consider
different groups of lines separately and examine them incrementally.

4.1.4 Circuit Initialization

The problem of circuit initialization is a well known problem in the area of testing [PR00] and
is closely related to state reachability problems known from BMC [RSSB14]. The problem asks
whether a sequential circuit is initializable, i. e. all flip-flops can be set to a known value assuming
the initial state is (completely) unknown. If this is not the case (which usually applies), one can
seek for two related optimization questions: 1) starting from a unknown state what is the maximum
number of initialized flip-flops, or 2) what is the smallest number of initially controlled flip-flops
needed to initialize the complete circuit. For both objectives a minimal trace length is preferred.

Classical approaches either solve this problem heuristically (e. g. [PR00]) or are complete, but
only with the pessimistic 01X-logic (cf. [RSSB14]). So far there is no approach that applies a
complete method using the accurate QBF modelling for the unknown values.

Using QBF with Soft Variables Based on the method in [RSSB14], we can define a BMC
problem based on QBF with soft variables. Let gij ∈Gi be a variable representing the value of
a flip-flop at depth i and |Gi| the number of variables in Gi. For the objective 1) we obtain:
ψ(

{1,2}g
k
1,...,

{1,2}g
k
|Gk|

) = ∃∅∀G0∃G1 ...∃Gk−1.I0 ∧T0,1 ...∧Tk−1,k∧Pk. If the score functions
recommend to quantify a soft variable existentially on the first level, the maximum number of
initialized flip-flops in time step k is given by the number of these existentially quantified variables.
The second objective 2) can be expressed as: ψ(

{2,3}g
0
1,...,

{2,3}g
0
|G0|) =∃Gk∀∅∃G1 ...∃Gk−1.I0∧

T0,1 ...∧Tk−1,k∧Pk. Here, Gk is quantified on the first level since we have to ensure that the value
for the flip-flops in the k’th time step are fixed to a specific known value independently from the
potentially unknown flip-flop values of the initial time step 0. By applying a score function favoring
the quantification of soft variables at the universal level 2, the result for this optimization problem
is equivalent to the minimum number of controlled flip-flops in the first time step.

Note, in contrast to the method in [RSSB14], this approach does not contain a proof whether
more flip-flops can be initialized in further time steps, but it provides more accurate results as
shown in the following case study.

Case Study We applied the encoding to the benchmark b06 from the ITC 99 benchmark series
which is commonly used in the EDA community and previously proven to be not completely
initializable using 01X-encoding [RSSB14]. However, using QBF with soft variables, we have
identified an initialization sequence of 5 time steps driving each flip-flop to a specified value.

3 It may be meaningful to define groups of lines (e. g. buses or outputs of a specific module such as multiplier), which
can be defined analogously.

b0
6

b0
7

b0
8

b0
9

b1
0

b11

b1
2

b1
3

b1
5

s0
11

9
6

s0
1
2
3
8

s0
1
4
2
3

s0
1
4
8
8

s0
1
4
9
4

s0
5
3
7
8

s1
3
2
0
7

s3
5
9
3
2

s3
8
4
1
7

10%

15%

20%

25%

01X Lifting Simulation

Figure 1: Loss for test pattern relaxation using approximated methods

4.1.5 Test Pattern Relaxation

In the area of testing [JG03] and in particular Automatic Test Pattern Generation (ATPG) the
number of specified input bits in a test pattern is a major quality metric. Partially specified test
patterns, so-called test cubes, serve as a foundation for further post-processing steps controlling
secondary objectives, e. g. compaction, or test power reduction. As the quality of these methods
depends on the number of unspecified values, test patterns with a greater amount of unspecified
inputs are preferred.

Using QBF with Soft Variables Once a test pattern is found, we introduce soft variables for
all inputs x1,...,xn in order to preferably treat them as unknowns. A resulting QBF may look
like: ψ(

{2,3}x1,...,

{2,3}xn) = ∃∅∀∅∃Y.ϕ, where ϕ is the encoding of the circuit using variables
V and the property justifying the test pattern. If the score function is built favoring the universal
quantification level, one obtains the maximum number of lines that can be excluded from the test
pattern such that the fault is still visible.

Case Study In [SRP+13] an approach using an accurate QBF modeling was already presented,
however without using the soft variable concept. For the common ISCAS 89 and ITC 99 benchmark
circuits we generated minimal test cubes for 100 test pattern detecting small delay faults [JG03].
We used QBF with soft variables to document the quality loss of common heuristics (01X, lifting,
and simulation) in the number of unspecified inputs compared to the optimal solution. Fig. 1
shows the quality loss for different benchmarks. As it can be seen, depending on the internal
structure of the individual benchmark the heuristics can identify up to 23% less unspecified inputs
for benchmark circuit b09.

4.1.6 Minimal Counterexamples

SAT-based Bounded Model Checking (BMC) [BCC+03] is a formal verification technique for
designs modeled as finite state machines (FSM). The transition relation of the FSM is unrolled
step by step and a property is verified at the current depth. The depth k is incremented until
either the property is violated for the given depth, or a user-defined bound for the depth is reached.
A SAT formula for the BMC problem can be written as: ϕ = I0∧T0,1∧...∧Tk−1,k∧¬Pk, where I0
is the initial state of the system, Ti,i+1 is the transition relation for step i and Pk is the property
at step k. Note that ϕ is true iff the property is violated.

In case of a violated property the model of ϕ represents a full trace of assignments to the primary
inputs of the transition relation (i.e. a counterexample) of the current unrolling depth. This trace
can be used for diagnosis or abstraction refinements. In order to improve the diagnosis routines

Table 1: Results for HWMCC benchmarks

QBF Lifting
Family Inst. Inputs Time X Time X Loss

beemi* 14 / 0 489.71 0.60 17.50 4.01 17.50 0.00
beemsch* 16 / 0 320.38 1.03 13 0.68 12 0.31
bj* 12 / 1 16.27 0.07 14.36 0.02 14.36 0.00
brpp* 5 / 0 177.40 287.46 58.40 0.14 46.20 20.76
counter* 2 / 0 82.00 0.01 21.00 0.02 20.50 2.38
dme* 20 / 0 455.35 6.95 301.20 0.37 262.45 12.12
ken* 2 / 0 268.68 3.48 161.10 0.19 141.48 7.25
pci* 5 / 0 477.25 91.64 282.50 0.29 282.50 0.00
srg* 3 / 0 81.00 0.29 25.67 0.02 11.33 52.12
texas* 9 / 1 117.63 6.29 102.88 0.49 101.63 0.80
vis* 6 / 2 78.00 49.52 45.00 0.18 44.00 2.30

total 94 / 4 288.32 25.74 102.88 0.91 92.87 5.98

the number of primary inputs, which are needed to justify the violation of the property, can be
delimited.

Note that the test pattern relaxation problem as described in §4.1.5 can be seen as a special
case of the minimal counterexample problem. Instead of asking whether a property is violated, we
ask whether a property (detection of a fault) holds minimizing the number of specified inputs (test
cube).

Using QBF with Soft Variables Consider a BMC problem ϕ as stated above with a coun-
terexample at depth k. We denote X = x1,...,xn as the variables representing all inputs of the
transition relations and Y = y1,...,ym all other variables in ϕ. In order to minimize the number of
specified inputs (or maximize the unknown inputs), we state the following QBF with soft variables
instance: ψ(

{2,3}x1,...,

{2,3}xn) =∃∅∀∅∃Y.ϕ, i. e. a QBF containing only existentially quantified
variables Y on level 3 and the soft variables X. If we define the score function σ such that the
universally quantified position gets a larger score than the existential position, the result of Ω(ψ)
returns the maximum number of inputs which can be excluded from the counterexample such the
property is still unsatisfied. Hence, we obtain a counterexample with a minimal number of specified
inputs.

Case Study We considered 94 unsatisfiable BMC benchmarks from 11 classes of the Hardware
Model Checking Competitions (2010, 2011 and 2012). We selected the Bounded Model Checker
cip [KLSB11] which is able to extract counterexamples from buggy benchmark designs. For
some groups with smaller number of inputs we computed the minimal counterexamples for these
benchmarks, and compared them with the results obtained by applying a lifting algorithm.

The results are given in Table 1. In the first three columns the family name, the number of
overall / non-solved QBF instances within a timeout of 30 CPU minutes, and the average number
of inputs of the original counterexample are given. In order to compare results, the following
columns contains only results for the instances where the QBF approach was able to provide a
solution. The following two columns show the average run time in seconds and the average number
of inputs we can exclude from the counterexample using QBF with soft variables. The next two
columns show the same for the lifting approach, and the last column indicates the average quality
loss of the lifting approach.

On average the loss of accuracy with lifting is about 6% compared to the exact QBF with soft
variables. However, for some benchmarks the loss is over 70% (instance brpptimeonenegnv). The
run times for these smaller examples are very reasonable with just 4 non-solved benchmarks, but
our approach still has scaling issues, especially if the number of lines to maximize is large.

4.2 Further applications

For the task of finding optimal dependency schemes [Sam08] one can use the optimization problem
for QBF with soft variables. Therefore, we declare a single existential variable of the original
problem as soft variable allowing to be quantified on all existential prefix position. In the score
function we prefer the position with the least dependencies on universally quantified variables as
possible.

Another application area where QBF with soft variables may be a useful mechanism is planning
and decision making, which are common problems evolving from the game theory domain. In a
multi-agent environment, where more than one player is present, such problems ask to determine
the best action. Hence, the goal is to find the action model with the highest score. In [YWJ07]
a weighted MaxSAT solver is used to determine these models. But this approach is limited if
we consider uncertainness of other players’ action, the environment or possibly unknown actions
performed earlier. Using MaxQBF one’s own action score could be maximized with accuratly
modeled behaviour of the enviroment. Moreover, by using QBF with soft variables it can be
determined whether the order of the actions can be altered or even if an action can be left out in
order to decrease the overall costs.

A related problem are two-players games [AMN05], which can be naturally formulated with QBF
logic by giving the existential quantifier (resp. the universal quantifier) the role of the system player
(resp. the environment player). As in the planning problem one could try to make own moves
independent from the opponent ones using QBF with soft variables for the existential variables.
This would lead to more generalized winning strategies. This problem is related to the uniform
counterexamples (cf. §4.1.2) and can be tackled in a similar manner.

5 Conclusions

We presented first results on the novel concept of soft variables for quantified Boolean formulae.
The related optimization problem allows to optimize the prefix according to a user-given preference.
Furthermore, we introduced a MaxQBF solver and a sound and complete algorithm to solve QBF
with soft variables using MaxQBF.

Recent improvements in classical algorithms for SAT and QBF lead to new research interests
in answering beyond yes/no questions. Such optimization problems using quantified formulas are
often hard to encode due to the static prefix or rather predefined dependencies of the variables.
The concept of soft variables overcomes this issues and opens a wide field of such applications
requiring an accurate model. We demonstrated the applicability of our formalism by introducing
several applications in the area of formal verification, debugging, testing and artificial intelligence.

However, also QBF is limited if the abstracted part modeled by universally quantified variables
either show sequential behavior or there are multiple black box parts with overlapping cones of
the black box inputs and outputs. In these cases QBF (hence also QBF with soft variables) is not
accurate anymore [GRS+13]. To overcome the latter issue one can define explicit dependencies of the
variables rather than defining a linear prefix. This extension is known as Dependency QBF (DQBF)
using so-called Henkin quantifiers, where variables are quantified with a explicitly given variable set
of dependencies [Hen61]. The definition of a DQBF with soft variables is straightforward: instead
of possible prefix positions a soft variable is allowed to be quantified with different dependency
sets4. Research interest starts on focusing DQBF algorithms and applications [GRS+13], but the
scalability of these algorithms is still not reasonable for tackling even more complex optimization
problems (deciding pure DQBF is already NEXPTIME-complete [PRA01]). Therefore we do
not consider soft variables for DQBF in this paper, but it may become relevant if appropriate
algorithms for solving DQBF are present.

As future work we want to investigate the new application areas covered by our soft variable

4 Actually, the prefix of a QBF is just a convenient notation for a linear dependency relation between the variables.

mechanism as well as dedicated solving mechanisms beyond the techniques used for MaxSAT/QBF-
based algorithms to increase the scalability.

[AMN05] R. Alur, P. Madhusudan, W. Nam. Symbolic computational techniques for solving
games. STTT 7(2):118–128, 2005.

[BCC+03] A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, Y. Zhu. Bounded model checking.
Advances in Computers 58:117–148, 2003.

[BELM12] B. Becker, R. Ehlers, M. Lewis, P. Marin. ALLQBF Solving by Computational Learning.
In ATVA. LNCS 7561, pp. 370–384. Springer, 2012.

[BHMW09] A. Biere, M. Heule, H. van Maaren, T. Walsh (eds.). Handbook of Satisfiability.
Frontiers in Artificial Intelligence and Applications 185. IOS Press, 2009.

[BLV08] M. Benedetti, A. Lallouet, J. Vautard. Quantified constraint optimization. In Principles
and Practice of Constraint Programming. Pp. 463–477. 2008.

[CFLS93] A. Condon, J. Feigenbaum, C. Lund, P. Shor. Probabilistically checkable debate
systems and approximation algorithms for PSPACE-hard functions. In Proceedings of
the 25th annual ACM symposium on Theory of computing. Pp. 305–314. 1993.

[CP04] H. Chen, M. Pál. Optimization, games, and quantified constraint satisfaction. In
Mathematical Foundations of Computer Science 2004. Pp. 239–250. Springer, 2004.

[EB05] N. Eén, A. Biere. Effective Preprocessing in SAT through Variable and Clause Elimi-
nation. In SAT. 2005.

[GNT07] E. Giunchiglia, M. Narizzano, A. Tacchella. Quantifier Structure in Search-Based Pro-
cedures for QBFs. IEEE Trans. on CAD of Integrated Circuits and Systems 26(3):497–
507, 2007.

[GRS+13] K. Gitina, S. Reimer, M. Sauer, R. Wimmer, C. Scholl, B. Becker. Equivalence
Checking of Partial Designs Using Dependency Quantified Boolean Formulae. In Proc.
of the 31st IEEE Int’l Conf. on Computer Design. Pp. 396–403. 2013.

[HB07] M. Herbstritt, B. Becker. On Combining 01X-Logic and QBF. In EUROCAST. Lecture
Notes in Computer Science 4739, pp. 531–538. Springer, 2007.

[Hen61] L. Henkin. Some remarks on infinitely long formulas. In Infinitistic Methods: Proceed-
ings of the 1959 Symposium on Foundations of Mathematics. Pp. 167–183. Pergamon
Press, Sept. 1961.

[IJM13] A. Ignatiev, M. Janota, J. Marques-Silva. Quantified Maximum Satisfiability. In SAT.
Pp. 250–266. Springer, 2013.

[JBM+00] A. Jain, V. Boppana, R. Mukherjee, J. Jain, M. Fujita, M. S. Hsiao. Testing, Verifica-
tion, and Diagnosis in the Presence of Unknowns. In VLSI Test Symp. Pp. 263–269.
2000.

[JG03] N. K. Jha, S. K. Gupta. Testing of Digital Systems. Cambridge U. Press, 2003.

[KLSB11] S. Kupferschmid, M. Lewis, T. Schubert, B. Becker. Incremental Preprocessing Meth-
ods for Use in BMC. Formal Methods in System Design, pp. 1–20, 2011.

[MMB12] P. Marin, C. Miller, B. Becker. Incremental QBF Preprocessing for Partial Design
Verification - (Poster Presentation). In SAT. LNCS 7317. Springer, 2012.

[MMLB12] P. Marin, C. Miller, M. Lewis, B. Becker. Verification of partial designs using incre-
mental QBF solving. In DATE. Pp. 623–628. 2012.

[NSB07] T. Nopper, C. Scholl, B. Becker. Computation of minimal counterexamples by using
black box techniques and symbolic methods. In ICCAD. Pp. 273–280. 2007.

[PR00] I. Pomeranz, S. M. Reddy. On synchronizable circuits and their synchronizing sequences.
IEEE Trans. on CAD of Integrated Circuits and Systems 19(9):1086–1092, 2000.

[PRA01] G. Peterson, J. Reif, S. Azhar. Lower Bounds for Multiplayer Non-Cooperative Games
of Incomplete Information. Computers & Mathematics with Applications 41(7–8):957–
992, 2001.

[RPSB12] S. Reimer, F. Pigorsch, C. Scholl, B. Becker. Enhanced Integration of QBF Solving
Techniques. In MBMV. Pp. 133–143. 2012.

[RS04] K. Ravi, F. Somenzi. Minimal Assignments for Bounded Model Checking. In TACAS.
Lecture Notes in Computer Science 2988, pp. 31–45. Springer, 2004.

[RSSB14] S. Reimer, M. Sauer, T. Schubert, B. Becker. Using MaxBMC for Pareto-Optimal
Circuit Initialization. In DATE. 2014.

[Sam08] M. Samer. Variable dependencies of quantified CSPs. In Logic for Programming,
Artificial Intelligence, and Reasoning. Pp. 512–527. 2008.

[SB01] C. Scholl, B. Becker. Checking equivalence for partial implementations. In Design
Automation Conference, 2001. Proceedings. Pp. 238 – 243. 2001.

[Sin05] C. Sinz. Towards an optimal CNF encoding of Boolean cardinality constraints. In
Principles and Practice of Constraint Programming-CP 2005. Pp. 827–831. Springer,
2005.

[SM73] L. J. Stockmeyer, A. R. Meyer. Word problems requiring exponential time (Preliminary
Report). In Proceedings of the Fifth Annual ACM Symposium on Theory of Computing.
STOC ’73, pp. 1–9. ACM, New York, NY, USA, 1973.

[SRP+13] M. Sauer, S. Reimer, I. Polian, T. Schubert, B. Becker. Provably optimal test cube
generation using quantified Boolean formula solving. In ASP-DAC. Pp. 533–539. IEEE,
2013.

[Tse68] G. Tseitin. On the Complexity of Derivation in Propositional Calculus. Studies in
Constructive Mathematics and Mathematical Logic, 1968.

[YWJ07] Q. Yang, K. Wu, Y. Jiang. Learning action models from plan examples using weighted
MAX-SAT. Artif. Intell. 171(2-3):107–143, 2007.

[ZSM03] H. Zhang, H. Shen, F. Manya. Exact algorithms for MAX-SAT. Electronic Notes in
Theoretical Computer Science 86(1):190–203, 2003.

Introduction
Preliminaries
QBF
MaxQBF

QBF with Soft Variables
Soft Variables
Algorithm
Solving QBF with Soft Variables
Solving MaxQBF
Implementation Details

Applications
Maximizing Unknowns in a Circuit
Comparison to Previous Work
Uniform Counterexamples
Diagnosis
Circuit Initialization
Test Pattern Relaxation
Minimal Counterexamples

Further applications

Conclusions