scholarly journals Fast Set Bounds Propagation Using a BDD-SAT Hybrid

2010 ◽  
Vol 38 ◽  
pp. 307-338 ◽  
Author(s):  
G. Gange ◽  
P. J. Stuckey ◽  
V. Lagoon
Keyword(s):  
Constraint Satisfaction ◽  
Binary Decision Diagram ◽  
Constraint Satisfaction Problems ◽  
Basic Algorithm ◽  
Learning Abilities ◽  
Binary Decision ◽  
Constraint Solver ◽  
Powerful Approach ◽  
Sat Solver

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.

Reducing the Complexity of Modeling Large Software Systems

2009 ◽  
pp. 3399-3429
Author(s):  
Jules White ◽  
Douglas C. Schmidt ◽  
Andrey Nechypurenko ◽  
Egon Wuchner
Keyword(s):  
Constraint Satisfaction ◽  
Constraint Satisfaction Problems ◽  
Correct Solution ◽  
Software Systems ◽  
Domain Expert ◽  
Modeling Tool ◽  
Constraint Solver ◽  
Model Driven ◽  
Model Driven Approach ◽  
Domain Constraints

Model-driven development is one approach to combating the complexity of designing software intensive systems. A model-driven approach allows designers to use domain notations to specify solutions and domain constraints to ensure that the proposed solutions meet the required objectives. Many domains, however, require models that are either so large or intricately constrained that it is extremely difficult to manually specify a correct solution. This chapter presents an approach to provide that leverages a constraint solver to provide modeling guidance to a domain expert. The chapter presents both a practical framework for transforming models into constraint satisfaction problems and shows how the Command Pattern can be used to integrate a constraint solver into a modeling tool.

scholarly journals Solving Set Constraint Satisfaction Problems using ROBDDs

2005 ◽  
Vol 24 ◽  
pp. 109-156 ◽  
Author(s):  
P. J. Hawkins ◽  
V. Lagoon ◽  
P. J. Stuckey
Keyword(s):  
Constraint Satisfaction ◽  
Constraint Satisfaction Problems ◽  
Set Domain ◽  
Ordered Binary Decision Diagrams ◽  
Binary Decision ◽  
New Approach ◽  
Performance Improvements ◽  
Set Constraints ◽  
Finite Set ◽  
Standard Set

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.

scholarly journals Compiling CSPs: A Complexity Map of (Non-Deterministic) Multivalued Decision Diagrams

2014 ◽  
Vol 23 (04) ◽  
pp. 1460015 ◽  
Author(s):  
Jérôme Amilhastre ◽  
Hélène Fargier ◽  
Alexandre Niveau ◽  
Cédric Pralet
Keyword(s):  
Polynomial Time ◽  
Constraint Satisfaction ◽  
Binary Decision Diagrams ◽  
Constraint Satisfaction Problems ◽  
Decision Diagrams ◽  
Np Hard ◽  
Ordered Binary Decision Diagrams ◽  
Binary Decision

Constraint Satisfaction Problems (CSPs) offer a powerful framework for representing a great variety of problems. The difficulty is that most of the requests associated with CSPs are NP-hard. When these requests have to be addressed online, Multivalued Decision Diagrams (MDDs) have been proposed as a way to compile CSPs. In the present paper, we draw a compilation map of MDDs, in the spirit of the NNF compilation map, analyzing MDDs according to their succinctness and to their tractable transformations and queries. Deterministic ordered MDDs are a generalization of ordered binary decision diagrams to non-Boolean domains: unsurprisingly, they have similar capabilities. More interestingly, our study puts forward the interest of non-deterministic ordered MDDs: when restricted to Boolean domains, they capture OBDDs and DNFs as proper subsets and have performances close to those of DNNFs. The comparison to classical, deterministic MDDs shows that relaxing the determinism requirement leads to an increase in succinctness and allows more transformations to be satisfied in polynomial time (typically, the disjunctive ones). Experiments on random problems confirm the gain in succinctness.

A SPACE-EFFICIENT BACKTRACK-FREE REPRESENTATION FOR CONSTRAINT SATISFACTION PROBLEMS

2008 ◽  
Vol 17 (04) ◽  
pp. 703-730 ◽  
Author(s):  
J. CHRISTOPHER BECK ◽  
TOM CARCHRAE ◽  
EUGENE C. FREUDER ◽  
GEORG RINGWELSKI
Keyword(s):  
Constraint Satisfaction ◽  
Constraint Satisfaction Problem ◽  
Significant Proportion ◽  
Constraint Satisfaction Problems ◽  
Basic Algorithm ◽  
High Coverage ◽  
Trade Off ◽  
Free Representation ◽  
Pruning Heuristics ◽  
First Time

In this paper we present a radical approach to obtaining a backtrack-free representation for a constraint satisfaction problem: remove values that lead to dead-ends. This technique does not require additional space but has the drawback of removing solutions. We investigate a number of variations on the basic algorithm including the use of seed solutions, consistency techniques, and a variety of pruning heuristics. Our experimental results indicate that a significant proportion of the solutions to the original problem can be retained especially when an optimization algorithm that specifically searches for such “good” backtrack-free representations is employed. Further extensions increase solution retention by searching for high-coverage backtrack-free representations, by removing tuples rather than values, and by combining multiple backtrack-free representations. Our approach elucidates, for the first time, a three-way trade-off between space complexity, potential backtracks, and solution loss and enables algorithms that can actively reason about the trade-off between space, backtracks, and solution loss.

scholarly journals Search Strategies as Synchronous Processes (Extended Abstract)

2017 ◽  
Author(s):  
Pierre Talbot
Keyword(s):  
Constraint Satisfaction ◽  
Search Strategy ◽  
State Of The Art ◽  
Search Strategies ◽  
Constraint Satisfaction Problems ◽  
Constraint Solver ◽  
Process Calculi

Solving constraint satisfaction problems (CSP) efficiently depends on the solver configuration and the search strategy. However, it is difficult to customize the constraint solvers because they are not modular enough, and it is hard to create new search strategies by composition. To solve these problems, we propose spacetime programming, a paradigm based on lattices and synchronous process calculi that views search strategies as processes working collaboratively towards the resolution of a CSP. We implement the compiler of the language and use it to replace the search module of Choco, a state of the art constraint solver, with an efficient spacetime program that offers better modularity and compositionality of search strategies.

Reducing the Complexity of Modeling Large Software Systems

2009 ◽  
pp. 372-400
Author(s):  
Jules White ◽  
Douglas C. Schmidt ◽  
Andrey Nechypurenko ◽  
Egon Wuchner
Keyword(s):  
Constraint Satisfaction ◽  
Constraint Satisfaction Problems ◽  
Correct Solution ◽  
Software Systems ◽  
Domain Expert ◽  
Modeling Tool ◽  
Constraint Solver ◽  
Model Driven ◽  
Model Driven Approach ◽  
Domain Constraints

Model-driven development is one approach to combating the complexity of designing software intensive systems. A model-driven approach allows designers to use domain notations to specify solutions and domain constraints to ensure that the proposed solutions meet the required objectives. Many domains, however, require models that are either so large or intricately constrained that it is extremely difficult to manually specify a correct solution. This chapter presents an approach to provide that leverages a constraint solver to provide modeling guidance to a domain expert. The chapter presents both a practical framework for transforming models into constraint satisfaction problems and shows how the Command Pattern can be used to integrate a constraint solver into a modeling tool.

scholarly journals Intelligent search strategies based on adaptive Constraint Handling Rules

2005 ◽  
Vol 5 (4-5) ◽  
pp. 567-594 ◽  
Author(s):  
ARMIN WOLF
Keyword(s):  
Constraint Satisfaction ◽  
Search Strategies ◽  
Constraint Satisfaction Problems ◽  
Constraint Handling ◽  
Search Process ◽  
Constraint Solver ◽  
Intelligent Search ◽  
Constraint Processing ◽  
Made In

The most advanced implementation of adaptive constraint processing with Constraint Handling Rules (CHR) allows the application of intelligent search strategies to solve Constraint Satisfaction Problems (CSP). This presentation compares an improved version of conflict-directed backjumping and two variants of dynamic backtracking with respect to chronological backtracking on some of the AIM instances which are a benchmark set of random 3-SAT problems. A CHR implementation of a Boolean constraint solver combined with these different search strategies in Java is thus being compared with a CHR implementation of the same Boolean constraint solver combined with chronological backtracking in SICStus Prolog. This comparison shows that the addition of “intelligence” to the search process may reduce the number of search steps dramatically. Furthermore, the runtime of their Java implementations is in most cases faster than the implementations of chronological backtracking. More specifically, conflict-directed backjumping is even faster than the SICStus Prolog implementation of chronological backtracking, although our Java implementation of CHR lacks the optimisations made in the SICStus Prolog system.

scholarly journals Exploiting Single-Cycle Symmetries in Continuous Constraint Problems

2009 ◽  
Vol 34 ◽  
pp. 499-520 ◽  
Author(s):  
V. Ruiz de Angulo ◽  
C. Torras
Keyword(s):  
Constraint Satisfaction ◽  
Simple Algorithm ◽  
Constraint Satisfaction Problems ◽  
Single Cycle ◽  
Constraint Solver ◽  
Dimensional Cube ◽  
Very High

Symmetries in discrete constraint satisfaction problems have been explored and exploited in the last years, but symmetries in continuous constraint problems have not received the same attention. Here we focus on permutations of the variables consisting of one single cycle. We propose a procedure that takes advantage of these symmetries by interacting with a continuous constraint solver without interfering with it. A key concept in this procedure are the classes of symmetric boxes formed by bisecting a n-dimensional cube at the same point in all dimensions at the same time. We analyze these classes and quantify them as a function of the cube dimensionality. Moreover, we propose a simple algorithm to generate the representatives of all these classes for any number of variables at very high rates. A problem example from the chemical field and the cyclic n-roots problem are used to show the performance of the approach in practice.

Sign in / Sign up

Export Citation Format

Share Document