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.

Set Based Hierarchical Design: A Constraint Satisfaction Approach

1995 ◽  
Author(s):  
Christian Bliek
Keyword(s):  
Constraint Satisfaction ◽  
Design Automation ◽  
Constraint Satisfaction Problems ◽  
Combinatorial Complexity ◽  
Hierarchical Decomposition ◽  
Hierarchical Design ◽  
Decomposition Techniques ◽  
New Approach ◽  
Candidate Solution ◽  
Literature Reviews

Abstract Many are the literature reviews where constraint satisfaction is rejected as a candidate solution for design automation. Some point to the combinatorial complexity associated with the solution of large constraint satisfaction problems, others claim it is inadequate to handle the uncertainty prominent in engineering design. In this paper we present a new approach in which hierarchical decomposition techniques exploit sensitivity to reduce combinatorial complexity and uncertainty is modeled using conservative enclosures of sets of possible solutions.

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.

Searching Feasible Design Space by Solving Quantified Constraint Satisfaction Problems

2013 ◽  
Vol 136 (3) ◽  
Author(s):  
Jie Hu ◽  
Masoumeh Aminzadeh ◽  
Yan Wang
Keyword(s):  
Monte Carlo ◽  
Constraint Satisfaction ◽  
Design Space ◽  
Constraint Satisfaction Problem ◽  
Constraint Satisfaction Problems ◽  
Design Solution ◽  
New Approach ◽  
Solution Sets ◽  
Branch And Prune Algorithm ◽  
Branch And Prune

In complex systems design, multidisciplinary constraints are imposed by stakeholders. Engineers need to search feasible design space for a given problem before searching for the optimum design solution. Searching feasible design space can be modeled as a constraint satisfaction problem (CSP). By introducing logical quantifiers, CSP is extended to quantified constraint satisfaction problem (QCSP) so that more semantics and design intent can be captured. This paper presents a new approach to formulate searching design problems as QCSPs in a continuous design space based on generalized interval, and to numerically solve them for feasible solution sets, where the lower and upper bounds of design variables are specified. The approach includes two major components. One is a semantic analysis which evaluates the logic relationship of variables in generalized interval constraints based on Kaucher arithmetic, and the other is a branch-and-prune algorithm that takes advantage of the logic interpretation. The new approach is generic and can be applied to the case when variables occur multiple times, which is not available in other QCSP solving methods. A hybrid stratified Monte Carlo method that combines interval arithmetic with Monte Carlo sampling is also developed to verify the correctness of the QCSP solution sets obtained by the branch-and-prune algorithm.

scholarly journals Tractable Set Constraints

2012 ◽  
Vol 45 ◽  
pp. 731-759 ◽  
Author(s):  
M. Bodirsky ◽  
M. Hils
Keyword(s):  
Artificial Intelligence ◽  
Constraint Satisfaction ◽  
Constraint Satisfaction Problem ◽  
Description Logics ◽  
Constraint Satisfaction Problems ◽  
Algebraic Characterization ◽  
Crucial Importance ◽  
Hard Constraint ◽  
Set Constraints ◽  
Constraint Language

Many fundamental problems in artificial intelligence, knowledge representation, and verification involve reasoning about sets and relations between sets and can be modeled as set constraint satisfaction problems (set CSPs). Such problems are frequently intractable, but there are several important set CSPs that are known to be polynomial-time tractable. We introduce a large class of set CSPs that can be solved in quadratic time. Our class, which we call EI, contains all previously known tractable set CSPs, but also some new ones that are of crucial importance for example in description logics. The class of EI set constraints has an elegant universal-algebraic characterization, which we use to show that every set constraint language that properly contains all EI set constraints already has a finite sublanguage with an NP-hard constraint satisfaction problem.

Sign in / Sign up

Export Citation Format

Share Document