Many real world discrete optimization problems are expressible as nested problems where we solve one optimization or satisfaction problem as a subproblem of a larger meta problem. Nested problems include many importan...
详细信息
ISBN:
(纸本)9783319104287;9783319104270
Many real world discrete optimization problems are expressible as nested problems where we solve one optimization or satisfaction problem as a subproblem of a larger meta problem. Nested problems include many important problem classes such as: stochastic constraint satisfaction/optimization, quantified constraint satisfaction/optimization and minimax problems. In this paper we define a new class of problems called nested constraint programs (NCP) which include the previously mentioned problem classes as special cases, and describe a search-based CP solver for solving NCP's. We briefly discuss how nogood learning can be used to significantly speedup such an NCP solver. We show that the new solver can be significantly faster than existing solvers for the special cases of stochastic/quantified CSP/COP's, and that it can solve new types of problems which cannot be solved with existing solvers.
Novel search space splitting techniques have recently been successfully exploited to paralleliz constraintprogramming and Mixed Integer programming solvers. We first show how universal hashing can be used to extend o...
详细信息
ISBN:
(纸本)9783319104287;9783319104270
Novel search space splitting techniques have recently been successfully exploited to paralleliz constraintprogramming and Mixed Integer programming solvers. We first show how universal hashing can be used to extend one such interesting approach to a generalized setting that goes beyond discrepancy-based search, while still retaining strong theoretical guarantees. We then explain that such static or explicit splitting approaches are not as effective in the context of parallel combinatorial search with intensive knowledge acquisition and sharing such as parallel SAT, where implicit splitting through clause sharing appears to dominate. Furthermore, we show that in a parallel setting there exists a surprising tradeoff between the well-known communication cost for knowledge sharing across multiple compute nodes and the so far neglected cost incurred by the computational load per node. We provide experimental evidence that one can successfully exploit this tradeoff and achieve reasonable speedups in parallel SAT solving beyond 16 cores.
the Patient Transportation Problem (PTP) aims to bring patients to health centers and to take them back home once the care has been delivered. All the requests are known beforehand and a schedule is built the day befo...
详细信息
ISBN:
(数字)9783319983349
ISBN:
(纸本)9783319983349;9783319983332
the Patient Transportation Problem (PTP) aims to bring patients to health centers and to take them back home once the care has been delivered. All the requests are known beforehand and a schedule is built the day before its use. It is a variant of the well-known Dial-a-Ride Problem (DARP) but it has nevertheless some characteristics that complicate the decision process. three levels of decisions are considered: selecting which requests to service, assigning vehicles to requests and routing properly the vehicles. In this paper, we propose a constraintprogramming approach to solve the Patient Transportation Problem. the model is designed to be flexible enough to accommodate new constraints and objective functions. Furthermore, we introduce a generic search strategy to maximize efficiently the number of selected requests. Our results show that the model can solve real life instances and outperforms greedy strategies typically performed by human schedulers.
constraintprogramming (CP) figures prominently in the process of functional hardware verification. the verification process is based on generating random tests according to given set of constraints. In this paper. we...
详细信息
ISBN:
(纸本)9783642406263;9783642406270
constraintprogramming (CP) figures prominently in the process of functional hardware verification. the verification process is based on generating random tests according to given set of constraints. In this paper. we introduce INTELLIGEN, a propagation based solver, and the random generator of Cadence's Specman verification tool. INTELLIGEN is designed to handle several problems beyond the mere need to find a feasible solution, including: generating random tests with a 'good' distribution over the solution space;maintaining test reproducibility through different run modes and minor code changes;and debug of the solving process by verification engineers. We discuss the advantages of CP solvers over other solving technologies (such as BDD, SAT or SMT), and how INTELLIGEN overcomes the disadvantages of CP.
M. Bezem defined an extensional semantics for positive higher-order logic programs. Recently, it was demonstrated by Rondogiannis and Symeonidou that Bezem's technique can be extended to higher-order logic program...
详细信息
M. Bezem defined an extensional semantics for positive higher-order logic programs. Recently, it was demonstrated by Rondogiannis and Symeonidou that Bezem's technique can be extended to higher-order logic programs with negation, retaining its extensional properties, provided that it is interpreted under a logic with an infinite number of truth values. Rondogiannis and Symeonidou also demonstrated that Bezem's technique, when extended under the stable model semantics, does not in general lead to extensional stable models. In this paper, we consider the problem of extending Bezem's technique under the well-founded semantics. We demonstrate that the well-founded extension fails to retain extensionality in the general case. On the positive side, we demonstrate that for stratified higher-order logic programs, extensionality is indeed achieved. We analyze the reasons of the failure of extensionality in the general case, arguing that a three-valued setting cannot distinguish between certain predicates that appear to have a different behaviour inside a program context, but which happen to be identical as three-valued relations.
the typical constraint store transmits a limited amount of information because it consists only of variable domains. We propose a richer constraint store in the form of a limited-width multivalued decision diagram (MD...
详细信息
ISBN:
(纸本)9783540749691
the typical constraint store transmits a limited amount of information because it consists only of variable domains. We propose a richer constraint store in the form of a limited-width multivalued decision diagram (MDD). It reduces to a traditional domain store when the maximum width is one but allows greater pruning of the search tree for larger widths. MDD propagation algorithms can be developed to exploit the structure of particular constraints, much as is done for domain filtering algorithms. We propose specialized propagation algorithms for alldiff and inequality constraints. Preliminary experiments show that MDD propagation solves multiple alldiff problems an order of magnitude more rapidly than traditional domain propagation. It also significantly reduces the search tree for inequality problems, but additional research is needed to reduce the computation time.
this book constitutes the proceedings of the 25thinternationalconference on principles and practice of constraintprogramming, CP 2019, held in Stamford, CT, USA, France, in September/October 2019.
ISBN:
(数字)9783030300487
ISBN:
(纸本)9783030300470
this book constitutes the proceedings of the 25thinternationalconference on principles and practice of constraintprogramming, CP 2019, held in Stamford, CT, USA, France, in September/October 2019.
Combinatorial problem solving is often carried out by reducing problems to SAT or some other finite domain constraint language. Explicitly defining reductions can be avoided by using so-called "model and solve&qu...
详细信息
ISBN:
(纸本)9783030300487
Combinatorial problem solving is often carried out by reducing problems to SAT or some other finite domain constraint language. Explicitly defining reductions can be avoided by using so-called "model and solve" systems. In this case the user writes a declarative problem specification in a constraint modelling language, such as MiniZinc. the specification implicitly defines a reduction, which is implemented by the constraint solving system. Unfortunately, reductions can destroy useful instance structure, such has having small treewidth. We show that reductions defined by certain guarded first order formulas preserve bounded treewidth. We also show such reductions can be executed automatically from problem specifications written in a guarded existential second order logic (there exists SO) by simple grounding or "flattening" algorithms. Many constraint modelling languages are essentially extensions of there exists SO, and this result applies to natural, useful, fragments of these languages.
Protein structure predictions is regarded as a highly challenging problem both for the biology and for the computational communities. Many approaches have been developed in the recent years. moving to increasingly com...
详细信息
ISBN:
(纸本)9783540859574
Protein structure predictions is regarded as a highly challenging problem both for the biology and for the computational communities. Many approaches have been developed in the recent years. moving to increasingly complex lattice models or even off-lattice models. this paper presents a Large Neighborhood Search (LNS) to find the native state for the Hydrophobic-Polar (HP) model on the Face Centered Cubic (FCC) lattice or. in other words, a self-avoiding! walk on the FCC lattice having a maximum number of H-H contacts. the algorithm starts with a tabu-search algorithm, whose solution is then improved by a combination of constraintprogramming and LNS. this hybrid algorithm improves earlier approaches in the literature over several well-known instances and demonstrates the potential of constraint-programming approaches for ab initio methods.
暂无评论