isl/doc/implementation.tex

170 This method is not based on Feautrier's algorithm, but on rational
180 the constraints on the parameters, known as the context tableau.
187 as that used by its incremental LP solver based on the \emph{primal}
189 on that of {\tt Simplify} \shortcite{Detlefs2005simplify}, which, in turn,
195 Given some affine constraints on the variables,
203 on a tableau exchanges a column and a row variable and is called a pivot.
251 is the unit vector $e_i$.  If, on the other hand, it is a row variable,
255 may depend on the parameters.  Each time the constant term of a constraint row
332 implicit conditions on the big parameter through conditions on such
354 are made on the sign of the unknowns.  Instead, the sign of the unknowns
357 does explicitly add non-negativity constraints on the unknowns unless
361 {\tt isl} makes the same divisibility assumption on the big parameter
374 do not perform very well on problems that are (non-obviously) empty,
376 In {\tt isl}, we therefore first perform a feasibility check on
393 {\tt isl} performs such simplifications on all sets and relations.
395 on the input.
454 These constant terms will be non-negative on different parts
466 on $u$ and therefore extends a solution to the new system.
488 It is also possible to perform a similar compression on the unknowns,
500 based on a parametric constant term in the main tableau with indeterminate
504 on the path leading to the leaf.
516 to avoid this overhead in future.  That is, we are planning on introducing
518 representations and on allowing the output of {\tt isl\_pip} to optionally
544 on the sign of an affine expression over the elements of the context.
566 evaluates to a positive number on some of these points and to a negative
567 number on some others, then no feasibility test needs to be performed.
572 one or two feasibility tests need to be performed depending on the result
585 \subsubsection{Choice of Constant Term on which to Split}
591 to split on first.  {\tt PipLib} uses a heuristic based on the (absolute)
598 rows as possible.  The intuition behind this heuristic is that on the
600 while on the negative side, we need to perform a pivot, which may
601 affect any number of rows meaning that the effect on the signs
610 or at least very similar to those taken on the original context, i.e.,
612 the dual simplex method incrementally on the context and backtrack
636 worked on a parametric integer programming implementation
639 in the context tableau.  Based on this report,
655 A restriction of the algorithm is that it only works on bounded sets.
671 integer feasibility checks on that part of the context outside
685 on some more difficult instances to those of other tools,
686 run on an Intel Xeon W3520 @ 2.66GHz.
718 sometimes report the problem to be too complex (TC), while on some other
723 minutes on the first problem.  The gbr version introduces some
724 overhead on some of the easier problems, but is overall the clear winner.
757 Manual experiments on small instances of the problems of
1356 cases depending on whether $R$ is {\em cyclic}, where $R$ is defined
1376 If, on the other hand, $R$ is cyclic, then we have to resort
1396 Note that the exactness on the power is always sound, even
1404 In the implementation we currently perform this test on $P'$ instead of $K'$.
1454 The graph on which Tarjan's algorithm is applied is constructed on-the-fly.
1457 The exactness check is performed on each component separately.
1460 is skipped on the components that still need to be handled.
1467 on the condition $R_i \circ R_j = \emptyset$, then there is no problem,
1468 as this condition will still hold on the computed approximations
1474 Note that testing for transitive closedness on the result may
1578 Consider the relation on the right of \shortciteN[Figure~2]{Beletska2009},
1687 Otherwise, we apply Floyd-Warshall on the graph with as vertices
1739 \caption{The relation (solid arrows) on the right of Figure~1 of
1744 Consider the relation on the right of Figure~1 of
1784 on $R_{01}$ and $R_{10}$.  However, $R_{00}$ is updated to
1819 say on domain $D$.  We will use the notation
1961 that is based on their ideas.
1980 lower and upper bounds on the difference set $\Delta \, R$.
1997 use the above algorithm as a substep on the disjuncts in the relation.