Information Technology Reference
In-Depth Information
lems in automated reasoning, planning, scheduling and several areas of engineering
and design. In recent years, much effort has been spent to increase the efficiency of
both complete and incomplete algorithms for SAT. Therefore, SAT-based methods
have become an important complement to traditional specialized ones.
Real-world problems must be solved continually because real environment is
always changing by adding or removing new constraints such as the evolution of the
set of tasks to be performed in scheduling or planning applications. Problem solving
is a never ending process [21]. Thus, one may have to deal with a series of problems
that change over time where the current solution of an instance of a problem has to be
adapted to handle the next one. In the CSP community, this concept is known as the
dynamic CSP and was introduced by Dechter and Dechter [11] to maintain solutions
in dynamic constraint networks. The incremental satisfiability problem (ISAT) is a
generalisation of SAT which allows changes of a problem over time and can be
considered as a prototypical dynamic CSP [13], [15].
ISAT was introduced by Hooker [14] as the problem of checking whether
satisfiability is preserved when adding one clause at a time to an initial satisfiable set
of clauses. It was solved using an implementation of the Davis-Putnam-Loveland
procedure (DPL) [10], [17]. When adding a new clause, the procedure maintains
building the search tree generated previously for the initial satisfiable set of clauses.
Incremental DPL performs substantially faster than DPL for a large set of SAT prob-
lems [14].
A more general definition has been suggested by Kim
et al.
[16] to address
practical situations that arise in various domains such as planning and electronic
design automation (EDA). Given a set
Φ
of
m
Boolean functions in Conjunctive
{
(
)
() ()
()
()
}
Normal Form
ϕ
X
over a set of variables
X
,
Φ
=
ϕ
X
ϕ
X
=
ϕ
X
∧
ϕ
X
i
i
i
P
Si
(
)
where each function has a common prefix function
ϕ
X
and a different suffix
P
(
)
function
ϕ
X
. The problem is to determine the satisfiability of each function
Si
(
)
ϕ . Kim
et al.
[16] applied ISAT to prove the untestability of non-robust delay
fault in logic circuits. They formulated the encoding SAT instances as a sequence of
closely related SAT instances sharing a common sub-sequence. They used a DPL-like
approach to solve ISAT and showed that the results achieved using this methodology
outperform those obtained when solving each SAT instance independently.
Hoos and O'Neill [15] introduced another formulation of ISAT as the dynamic
SAT problem (DynSAT). It consists of adding or removing dynamically clauses from
a given SAT instance. The problem is to determine for a given DynSAT instance
whether it is satisfiable for each time. DynSAT can be solved simply as a set of inde-
pendent SAT, but solving them together and considering that they share a common
subset of clauses, may result in significant decrease in total run time. They presented
an initial investigation of mainly two approaches for solving DynSAT. They used
existing local search algorithms for SAT to solve the current SAT instance, while
applying either random restart or trajectory continuation before solving the next SAT
instance in the DynSAT sequence. Their empirical analysis on variants of WalkSAT
algorithm [22] indicated that trajectory continuation approach is more efficient than
X
i
Search WWH ::
Custom Search