Timeline Planning in the J-TRE Environment - Agents and Artificial Intelligence - page 220

Fig. 2. Constraint reasoner architecture. The SAT solver controls most of the search aspects noti-
fying the listener of variable assignments.

In order to identify timeline inconsistency flaws (aka contention peaks ) inside the
check consistency routine, tokens are sorted according to their earliest start time. In
case of state variables, a set of Minimal Conflict Sets (MCSs) is identified by finding
couples of overlapping tokens. In case of reusable resources, tokens are sequentially
scrolled and collected in the current peak P until they overlap in time. Once a new
token does not overlap with tokens in P , if total requirement of tokens in P exceeds
resource capacity than P is added to the set of current peaks, all tokens that do not
overlap with the last token are removed from P andthelasttokenisaddedto P .The
collecting process continues until all tokens are scrolled. For each peak, a set of Min-
imal Conflict Sets (MCSs) is identified by sorting tokens in decreasing order of their
resource requirements and collecting MCSs in a lexicographic ordering. For each MCS,
a timeline inconsistency flaw is added to the set of current flaws. Finally, timeline in-
consistency flaws are solved simply creating a branch on the search tree for each of the
possible orderings of the tokens constituting the MCS.

4.2 SAT-CSP Based Mixed Approach: J-TRE (smt)

To represent a partial plan and reason about it, in J- TRE (smt) we have pursued the idea
of using a combination of SAT and CSP solving. As a starting point we have used
an implementation of the well known MiniSAT solver [17] modified to endow it with
capabilities for handling both preferences [18] and dynamic addition of variables and
clauses. We will then let the SAT solving procedure to guide all the search process of
both SAT and CSP problems in a Satisfiability Modulo Theory (SMT) fashion - e.g.,
[19]. Figure 2 shows the underlying structure of the constraint reasoner.
We can associate different CSP constraints to a SAT variable that “activates” them.
Each time an activation variable is assigned true value by the SAT solver, the solver
listener is notified and the correspondent constraints are dynamically added to the CSP
performing propagation. The interplay works also the other way around: if a SAT vari-
able goes from true to non assigned (the SAT solver is either backtracking or back-
jumping) then the corresponding constraints in the CSP are “deactivated” retracting
them from the dynamic CSP that again is propagated to the previous situation. It is
worth observing that the SAT solver manipulates variables according to a Last In First
Out strategy facilitating efficiency of retraction in the correspondent dynamic CSP. A
consequence of this is that we can safely reuse the J- TRE (ac) constraint reasoner to per-
form propagation of numeric variables. Furthermore, not all the SAT variables have a