=Paper=
{{Paper
|id=None
|storemode=property
|title=The incremental satisfiability problem for a
two conjunctive normal form
|pdfUrl=https://ceur-ws.org/Vol-1659/paper4.pdf
|volume=Vol-1659
|authors=Guillermo De Ita,J. Raymundo Marcial-Romero,J. A. Hernández
|dblpUrl=https://dblp.org/rec/conf/lanmr/LunaMH16
}}
==The incremental satisfiability problem for a
two conjunctive normal form==
https://ceur-ws.org/Vol-1659/paper4.pdf
The Incremental Satisfiability Problem for a
Two Conjunctive Normal Form
Guillermo De Ita1 , J. Raymundo Marcial-Romero2 and J. A. Hernández2
1
Faculty of Computer Sciences, BUAP
2
Facultad de Ingenierı́a, UAEM
deita@cs.buap.mx, jrmarcialr@uaemex.mx, xoseahernandez@gmail.com.mx
Abstract. We propose a novel method to review K ` φ when K and
φ are both in Conjunctive Normal Forms (CF). We extend our method
to solve the incremental satisfiablity problem (ISAT), and we present
different cases where ISAT can be solved in polynomial time.
Keyword: Satisfiability Problem, Incremental Satisfiability Problem, 2-
SAT, Entail Propositional Problem, Efficient Satisfiability Instances.
1 Introduction
The primary goal of complexity theory is to classify computational problems ac-
cording to their inherent computational complexity. A central issue in determin-
ing these frontiers has been the satisfiability problem (SAT) in the propositional
calculus. The case 2-SAT, to determine the satisfiability of propositional two
Conjunctive Normal Forms (2-CF), is an important tractable case of SAT. Vari-
ations of the 2-SAT problem, e.g. in the optimization and counting area, have
been key for establishing frontiers between tractable and intractable problems.
One of the fundamental problems in automatic reasoning is the propositional
entail problem which is a relevant task in many other issues such as estimating
the degree of belief, to review or update beliefs, the abductive explanation, logical
diagnosis, and many other procedures in Artificial Intelligence (AI) applications.
It is known that logic entail problem is a hard challenge in automatic rea-
soning due to it is co-NP-Hard even in the propositional case [8]. However, some
fragments of propositional logic allow efficient reasoning methods [3]. One of the
most relevant cases of efficient reasoning is the fragment of Horn Formulas. We
present a novel method to solve the entail problem between conjunctive forms
and how to apply it for solving the incremental satisfiability problem (ISAT).
Hooker [7] presented an algorithm for the ISAT problem, in which the main
contribution was the speed-up for solving a single formula by solving a growing
subset of its constraints. Whittemore et al. [11] defined the incremental satisfia-
bility problem as the solving of each formula in a finite sequence of subformulas.
Wieringa [12] presented an incremental satisfiability solver and some of its ap-
plications. Finally, Nadel [10] presented a variation of ISAT problem under
assumptions that are modeled as first decision variables; all inferred clauses that
depend on some of the assumptions include their negation.
25
We present here an algorithm for solving the 2-ISAT problem, and we es-
tablish an upper bound for the time-complexity of 2-ISAT, as well as, we show
some efficient cases for the ISAT and the 2-ISAT problems.
2 Preliminaries
Let X = {x1 , . . . , xn } be a set of n Boolean variables. A literal is either a variable
xi or a negated variable xi . As usual, for each x ∈ X, x0 = x and x1 = x.
A clause is a disjunction of different and non-complementary literals. Notice
that we discard the case of tautological clauses. For k ∈ IN , a k-clause is a
clause consisting of exactly k literals, and a (≤ k)-clause is a clause with at
most k literals. A phrase is a conjunction of literals, a k-phrase is a phrase with
exactly k literals.
A conjunctive normal form (CNF, or CF) F is a conjunction of clauses. We
say that F is a monotone positive CF if all of its variables appear in unnegated
form. A k-CF is a CF containing only k-clauses. (≤ k)-CF denotes a CF con-
taining clauses with at most k literals. A 2-CF formula F is said to be strict
only if each clause of F consists of two literals. A disjunctive normal form (DF)
is a disjunction of phrases, and a k-DF is a DF containing only k-phrases.
A variable x ∈ X appears in a formula F if either x or x is an element of
F . We use υ(X) to represent the variables involved in the object X; where X
can be a literal, a clause, or a CF. Lit(F ) is the set of literals involved in F , i.e.
if X = υ(F ), then Lit(F ) = X ∪ X = {x1 , x1 , ..., xn , xn }. Also we used ¬Y as
the negation operator on the object Y . We denote {1, 2, ..., n} by [[n]], and the
cardinality of a set A by |A|.
An assignment s for a formula F is a function s : υ(F ) → {0, 1}. An assign-
ment s can also be considered as a set of literals without a complementary pair
of literals, e.g., if l ∈ s, then l 6∈ s. Let c be a clause and s an assignment, c is
satisfied by s if and only if c ∩ s 6= ∅. On the other hand, if for all l ∈ c, l ∈ s,
then s falsifies c.
Let F be a CF, F is satisfied by an assignment s if each clause in F is satisfied
by s. F is contradicted by s if any clause in F is falsified by s. A model of F
is an assignment for υ(F ) that satisfies F . A falsifying assignment of F is an
assignment for υ(F ) that contradicts F . A DF F is satisfied by s if any phrase
is satisfied by s. F is contradicted by s if all of its phrases are contradicted by s.
If n = |υ(F )|, then there are 2n possible assignments defined over υ(F ). Let
S(F ) be the set of 2n assignments defined over υ(F ). s ` F denotes that the
assignment s is a model of F . s 6` F denotes that s is a falsifying assignment of
F . If F1 ⊂ F is a formula consisting of some clauses from F , and υ(F1 ) ⊂ υ(F ),
an assignment over υ(F1 ) is a partial assignment over υ(F ). If s has logical values
determined for each variable in F then s is a total assignment of F .
The SAT problem consists on determining whether F has a model. SAT(F )
denotes the set of models of F , then SAT(F ) ⊆ S(F ). The set FAL(F ) =
S(F ) \ SAT (F ) consists of the assignments from S(F ) that falsify F . Clearly,
for any propositional formula F , S(F ) = SAT (F ) ∪ F AL(F ).
26
A Knowledge Base (KB) is a set K of formulas. Given a KB K and a propo-
sitional formula φ, we say that K implies φ, and we write K ` φ, if φ is satisfied
for each model of K, i.e., if SAT (K) ⊆ SAT (φ). This last problem is known as
the propositional entail problem. The incremental satisfiability problem (ISAT)
consists in deciding if an initial knowledge Base K keeps its satisfiability anytime
a conjunction of new clauses φ is added.
3 Computing falsifying assignments of CF’s
Vm
Assume a KB K in CF, K = i=1 Ci , where each Ci is a clause, i ∈ [[m]]. For
each clause Ci , i ∈ [[m]], the assignment s(Ci ) = 1 contains at least one literal
in Ci . It is easy to build F AL(K) since each clause Ci ∈ K determines a subset
of falsifying assignments of K. The following lemma expresses how to form the
falsifying set of assignments of a CF.
Vm Sm
Lemma 1 Given a CF K = i=1 Ci , it holds that F AL(K) = i=1 {σ ∈ S(K) |
F AL(Ci ) ⊆ σ}
Lemma 2 If a CF K is satisfiable, then ∀K 0 ⊆ K, K 0 is a satisfiable CF.
Corollary 1 If a CF K is unsatisfiable, then ∀ CF K 0 such that K ⊆ K 0 , K 0
remains unsatisfiable.
Now, let us consider the propositional entail problem: K ` φ, where K and
φ are CF’s. The decision problem K ` φ is a classical Co-NP-Complete problem
for CF’s in general, since this problem is logically equivalent to the tautology
problem for any DF, which is a classic co-NP-complete problem.
On the other hand, K ` φ iff SAT (K) ⊆ SAT (φ), and this last goal is
equivalent to prove F AL(φ) ⊆ F AL(K), due to basic properties on sets that are
closed under complementation.
Lemma 3 F AL(φ) ⊆ F AL(K) if and only if K ` φ.
The best known case of an efficient method for the inference K ` φ between
CF’s is when both K and φ are Horn formulas. In this case, the application of
SLD-resolution leads to a linear-time process for deciding K ` φ. The appli-
cation of SLD-resolution has been the mechanism most commonly used in the
development of logic programming languages [5].
However, including 2-CF’s as extensions of a Horn formula and continue
applying SLD-resolution method as the inference engine, gives an exponential-
time complexity process on the number of Horn inferences to perform.
Despite of the refutation methods commonly used in the Horn inference, Vm we
consider here another method to determine whether K ` φ. When K = i=1 Ci
Vk
and φ = i=1 ϕi , our method focuses on checking that F AL(φ) ⊆ F AL(K) in
order to prove K ` φ.
Each set F AL(Ci ) can be represented in a succinct way via a string Ai of
length n = |υ(K)|. Given a clause Ci = (xi1 ∨. . .∨xik ), the value at each position
27
from i1 -th to ik -th of the string Ai is fixed with the truth value falsifying each
literal of Ci . E.g., if xij ∈ Ci , the ij -th element of Ai is set to 0. On the other
hand, if xij ∈ Ci , then the ij -th element is set to 1.
The variables in υ(K) which do not appear in Ci are represented by the
symbol ’*’ meaning that they could take any logical value in the set {0, 1}. In
this way, the string Ai of length n = |υ(K)| represents the set of assignments
falsifying the clause Ci .
We call falsifying string to the string Ai representing the set of falsifying
assignments of a clause Ci . We denote by F al String(Ci ), the string (with n
symbols), that is the falsifying string for the clause Ci . As K and φ are CF’s,
the falsifying strings of their clauses allow us to denote F AL(φ) and F AL(K).
If K 6` φ ≡ F AL(φ) 6⊂ F AL(K) implies that there exists a set of assignments
S such that S ⊆ F AL(φ) and S 6⊂ F AL(K). A reviewing procedure for K ` φ
consists on taking each falsifying string representing F AL(φ) and reviewing if it
is a subset of F AL(K), e.g:S
m Vm Vk
∀i ∈ [[k]] : F AL(ϕi ) ⊆ j=1 F AL(Cj ) where K = i=1 Ci , φ = i=1 ϕi
4 An exact algorithm for K ` φ, when K and φ are CF’s
We present a method for checking K ` φ, with K and φ CF’s.
Definition 1 Given two clauses C1 and C2 , if they have at least one comple-
mentary literal, it is said that they have the independence property. Otherwise,
we say that the clauses are dependent.
Notice that falsifying strings for independent clauses have complementary
values (0 and 1) in at least one of their fixed values.
Let F = {C1 , C2 , · · · , Cm } be a CF, n = |υ(F )|. Let Ci , i ∈ [[m]] be a clause
in F and x ∈ υ(F ) \ υ(Ci ) be any variable, we have that Ci ≡ (Ci ∨ ¬x) ∧ (Ci ∨ x)
Definition 2 Given a pair of dependent clauses C1 and C2 , if Lit(C1 ) ⊆ Lit(C2 )
we say that C2 is subsumed by C1 .
If C1 subsumes C2 then F AL(C2 ) ⊆ F AL(C1 ). On the other hand, if C2
is not subsumed by C1 and they are dependents, there is a set of indices I =
{1, . . . , p} ⊆ {1, . . . , n} such that for each i ∈ I, xi ∈ C1 but xi 6∈ C2 . There
exists a reduction to transform C2 to become independent from C1 , we call this
transformation as the independent reduction between two clauses that works as
follows: let C1 and C2 be two dependent clauses. Let {x1 , x2 , . . . , xp } = Lit(C1 )\
Lit(C2 ). Thus, C1 ∧ C2 ≡ C1 ∧ (C2 ∨ ¬x1 ) ∧ (C2 ∨ x1 ). Now C1 and (C2 ∨ ¬x1 ) are
independent. Then, C1 ∧ C2 ≡ C1 ∧ (C2 ∨ ¬x1 ) ∧ (C2 ∨ x1 ∨ ¬x2 ) ∧ (C2 ∨ x1 ∨ x2 )
The first three clauses are independent. Repeating the process of making the
last clause independent with the previous ones, until xp is considered; we have
that C1 ∧ C2 can be written as:
C1 ∧(C2 ∨¬x1 )∧(C2 ∨x1 ∨¬x2 )∧. . .∧(C2 ∨x1 ∨x2 ∨...∨¬xp )∧(C2 ∨x1 ∨x2 ∨...∨xp ).
28
The last clause contains all literals of C1 , so it is subsumed by C1 , and then
C1 ∧ C2 ≡ C1 ∧ (C2 ∨ ¬x1 ) ∧ (C2 ∨ x1 ∨ ¬x2 ) ∧ . . . ∧ (C2 ∨ x1 ∨ x2 ∨ ... ∨ ¬xp ) (1)
We obtain on the right hand side of (1) an independent set of p + 1 clauses
which we denote as indep reduction(C1 , C2 ). We use the independent reduction
between two clauses C and ϕ to define:
ϕ if ϕ and C are independent
Ind(C, ϕ) = ∅ if Lit(C) \ Lit(ϕ) = ∅
indep reduction(C, ϕ) − C Otherwise
The operation Ind(C, ϕ) forms a conjunction of clauses whose falsifying as-
signments are exactly F AL(ϕ) − F AL(C).
Theorem 1 If ϕ and C are two clauses, then F AL(Ind(C, ϕ)) = F AL(ϕ) −
F AL(C)
Vm
Let K = j=1 Cj be a CF and ϕ be a clause. If we apply the Ind operator
between each Cj ∈ K and ϕ, we get as a result a set S such that S ⊆ F AL(ϕ)
and S 6⊂ F AL(K).
In order to generate a minimum set of independent clauses as a result of
Ind(K, ϕ), it is crucial to sort the clauses Cj ∈ K according to the length
|Sj | = |Lit(Cj ) \ Lit(ϕ)| in ascending order, because the number of literals in
Cj , different to the literals in ϕ, determines the number of independent clauses
to be generated.
The operator Ind applied on the clause ϕ and each one of the clauses Cj ∈ K,
allow us to build the space F AL(ϕ) − F AL(K). Thus, the following recurrence
is defined as: A1 = ϕ, Aj+1 = Ind(Cj , Aj )), j = 1, . . . , m.
In order to perform Ind(Cj , Aj ), the remaining clauses in Cl ∈ K, l = j +
1, . . . , m, those which are not reduced independently with Aj , are sorted again
in ascendent order according to the number of common literals with the literals
represented by Aj . This process can be extended to each ϕi ∈ φ, i = 1, . . . , k,
as: Ai,1 = ϕi ; Ai,j+1 = Ind(Cj , Ai,j ), j = 1, . . . , m, and i = 1, . . . , k being so
Sk
constructed clauses Ai,m+1 such that i=1 (Ai,m+1 ) = F AL(φ)−F AL(K). These
strings Ai,j , i = 1, . . . , k, j = 1, . . . , m form a matrix of strings. Notice that if
Ai,j = ∅ then Ai,l = ∅, for l = j + 1, . . . , m.
5 Incremental Satisfiability Problem
Definition 3 Let F be a 2-CF and L its set of literals. The relation →R ⊂ L×L
is defined as follows: x →R y if and only if x → y.
The transitive closure of →R , denoted by ”⇒” allows to define T (x) = {x} ∪
{y : x ⇒ y}.
Definition 4 Let F be a 2-CF, for any literal x ∈ F , it is said that T (x) is
inconsistent if x ∈ T (x) or ⊥ ∈ T (x), otherwise T (x) is said to be consistent.
29
Definition 5 A base for the set of models of a 2-CF F , denoted as S(F ), is a
partial assignment s of F which consists of the variables with a fixed truth value.
The incremental satisfiability problem (ISAT) involves checking whether sat-
isfiability is maintained when new clauses are added to an initial satisfiable
knowledge base K. ISAT is considered as a generalization of SAT since it allows
changes of the input formula over the time, and also, it can be considered as a
prototypical Dynamic Constraint Satisfaction Problem (DCSP) [9].
Different methods have been applied to solve ISAT, among them, branch and
bounds procedures as variants of the classical Davis-Putnam-Loveland (DPL)
method, denoted as IDPL methods. In IDPL procedures, when adding new
clauses, those procedures maintain the search tree generated previously for the
set of clauses K. IDPL performs substantially faster than DPL for a large set of
SAT problems [7].
As a generalization of SAT, ISAT has been considered as an NP Prob-
lem, although until now, we have not seen complexity theory studies about the
complexity-time differences between SAT and ISAT. For example, it is known
that 2-SAT is in the complexity class P, however it is not known the computa-
tional complexity of 2-ISAT. It is clear that a set of changes over a satisfiable KB
K in 2-CF could change K into a general CF, in whose case, it turns in a general
CF K 0 , K ⊂ K 0 , and where the SAT problem on K 0 is a classic NP-complete
problem.
Rather than solving related formulas separately, modern solvers attempt to
solve them incrementally since many practical applications require solving a
sequence of related SAT formulas [2, 4]. We present in this section, a study about
the threshold for the 2-ISAT problem that could be relevant to understand the
border between P and NP complexity classes.
Assuming an initial KB K, and a new CF φ to be added, both are satisfiable
CF’s, let us consider some cases where ISAT can be determined directly.
1. If K and φ are 2-CF’s then (K ∧ φ) is a 2-CF that is the input of ISAT, and
in this case, 2-ISAT is solvable in linear-time by applying the well known
algorithms for 2-SAT [6, 1]
2. If φ consists of one clause and we have the satisfiability tree of K, we only
have to review which satisfiable branches of the tree falsify φ, and this can
be done in linear time on the number of satisfiable branches of the tree.
3. For monotone formulas, ISAT keeps satisfiable formulas. If each variable
maintains an unique sign in both K and φ then (K ∧ φ) is always satisfiable.
Let us consider now that K is a 2-CF and φ is a general CF, both of them
different from the previous cases. By the results presented in Section 4, each
ϕi ∈ φ such that K ` ϕi is removed from φ, so we assume that φ = (φ − ϕi ). It
means, we will consider only the clauses in φ which decrease effectively the set
of models of K. Assume that the computation of both T (x) and Bi = F AL(ϕi )
have been computed for each x ∈ Lit(K) and each ϕi ∈ φ, respectively.
The proposal for reviewing the satisfactibility of (K ∧ φ) is based on the
following properties:
30
1. Given the partial assignments A1 , A2 which they are part of any model (if
there exists) of K. Those partial assignments may be extended in a way that
they do not falsify any ϕi ∈ φ, which is verified by Ind(Aj , ϕi ), j = 1, 2. If
it is possible, then a model for (K ∧ φ) is built.
2. Otherwise, Ind(Aj , ϕi ) = ∅, j = 1, 2 and any model of K will be part of any
falsifying assignment of φ. Thus, (K ∧ φ) is unsatisfiable.
When the operation Ind(A1 , ϕi ) is applied, a new literal x will be joined to
A1 . In fact, we consider to join T (x) instead of x. For example, if A1 = ∗01∗∗∗1∗
and ϕ1 = ∗0 ∗ 010 ∗ ∗, Ind(A1 , ϕi ) gives as a result ∗011 ∗ ∗1∗, ∗0100 ∗ 1∗ and
∗010101∗. However, in this case it means to build the following three parcial
assignments: A1 ∪T (x4 ), A1 ∪T (¬x4 )∪T (¬x5 ), and A1 ∪T (¬x4 )∪T (x5 )∪T (¬x6 ).
If any of those strings is inconsistent then such string is substituted by ∅.
Let us analyze the growth on the number of possible partial assignments of
the operation: Ind(A1 , ϕi ), ∀ϕi ∈ φ. Firstly, the number of partial assignments
for a fixed ϕi is |S| = |υ(ϕi ) − υ(A1 )|. Moreover, each partial assignment si ∈ S
is independent to the other assignments in S, because they are different in at
least one literal, and each of them hold |si+1 | ≥ |si | + 1, ∀si ∈ S.
Although Ind(A, ϕi ) is computed in linear time on the size of both strings, the
computational complexity of the revision procedure depends on the number of
strings generated by Ind(A, ϕi ), ∀ϕi ∈ φ. In some cases, Ind(A, ϕi ) may generate
empty sets. However, in the worst case, the time complexity depends on the
cardinality of the sets Li = {x1 , . . . , xp } = lit(ϕi ) − lit(A), i = 1, . . . , k.
In order to improve the time complexity of our procedure, it is convenient to
sort the clauses ϕi ∈ φ according to the cardinality of the sets Li , i = 1, . . . , k
from the smallest to the biggest and removing the clauses that are independent
with A. Once the clauses are sorted in φ with respect to their cardinalities Li ,
the operation Ind(Ind(....Ind(Ind(A, ϕ1 ), ϕ2 ), . . . , ϕk ) is applied, determining
so the succession: S0 = v(A), S1 = v(ϕ1 ) − v(A), S2 = v(ϕ2 ) − (v(ϕ1 ) ∪ v(A)),
. . ., Sk = v(ϕk ) − (v(ϕk−1 ) ∪ . . . ∪ v(ϕ1 ) ∪ v(A))
Then, the number of new clauses in the worst case is given by:
k
Y
| Ind(A, φ) |≤ | Si |=| S1 | ∗ | S2 | ∗ . . . ∗ | Sik | . (2)
i=1
It is clear that the number of strings in |Ind(A, φ)| is not bigger than the
number of assignments in SAT (K) − F AL(φ) since the falsifying assignments of
ϕi ∈ φ are removed from the partial assignment denoted by the string A. That
means |S1 | ∗ |S2 | ∗ . . . ∗ |Sk |∈ O(|SAT (K) − F AL(φ)|). From this upper bound,
we infer some tractable cases for ISAT.
Theorem 1. Let K be a 2-CF formula and φ a CF formula. The following
holds:
1. If |SAT (K)| ≤ poly(n) then ISAT is solved in polynomial time. In fact, we
can have the set of models S explicitly and each model s ∈ S can be checked:
φ[s].
31
2. If |SAT (K) − F AL(φ)| ≤ poly(n) then the number of strings in |Ind(A, φ)|
is upper bounded by |SAT (K) − F AL(φ)| ≤ poly(n).
3. When φ[T (x)] is false for all consistent T (x), Ind(K, φ) finds the unsatis-
fiability of (K ∧ φ) in polynomial time on the set of literals of K and the
number of clauses of φ. Consequently, this determines a tractable case for
the 2-ISAT problem.
Conclusions
We propose a novel method to review K ` φ when K and φ are both in Conjunc-
tive Normal Forms. This initial method is extended to consider the incremental
satisfiability (ISAT) problem. We have shown different cases where the ISAT
problem can be solved in polynomial time.
Especially, we designed an algorithm for solving the 2-ISAT problem that
allow us to determine an upper bound for the time-complexity of this problem.
Furthermore, we have established some tractable cases for the 2-ISAT problem.
References
1. Buresh-Oppenheim J., Mitchell D., Minimum 2CNF resolution refutations in poly-
nomial time, Proc. SAT’07 - 10th int. Conf. on Theory and applications of satisfia-
bility testing, (2007), pp.300-313.
2. Cabodi G., Lavagno L., Murciano M., Kondratyev A., Watanabe Y., Speeding-up
heuristic allocation, scheduling and binding with SAT-based abstraction/refinement
techniques, ACM Trans. Design Autom. Electr. Syst., 15(2), (2010).
3. Creignou N., Papini O., Pichler R., Woltran S., Belief Revision within fragments of
propositional logic, DBAI Tech. Report DBAI-TR-2012-75, (2012).
4. Eén N., S orensson K., An Extensible SAT-solver, In Enrico Giunchiglia and Ar-
mando Tacchella, editors, Selected Revised Papers of 6th International Conference
on Theory and Applicationsof Satisfiability Testing (SAT), Santa Margherita Ligure,
Italy, LNCS Vol. 2919, (2003), pp. 502-518.
5. Gallier J., Logic for Computer Science: Foundations of Automatic Theorem Proving
(chapter 9), (2003), online revision (free to download).
6. Gusfield, D., Pitt, L., A Bounded Approximation for the Minimum Cost 2-Sat Prob-
lem, Algorithmica 8, (1992), pp. 103-117.
7. Hooker J.N., Solving the incremental satisfiability problem. Journal of Logic Pro-
gramming 15, (1993), pp.177-186.
8. Khardon R., Roth D.: Reasoning with Models, Artificial Intelligence 87, No.1,
(1996), pp. 187-213.
9. Gutierrez J., Mali A., Local search for incremental Satisfiability, Proc. Int. Conf. on
AI (IC-AI’02), Las Vegas, (2002), pp. 986-991.
10. Nadel A., Ryvchin V., Strichman O., Ultimately Incremental SAT, Proc. SAT 2014,
LNCS Vol. 8561, (2014), pp. 206218.
11. Whittemore J., Joonyoung K., Sakallah K.A. SATIRE: A New Incremental Satis-
fiability Engine, In Proceedings of the 38th Design Automation Conference (DAC)-
ACM, Las Vegas - USA, (2001), pp. 542-545.
12. Wieringa S., Incremental Satisfbiability Solving and its Applications, PhD thesis,
Department of Computer Science and Engineering, Aalto University Pub., (2014).
32