Information Technology Reference
In-Depth Information
Exploiting our multi-equals constraint we assign a SAT variable u 0 ,..., u i ,...,
u n , for each of the n tokens on the same timeline having the same proposition, to a
multi-equals constraint that will ensure equality between goal token's arguments and
target token's arguments. Whenever a variable u i becomes true, the token is forced to
unify with the correspondent token. The flaw solver will then add the resolution clause
( u 0
u n ) to the SMT solver. By adding further clauses to the SMT solver we
can link the merging of a token to the qualitative temporal network reasoning forcing
the equality of the temporal points of the tokens. Assuming, for example, that the SAT
variable u 0 represents the unification between tokens t 0 and t 1 , we add the following
clauses to the SMT: (
...
¬
u 0
t 0 .s
t 1 .s
) , (
¬
u 0
t 1 .s
t 0 .s
) , (
¬
u 0
t 0 .e
t 1 .e
)
and (
) . Because unification does not lead to further compatibilities
application, we always add preference for the unification case.
While the MCS extraction procedure is similar to the J- TRE (ac) case, we do not
enqueue MCSs as common flaws because we can exploit SMT solver to directly solve
them. We simply add a SAT clause asserting that the current state implies the disjunction
of possible orderings of tokens. Let us consider, for example, the case in which we have
an MCS composed by two tokens t 0
¬
u 0
t 1 .e
t 0 .e
and t 1 . The clause that will be added is (
¬
S
) where the symbol S is used to indicate the conjunction
of all activation variables that in current state are active 2 . The clause (
t 0 .e
t 1 .s
t 1 .e
t 0 .s
¬
t 0 .e
t 1 .s
¬
t 1 .e
t 0 .s
) can also be added to improve performances.
4.3
Quantitative Time through Arc Consistency: J-TRE (stp)
Although really simple, J- TRE (ac) treats temporal points like standard numerical vari-
ables in a Single Source Shortest Path manner similar to [8]. The resulting temporal
network doesn't allow almost any exploitation of information taken from constraint
reasoning for search space pruning purposes resulting in an early search space explo-
sion. With the intent to add more information in the constraint reasoning that can be
used to prune search space, we have introduced J- TRE (smt) that maintains a disjunctive
qualitative temporal network through a SAT encoding. We have seen that the J- TRE
architecture is flexible enough to handle these two quite different technologies. A third
attempt can be the use of a Simple Temporal Network [16] from which we can gain
information that could possibly allow us to improve both flaw choosing and flaw reso-
lution procedures.
In order to obtain an efficient All Pair Shortest Path behavior (namely the Simple
Temporal Network we are looking for) without changing much from the J- TRE (ac)
system, in J- TRE (stp) we have chosen to treat temporal points in a different way from
standard numerical variables. For each couple of variables x i and x j we add an addi-
tional variable d ij and a further constraint d ij = x j
x i . The idea here is to use the
d ij to represent the distance between variables x i and x j . We could use this informa-
tion to prune search space when solving scheduling flaws and/or merging in goal flows.
Unfortunately, this addition is not enough for our simple AC-3 algorithm and distance
2
Exploiting De Morgan laws, the symbol ¬S is used to indicate the disjunction of negations of
the literals of S . Being a disjunction of literals, with a little extension of terminology, we can
use ¬S inside clauses
 
Search WWH ::




Custom Search