Computing and Information Systems - Research Publications
Permanent URI for this collection
Search Results
1 - 7 of 7
-
ItemTelecommunications feature subscription as a partial order constraint problem(Springer Verlag, 2008)
-
ItemSolving partial order constraints for LPO termination(SPRINGER-VERLAG BERLIN, 2006)This paper introduces a new kind of propositional encoding for reasoning about partial orders. The symbols in an unspecified partial order are viewed as variables which take integer values and are interpreted as indices in the order. For a partial order statement on n symbols each index is represented in log2 n propositional variables and partial order constraints between symbols are modeled on the bit representations. We illustrate the application of our approach to determine LPO termination for term rewrite systems. Experimental results are unequivocal, indicating orders of magnitude speedups in comparison with current implementations for LPO termination. The proposed encoding is general and relevant to other applications which involve propositional reasoning about partial orders.
-
ItemSize-change termination analysis in κ-bits(SPRINGER-VERLAG BERLIN, 2006)
-
ItemTesting for termination with monotonicity constraints(SPRINGER-VERLAG BERLIN, 2005)
-
Item
-
ItemFast Set Bounds Propagation Using a BDD-SAT Hybrid(AI ACCESS FOUNDATION, 2010)Binary Decision Diagram (BDD) based set bounds propagation is a powerful approach to solving set-constraint satisfaction problems. However, prior BDD based techniques in- cur the significant overhead of constructing and manipulating graphs during search. We present a set-constraint solver which combines BDD-based set-bounds propagators with the learning abilities of a modern SAT solver. Together with a number of improvements beyond the basic algorithm, this solver is highly competitive with existing propagation based set constraint solvers.
-
ItemSolving set constraint satisfaction problems using ROBDDS(AI ACCESS FOUNDATION, 2005)In this paper we present a new approach to modeling finite set domain constraint problems using Reduced Ordered Binary Decision Diagrams (ROBDDs). We show that it is possible to construct an efficient set domain propagator which compactly represents many set domains and set constraints using ROBDDs. We demonstrate that the ROBDD-based approach provides unprecedented flexibility in modeling constraint satisfaction problems, leading to performance improvements. We also show that the ROBDD-based modeling approach can be extended to the modeling of integer and multiset constraint problems in a straightforward manner. Since domain propagation is not always practical, we also show how to incorporate less strict consistency notions into the ROBDD framework, such as set bounds, cardinality bounds and lexicographic bounds consistency. Finally, we present experimental results that demonstrate the ROBDD-based solver performs better than various more conventional constraint solvers on several standard set constraint problems.