constraint modelling is widely recognised as a key bottleneck in applying constraint solving to a problem of interest. the CONJURE automated constraint modelling system addresses this problem by automatically refining...
详细信息
ISBN:
(纸本)9783642406263;9783642406270
constraint modelling is widely recognised as a key bottleneck in applying constraint solving to a problem of interest. the CONJURE automated constraint modelling system addresses this problem by automatically refining constraint models from problem specifications written in the ESSENCE language. ESSENCE provides familiar mathematical concepts like sets, functions and relations nested to any depth. To date, CONJURE has been able to produce a set of alternative model kernels (i.e. without advanced features such as symmetry breaking or implied constraints) for a given specification. the first contribution of this paper is a method by which CONJURE can break symmetry in a model as it is introduced by the modelling process. this works at the problem class level, rather than just individual instances, and does not require an expensive detection step after the model has been formulated. this allows CONJURE to produce a higher quality set of models. A further limitation of CONJURE has been the lack of a mechanism to select among the models it produces. the second contribution of this paper is to present two such mechanisms, allowing effective models to be chosen automatically.
Chemical reactions consist of a rearrangement of bonds so that each atom in an educt molecule appears again in a specific position of a reaction product. In general this bijection between educt and product atoms is no...
详细信息
ISBN:
(纸本)9783642406263;9783642406270
Chemical reactions consist of a rearrangement of bonds so that each atom in an educt molecule appears again in a specific position of a reaction product. In general this bijection between educt and product atoms is not reported by chemical reaction databases, leaving the Atom Mapping Problem as an important computational task for many practical applications in computational chemistry and systems biology. Elementary chemical reactions feature a cyclic imaginary transition state (ITS) that imposes additional restrictions on the bijection between educt and product atoms that are not taken into account by previous approaches. We demonstrate that constraintprogramming is well-suited to solving the Atom Mapping Problem in this setting. the performance of our approach is evaluated for a subset of chemical reactions from the KEGG database featuring various ITS cycle layouts and reaction mechanisms.
Sophisticated compact SAT encodings exist for many types of constraints. Alternatively, for instances with many (or large) constraints, the SAT solver can also be extended with built-in propagators (the SAT Modulo the...
详细信息
ISBN:
(纸本)9783642406263;9783642406270
Sophisticated compact SAT encodings exist for many types of constraints. Alternatively, for instances with many (or large) constraints, the SAT solver can also be extended with built-in propagators (the SAT Modulo theories approach, SMT). For example, given a cardinality constraint x(1) + ... + x(n) <= k, as soon as k variables become true, such a propagator can set the remaining variables to false, generating a so-called explanation clause of the form x(1) boolean AND ... boolean AND x(k) -> (x(i)) over bar. But certain "bottle-neck" constraints end up generating an exponential number of explanations, equivalent to a naive SAT encoding, much worse than using a compact encoding with auxiliary variables from the beginning. therefore, Abio and Stuckey proposed starting off with a full SMT approach and partially encoding, on the fly, only certain "active" parts of constraints. Here we build upon their work. Equipping our solvers with some additional bookkeeping to monitor constraint activity has allowed us to shed light on the effectiveness of SMT: many constraints generate very few, or few different, explanations. We also give strong experimental evidence showing that it is typically unnecessary to consider partial encodings: it is competitive to encode the few really active constraints entirely. this makes the approach amenable to any kind of constraint, not just the ones for which partial encodings are known.
Gutierrez and Meseguer show how to enforce consistency in BnB-ADOPT(+) for distributed constraint optimization, but they consider unconditional deletions only. However, during search, more values can be pruned conditi...
详细信息
ISBN:
(纸本)9783642406263;9783642406270
Gutierrez and Meseguer show how to enforce consistency in BnB-ADOPT(+) for distributed constraint optimization, but they consider unconditional deletions only. However, during search, more values can be pruned conditionally according to variable instantiations that define subproblems. Enforcing consistency in these subproblems can cause further search space reduction. We introduce efficient methods to maintain soft arc consistencies in every subproblem during search, a non trivial task due to asynchronicity and induced overheads. Experimental results show substantial benefits on three different benchmarks.
Soft neighborhood substitutability (SNS) is a powerful technique to automatically detect and prune dominated solutions in combinatorial optimization. Recently, it has been shown in [26] that enforcing partial SNS (PSN...
详细信息
ISBN:
(纸本)9783642406263;9783642406270
Soft neighborhood substitutability (SNS) is a powerful technique to automatically detect and prune dominated solutions in combinatorial optimization. Recently, it has been shown in [26] that enforcing partial SNS (PSNSr) during search can be worthwhile in the context of Weighted constraint Satisfaction Problems (WCSP). However, for some problems, especially with large domains, PSNSr is still too costly to enforce due to its worst-case time complexity in O(ned(4)) for binary WCSP. We present a simplified dominance breaking constraint, called restricted dead-end elimination (DEEr), the worst-case time complexity of which is in O(ned(2)). Dead-end elimination was introduced in the context of computational biology as a preprocessing technique to reduce the search space [13, 14, 16, 17, 28, 30]. Our restriction involves testing only one pair of values per variable instead of all the pairs, withthe possibility to prune several values at the same time. We further improve the original dead-end elimination criterion, keeping the same time and space complexity as DEEr. Our results show that maintaining DEEr during a depth-first branch and bound (DFBB) search is often faster than maintaining PSNSr and always faster than or similar to DFBB alone.
Agricultural land allocation is a problem that exists in most provinces in Vietnam. Each household owns many disconnected parcels, which reduces agricultural development. the solution to the problem is to repartition ...
详细信息
Recent years have seen an increasing interest in the application of constraint solving techniques to test, verify and analyze software systems. A significant body of constraint-based techniques has been proposed and i...
详细信息
ISBN:
(纸本)9780769549934;9781479913244
Recent years have seen an increasing interest in the application of constraint solving techniques to test, verify and analyze software systems. A significant body of constraint-based techniques has been proposed and investigated in the context of test input generation, model-based testing, symbolic execution, static analysis, program verification, and many other areas. these techniques use or extend constraint solvers such as SAT and SMT solvers to reason about boolean, integer, real and floating-point data types, as well as complex data structures, control structures, method calls and other program features. the constraint systems that result from this work usually share many common features and are relevant to a variety of application domains. Following a first meeting held withthe principles and practice of constraintprogramming (CP) conference in 2006, and three subsequent meetings at the internationalconference on Software Testing, Verification and Validation (ICST) in 2010, 2011 and 2012, the aim of this paper is to bring together researchers and practitioners working in constraint-based software testing, verification and analysis, to investigate future developments in this research field.
We study the complexity of constraint satisfaction problems involving global constraints, i.e., special-purpose constraints provided by a solver and represented implicitly by a parametrised algorithm. Such constraints...
详细信息
Weighted Partial MaxSAT (WPMS) is an optimization variant of the Satisfiability (SAT) problem. Several combinatorial optimization problems can be translated into WPMS. In this paper we extend the state-of-the-art WPM2...
详细信息
We present a method that, given a constraint model, suggests global constraints to replace parts of it. this helps non-expert users to write higher-level models that are easier to reason about and may result in better...
详细信息
暂无评论