Solutions to valid Quantified constraint Satisfaction Problems (QCSPs) are called winning strategies and represent possible ways in which the existential player can react to the moves of the universal one to "win...
详细信息
ISBN:
(纸本)9783540859574
Solutions to valid Quantified constraint Satisfaction Problems (QCSPs) are called winning strategies and represent possible ways in which the existential player can react to the moves of the universal one to "win the game". However, different winning strategies are not necessarily equivalent: some may be preferred to others. We define Quantified constraint Optimization Problems (QCOP) as a framework which allows both to formally express preferences over QCSP strategies, and to solve the related optimization problem. We present examples and some experimental results. We also discuss flow this framework relates to other formalisms for hierarchical decision modeling known as von Stackelberg games and bilevel (and multilevel) programming.
We introduce a new method for solving systems of linear inequalities over the rationals-the conflict resolution method. the method successively refines an initial assignment withthe help of newly derived constraints ...
详细信息
ISBN:
(纸本)9783642042430
We introduce a new method for solving systems of linear inequalities over the rationals-the conflict resolution method. the method successively refines an initial assignment withthe help of newly derived constraints until either the assignment becomes a solution of the system or a trivially unsatisfiable constraint is derived. We show that this method is correct and terminating. Our experimental results show that conflict resolution outperforms the Fourier-Motzkin method and the Chernikov algorithm, in some cases by orders of magnitude.
Conflict-Driven Clause-Learning (CDCL) SAT solvers can automatically solve very large real-world problems. To go beyond, and in particular in order to solve and optimize problems involving linear arithmetic constraint...
详细信息
ISBN:
(纸本)9783319104287;9783319104270
Conflict-Driven Clause-Learning (CDCL) SAT solvers can automatically solve very large real-world problems. To go beyond, and in particular in order to solve and optimize problems involving linear arithmetic constraints, here we introduce IntSat, a generalization of CDCL to Integer Linear programming (ILP). Our simple 1400-line C++ prototype IntSat implementation already shows some competitiveness with commercial solvers such as CPLEX or Gurobi. Here we describe this new IntSat ILP solving method, show how it can be implemented efficiently, and discuss a large list of possible enhancements and extensions.
We present a new and more efficient heuristic by restricting lookahead saturation (LAS) with NVO (neighbourhood variable ordering) and DEW (dynamic equality weighting). We report on the integration of this heuristic i...
详细信息
ISBN:
(纸本)3540292381
We present a new and more efficient heuristic by restricting lookahead saturation (LAS) with NVO (neighbourhood variable ordering) and DEW (dynamic equality weighting). We report on the integration of this heuristic in Satz, a high-performance SAT solver, showing empirically that it significantly improves the performance on an extensive range of benchmark problems that exhibit hard structure.
Block modeling has been used extensively in many domains including social science, spatial temporal data analysis and even medical imaging. Original formulations of the problem modeled the problem as a mixed integer p...
详细信息
ISBN:
(纸本)9783030300487
Block modeling has been used extensively in many domains including social science, spatial temporal data analysis and even medical imaging. Original formulations of the problem modeled the problem as a mixed integer programming problem, but were not scalable. Subsequent work relaxed the discrete optimization requirement, and showed that adding constraints is not straightforward in existing approaches. In this work, we present a new approach based on constraintprogramming, allowing discrete optimization of block modeling in a manner that is not only scalable, but also allows the easy incorporation of constraints. We introduce a new constraint filtering algorithm that outperforms earlier approaches, in both constrained and unconstrained settings. We show its use in the analysis of real datasets.
Many cooperative systems merge a linear constraint solver and a domain reduction solver over finite domains or intervals. the latter handles a high level formulation of the problem and passes domain variable informati...
详细信息
ISBN:
(纸本)3540666265
Many cooperative systems merge a linear constraint solver and a domain reduction solver over finite domains or intervals. the latter handles a high level formulation of the problem and passes domain variable information. the former handles a linear formulation of the problem and computes a relaxed optimal solution. this paper proposes an extension to this framework called tight cooperation where the linear formulation of a high level constraint is restated in a way, as domains are reduced. this approach is illustrated on piecewise linear optimization. Experimental results are given. these show that tight cooperation can give better results than classical. cooperation and mixed-integer programming techniques.
this work shows the implementation of ntcc-lman [1], a framework for ntcc [2], a non deterministic timed concurrent constraint process calculus. this calculus provides a formal model in which concepts proper to roboti...
ISBN:
(纸本)3540232419
this work shows the implementation of ntcc-lman [1], a framework for ntcc [2], a non deterministic timed concurrent constraint process calculus. this calculus provides a formal model in which concepts proper to robotic control can be conveniently represented. the ntcc-lman framework includes a ntcc based kernel language, a compiler, a constraint system, a formal abstract machine based on ntcc reduction rules and a virtual machine. We show how the framework can be used to program typical robotic tasks to control LEGO robots in real time using timed ccp technology. To our knowledge, this is the first timed ccp framework for programming robotic devices.
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.
the paper introduces the MST(G, T, W) constraint, which is specified on two graph variables G and T and a vector W of scalar variables. the constraint is satisfied if T is a minimum spanning tree of G, where the edge ...
详细信息
ISBN:
(纸本)3540462678
the paper introduces the MST(G, T, W) constraint, which is specified on two graph variables G and T and a vector W of scalar variables. the constraint is satisfied if T is a minimum spanning tree of G, where the edge weights are specified by the entries of W. We develop algorithms that filter the domains of all variables to bound consistency.
the weighted constraint satisfaction problem (WCSP) occurs in the crux of many real-world applications of operations research, artificial intelligence, bioinformatics, etc. Despite its importance as a combinatorial su...
详细信息
ISBN:
(纸本)9783319661582;9783319661575
the weighted constraint satisfaction problem (WCSP) occurs in the crux of many real-world applications of operations research, artificial intelligence, bioinformatics, etc. Despite its importance as a combinatorial substrate, many attempts for building an efficient WCSP solver have been largely unsatisfactory. In this paper, we introduce a new method for encoding a (Boolean) WCSP instance as an integer linear program (ILP). this encoding is based on the idea of the constraint composite graph (CCG) associated with a WCSP instance. We show that our CCG-based ILP encoding of the Boolean WCSP is significantly more efficient than previously known ILP encodings. theoretically, we show that the CCG-based ILP encoding has a number of interesting properties. Empirically, we show that it allows us to solve many hard Boolean WCSP instances that cannot be solved by ILP solvers with previously known ILP encodings.
暂无评论