We present a general constraint-based encoding for domain-independent task planning. Task planning is characterized by causal relationships expressed as conditions and effects of optional actions. Possible actions are...
详细信息
ISBN:
(数字)9783319983349
ISBN:
(纸本)9783319983349;9783319983332
We present a general constraint-based encoding for domain-independent task planning. Task planning is characterized by causal relationships expressed as conditions and effects of optional actions. Possible actions are typically represented by templates, where each template can be instantiated into a number of primitive actions. While most previous work for domain-independent task planning has focused on primitive actions in a state-oriented view, our encoding uses a fully lifted representation at the level of action templates. It follows a time-oriented view in the spirit of previous work in constraint-based scheduling. As a result, the proposed encoding is simple and compact as it grows withthe number of actions in a solution plan rather than the number of possible primitive actions. When solved with an SMT solver, we show that the proposed encoding is slightly more efficient than state-of-the-art methods on temporally constrained planning benchmarks while clearly outperforming other fully constraint-based approaches.
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.
In this paper we describe the design and implementation of CP-VIZ, a generic visualization platform for constraintprogramming. It provides multiple views to show the search tree, and the state of constraints and vari...
详细信息
ISBN:
(纸本)9783642153952
In this paper we describe the design and implementation of CP-VIZ, a generic visualization platform for constraintprogramming. It provides multiple views to show the search tree, and the state of constraints and variables for a postmortem analysis of a constraint program. Different to most previous visualization tools, it is system independent, using a light-weight, intermediate XML format to exchange information between solvers and the visualization tools. CP-VIZ is available under an open-source licence, and has already been interfaced to four different constraint systems.
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.
We argue that turning a logic program into a set of completed definitions can be sometimes thought of as the "reverse engineering" process of generating a set of conditions that could serve as a specificatio...
详细信息
We argue that turning a logic program into a set of completed definitions can be sometimes thought of as the "reverse engineering" process of generating a set of conditions that could serve as a specification for it. Accordingly, it may be useful to define completion for a large class of Answer Set programming (ASP) programs and to automate the process of generating and simplifying completion formulas. Examining the output produced by this kind of software may help programmers to see more clearly what their program does, and to what degree its behavior conforms withtheir expectations. As a step toward this goal, we propose here a definition of program completion for a large class of programs in the input language of the ASP grounder gringo, and study its properties.
暂无评论