Various encodings have been proposed to convert constraint Satisfaction Problems (CSP) into Boolean Satisfiability problems (SAT). Some of them use a logical variable for each element in each domain: among these very ...
详细信息
ISBN:
(纸本)9783540749691
Various encodings have been proposed to convert constraint Satisfaction Problems (CSP) into Boolean Satisfiability problems (SAT). Some of them use a logical variable for each element in each domain: among these very successful are the direct and the support encodings. Other methods, such as the log-encoding, use a logarithmic number of logical variables to encode domains. However, they lack the propagation power of the direct and support encodings, so many SAT solvers perform poorly on log-encoded CSPs. In this paper, we propose a new encoding, called log-support, that combines the log and support encodings. It has a logarithmic number of variables, and uses support clauses to improve propagation. We also extend the encoding using a Gray code. We provide experimental results on Job-Shop scheduling and randomly-generated problems.
Adding constraints to a basic CSP model can significantly reduce search,e.g. for Golomb rulers [6]. the generation process is usually performed by hand, although some recent work has focused on automatically generatin...
ISBN:
(纸本)3540428631
Adding constraints to a basic CSP model can significantly reduce search,e.g. for Golomb rulers [6]. the generation process is usually performed by hand, although some recent work has focused on automatically generating symmetry breaking constraints [4]and (less so)on generating implied constraints [5]. We describe an approach to generating implied,symmetry breaking and specialisation constraints and apply this technique to quasigroup construction [10].
In this paper, we show how model-checking can be generalized to temporal logic constraint solving, by considering temporal logic formulae with free variables over some domain D, and by computing a validity domain for ...
详细信息
ISBN:
(纸本)9783642042430
In this paper, we show how model-checking can be generalized to temporal logic constraint solving, by considering temporal logic formulae with free variables over some domain D, and by computing a validity domain for the variables rather than a truth value for the formula. this allows us to define a continuous degree of satisfaction for a temporal logic formula ill a, given structure, opening up the field of model-checking to optimization. We illustrate this approach with reverse engineering problems coming from systems biology, and provide some performance figures oil parameter optimization problems with respect to temporal logic specifications.
constraint satisfaction and propositional satisfiability problems are often solved using backtracking search. Previous studies have shown that a technique called randomization and restarts can dramatically improve, th...
详细信息
ISBN:
(纸本)9783540749691
constraint satisfaction and propositional satisfiability problems are often solved using backtracking search. Previous studies have shown that a technique called randomization and restarts can dramatically improve, the performance of a, backtracking algorithm on some instances. We consider the commonly occurring scenario where one is to solve an ensemble of instances using a backtracking algorithm and wish to learn a good restart strategy for the ensemble. In contrast to much previous work, our focus is on universal strategies. We contribute to the theoretical understanding of universal strategies and demonstrate both analytically and empirically the pitfalls of non-universal strategies. We also propose a simple approach for learning good universal restart strategies and demonstrate the effectiveness and robustness of our approach through an extensive empirical evaluation on a real-world testbed.
We establish optimal bounds on the number of nested propagation steps in k-consistency tests. It is known that local consistency algorithms such as arc-, path- and k-consistency are not efficiently parallelizable. the...
详细信息
ISBN:
(纸本)9783319104287;9783319104270
We establish optimal bounds on the number of nested propagation steps in k-consistency tests. It is known that local consistency algorithms such as arc-, path- and k-consistency are not efficiently parallelizable. their inherent sequential nature is caused by long chains of nested propagation steps, which cannot be executed in parallel. this motivates the question "What is the minimum number of nested propagation steps that have to be performed by k-consistency algorithms on (binary) constraint networks with n variables and domain size d?" It was known before that 2-consistency requires Omega(nd) and 3-consistency requires Omega(n(2)) sequential propagation steps. We answer the question exhaustively for every k >= 2: there are binary constraint networks where any k-consistency procedure has to perform Omega( n(k-1)d(k-1)) nested propagation steps before local inconsistencies were detected. this bound is tight, because the overall number of propagation steps performed by k-consistency is at most n(k-1)d(k-1).
Multi-objective optimization is concerned with problems involving multiple Measures of performance which should be optimized simultaneously. In this paper, we extend AND/OR Branch-and-Bound (AOBB). a well known search...
详细信息
ISBN:
(纸本)9783642042430
Multi-objective optimization is concerned with problems involving multiple Measures of performance which should be optimized simultaneously. In this paper, we extend AND/OR Branch-and-Bound (AOBB). a well known search algorithm, from mono-objective to multi-objective optimization. the new algorithm MO-AOBB exploits efficiently the problem structure by traversing an AND/OR search tree and uses static and dynamic mini-bucket heuristics to guide the search. We show that MO-AOBB improves dramatically over the traditional OR search approach, on various benchmarks for multi-objective optimization.
In this paper, we present a domain specific optimization framework based on a concurrent model-based approach for handling the complete problem of mapping a DSP application on a parallel architecture. the implementati...
详细信息
Filtering constraint networks to reduce search space is one of the main cornerstones of constraintprogramming and among them (Generalized) Arc Consistency has been the most fundamental. While stronger consistencies a...
详细信息
ISBN:
(纸本)9783319104287;9783319104270
Filtering constraint networks to reduce search space is one of the main cornerstones of constraintprogramming and among them (Generalized) Arc Consistency has been the most fundamental. While stronger consistencies are also the subject of considerable attention, none matches GAC's and for this reason it continues to advance at a steady pace and has become the popular choice of consistency for filtering algorithms. In this paper, we build on the success of GAC by proposing a way to transform a constraint network into another such that enforcing GAC on the latter is equivalent to enforcing a stronger consistency on the former. the key idea is to factor out commonly shared variables from constraints' scopes, form new variables, then re-attach them back to the constraints where they come from. Experiments show that this method is inexpensive and outperforms specialized algorithms and other techniques when it comes to full pair-wise consistency (FPWC).
the SEQUENCE constraint is useful in modelling car sequencing, rostering, scheduling and related problems. We introduce half a dozen new encodings of the SEQUENCE constraint, some of which do not hinder propagation. W...
详细信息
ISBN:
(纸本)9783540749691
the SEQUENCE constraint is useful in modelling car sequencing, rostering, scheduling and related problems. We introduce half a dozen new encodings of the SEQUENCE constraint, some of which do not hinder propagation. We prove that, down a branch of a search tree, domain consistency can be enforced on the SEQUENCE constraint in just O(n(2) log n) time. this improves upon the previous bound of O(n(3)) for each call down the tree. We also consider a generalization of the SEQUENCE constraint - the Multiple SEQUENCE constraint. Our experiments suggest that, on very large and tight problems, domain consistency algorithms are best. However, on smaller or looser problems, much simpler encodings are better, even though these encodings hinder propagation. When there are multiple SEQUENCE constraints, a more expensive propagator shows promise.
暂无评论