Information Technology Reference
In-Depth Information
correspondent constraint. Those that are free from this connection can be used to model
the causality in the planning problem or to add further constraints like those deriving
from a disjunctive qualitative temporal network.
When the CSP propagation fails we have a
theory conflict
. In this case, the SAT
solver is consistent but the correspondent theory represented by the CSP (the set of
active constraints on CSP variables) is not. Similarly to the
lazy approach
in SMT,
we add the information on the theory failure in the SAT representation by adding the
negation of the conjunction of active constraints hence avoiding that the SAT solver
reselect the same state later on. It is worth saying that the negation of a conjunction of
literals can be transformed in a disjunction of negation by using De Morgan laws. In
the SAT reasoner, this new clause is considered as a new “conflict clause” from which a
no-good is generated and added the the representation after performing a backjumping
step.
Giving preference for false values to each SAT variable allows us to minimize the
number of active elements in the partial plan and, consequently, the number of active
CSP constraints. Our extended CSP solver can now handle both disjunctive CSPs and
domain causality through the SAT problem. If the SAT problem would become unsat-
isfiable then our extended CSP problem would have no solutions and the current search
space node will become inconsistent.
Using the Hybrid Engine for Timeline Based Planning.
So far, the planner collects
flaws, selects one of them according to a selection strategy and solves it through the
execution of DDL code which, in turns, adds new constraints among tokens and/or new
tokens into the partial plan.
Having our own implementation of the SMT solver we can easily add further con-
straints in order to simplify the search procedure by pruning some search space. For
example, we have modelled a disjunctive qualitative temporal network through SMT
that would avoid qualitative inconsistencies. If we use
to denote the boolean
variable which encodes the
x ≤ y
constraint, we can represent a disjunctive qual-
itative temporal network through the following constraints. For each triple of time-
points
t
0
,
t
1
and
t
2
, we add the following clauses representing the transitive closure:
(
x ≤ y
¬
t
0
≤
t
1
∨¬
t
1
≤
t
2
∨
t
0
≤
t
2
)
,
(
¬
t
1
≤
t
2
∨¬
t
2
≤
t
0
∨
t
1
≤
t
0
)
and
(
¬
t
0
≤
t
2
∨¬
t
2
≤
t
1
∨
t
0
≤
t
1
)
.
Flaw Management in J-TRE
(smt)
.
Each time a child is added to a node of the search
space, the SMT of the parent node is copied into the child nodes together with all no-
goods that have been learnt in previous search phases.
For what concerns goal flaws, we have two possible resolution strategies:
compat-
ibility application
and
merging
. The flaw solver will generate a branch on the search
space with two nodes representing the compatibility application on the first node and
all possible merges on the second. Compatibility application is managed simply execut-
ing DDL code representing the compatibility on the proper node. Further state variable
tokens and disjunctions can be added leading to new flaws on the current search space
node.
