A kernelization algorithm for a computational problem is a procedure which compresses an instance into an equivalent instance whose size is bounded with respect to a complexity parameter. For the constraint satisfacti...
详细信息
ISBN:
(纸本)9783319661582;9783319661575
A kernelization algorithm for a computational problem is a procedure which compresses an instance into an equivalent instance whose size is bounded with respect to a complexity parameter. For the constraint satisfaction problem (CSP), there exist many results concerning upper and lower bounds for kernelizability of specific problems, but it is safe to say that we lack general methods to determine whether a given problem admits a kernel of a particular size. In this paper, we take an algebraic approach to the problem of characterizing the kernelization limits of NP-hard CSP problems, parameterized by the number of variables. Our main focus is on problems admitting linear kernels, as has, somewhat surprisingly, previously been shown to exist. We show that a finite-domain CSP problem has a kernel with O(n) constraints if it can be embedded (via a domain extension) into a CSP which is preserved by a Maltsev operation. this result utilise a variant of the simple algorithm for Maltsev constraints. In the complementary direction, we give indication that the Maltsev condition might be a complete characterization for Boolean CSPs with linear kernels, by showing that an algebraic condition that is shared by all problems with a Maltsev embedding is also necessary for the existence of a linear kernel unless NP subset of co-NP/poly.
this paper studies how to verify the conformity of a program with its specification and proposes a novel constraint-programming framework for bounded program verification (CPBPV). the CPBPV framework uses constraint s...
详细信息
this paper studies how to verify the conformity of a program with its specification and proposes a novel constraint-programming framework for bounded program verification (CPBPV). the CPBPV framework uses constraint stores to represent boththe specification and the program and explores execution paths of bounded length nondeterministically. the CPBPV framework detects non-conformities and provides counter examples when a path of bounded lengththat refutes some properties exists. the input program is partially correct under the boundness restrictions, if each constraint store so produced implies the post-condition. CPBPV does not explore spurious execution paths, as it incrementally prunes execution paths early by detecting that the constraint store is not consistent. CPBPV uses the rich language of constraintprogramming to express the constraint store. Finally, CPBPV is parameterized with a list of solvers which are tried in sequence, starting withthe least expensive and less general. Experimental results often produce orders of magnitude improvements over earlier approaches, running times being often independent of the size of the variable domains. Moreover, CPBPV was able to detect subtle errors in some programs for which other frameworks based on bounded model checking have failed.
We study the experimental consequences of a recent theoretical result by Achlioptas et al. that shows that conventional models of random problems are trivially insoluble in the limit. We survey the literature to ident...
详细信息
ISBN:
(纸本)3540652248
We study the experimental consequences of a recent theoretical result by Achlioptas et al. that shows that conventional models of random problems are trivially insoluble in the limit. We survey the literature to identify experimental studies that lie within the scope of this result. We then estimate theoretically and measure experimentally the size at which problems start to become trivially insoluble. Our results demonstrate that most (but not all) of these experimental studies are luckily unaffected by this result. We also study an alternative model of random problems that does not suffer from this asymptotic weakness. We show that, at a typical problem size used in experimental studies, this model looks similar to conventional models. Finally, we generalize this model so that we can independently adjust the constraint tightness and density.
Although the Steel Mill Slab problem (prob 38 of CSPLib) has already been studied by the CP community, this approach is unfortunately not used anymore by steel producers since last century. Continuous casting is prefe...
详细信息
ISBN:
(纸本)9783319104287;9783319104270
Although the Steel Mill Slab problem (prob 38 of CSPLib) has already been studied by the CP community, this approach is unfortunately not used anymore by steel producers since last century. Continuous casting is preferred instead, allowing higher throughput and better steel quality. this paper presents a CP model related to scheduling of operations for steel making with continuous casting. Activities considered range from the extraction of iron in the furnace to its casting in continuous casters. We describe the problem, detail a CP scheduling model that is finally used to solve real-life instances of some of the PSI Metals' customers.
Recursively defined properties are ubiquitous. We present a proof method for establishing entailment G satisfies H of such properties G and H over a set of common variables. the main contribution is a particular proof...
详细信息
ISBN:
(纸本)9783540859574
Recursively defined properties are ubiquitous. We present a proof method for establishing entailment G satisfies H of such properties G and H over a set of common variables. the main contribution is a particular proof rule based intuitively upon the concept of coinduction. this rule allows the inductive step of assuming that tin entailment holds during the proof the entailment. In general, the proof method is based on an unfolding (and no folding) algorithm that reduces recursive definitions to a point where only constraint solving is necessary. the constraint-based proof obligation is then discharged with available solvers. the algorithm executes the proof-by a search-based method which automatically discovers the opportunity of applying induction instead of the user having to specify some induction schema, and which does not require any base case.
the success of several constraint-based modeling languages such as OPL, ZINC, or COMET, appeals for better software engineering practices, particularly in the testing phase. this paper introduces a testing framework e...
详细信息
ISBN:
(纸本)9783642153952
the success of several constraint-based modeling languages such as OPL, ZINC, or COMET, appeals for better software engineering practices, particularly in the testing phase. this paper introduces a testing framework enabling automated test case generation for constraintprogramming. We propose a general framework of constraint program development which supposes that a first declarative and simple constraint model is available from the problem specifications analysis. then, this model is refined using classical techniques such as constraint reformulation, surrogate and global constraint addition, or symmetry-breaking to form an improved constraint model that must be thoroughly tested before being used to address real-sized problems. We think that most of the faults are introduced in this refinement step and propose a process which takes the first declarative model as an oracle for detecting non-conformities. We derive practical test purposes from this process to generate automatically test data that exhibit non-conformities. We implemented this approach in a new tool called CPTEST that was used to automatically detect non-conformities on two classical benchmark programs, namely the Golomb rulers and the car-sequencing problem.
Flight routes are paths in a network, the nodes of which represent waypoints in a 3D space. A common approach to route planning is first to calculate a cheapest path in a 2D space, and then to optimize the flight cost...
详细信息
ISBN:
(纸本)9783319661582;9783319661575
Flight routes are paths in a network, the nodes of which represent waypoints in a 3D space. A common approach to route planning is first to calculate a cheapest path in a 2D space, and then to optimize the flight cost in the third dimension. We focus on the problem of finding a cheapest paththrough a network describing the 2D projection of the 3D waypoints. In European airspaces, traffic flow is handled by heavily constraining the flight network. the constraints can have very diverse structures, among them a generalization of the forbidden pairs type. they invalidate the FIFO property, commonly assumed in shortest path problems. We formalize the problem and provide a framework for the description, representation and propagation of the constraints in path finding algorithms, best-first, and A* search. In addition, we study a lazy approach to deal withthe constraints. We conduct an experimental evaluation based on real-life data and conclude that our techniques for constraint propagation work best together with an iterative search approach, in which only constraints that are violated in previously found routes are introduced in the constraint set before the search is restarted.
Large neighborhood search (LNS) [25] is a framework that combines the expressiveness of constraintprogramming withthe efficiency of local search to solve combinatorial optimization problems. this paper introduces an...
详细信息
ISBN:
(纸本)9783642406263;9783642406270
Large neighborhood search (LNS) [25] is a framework that combines the expressiveness of constraintprogramming withthe efficiency of local search to solve combinatorial optimization problems. this paper introduces an extension of LNS, called multi-objective LNS (MO-LNS), to solve multi-objective combinatorial optimization problems ubiquitous in practice. the idea of MO-LNS is to maintain a set of nondominated solutions rather than just one best-so-far solution. At each iteration, one of these solutions is selected, relaxed and optimized in order to strictly improve the hypervolume of the maintained set of nondominated solutions. We introduce modeling abstractions into the OscaR solver for MO-LNS and show experimentally the efficiency of this approach on various multi-objective combinatorial optimization problems.
the constraint paradigm provides powerful concepts to represent and solve different kinds of planning problems. Typically a large and conflicting set of restrictions, objectives and preferences has to be considered fo...
详细信息
ISBN:
(纸本)3540652248
the constraint paradigm provides powerful concepts to represent and solve different kinds of planning problems. Typically a large and conflicting set of restrictions, objectives and preferences has to be considered for real planning problems. We introduce a unified formalism - called Petri decision nets -for representation and implementation of complex CSP solution algorithms. the formalism enables the consideration of the problem structure as well as given objectives and the usage of problem specific heuristics or expert knowledge. It is based on the fundamental assumption that designing CSP solution algorithms means designing decision networks.
the protein structure prediction problem is one of the most (if not the most) important problem in computational biology. this problem consists of finding the conformation of a protein (i.e., a sequence of amino-acids...
详细信息
ISBN:
(纸本)3540652248
the protein structure prediction problem is one of the most (if not the most) important problem in computational biology. this problem consists of finding the conformation of a protein (i.e., a sequence of amino-acids) with minimal energy. Because of the complexity of this problem, simplified models like Dill's HP-lattice model [12] have become a major tool for investigating general properties of protein folding. Even for this simplified model, the structure prediction problem has been shown to be NP-complete [3, 5]. We describe a constraint formulation of the HP-model structure prediction problem, present the basic constraints and search strategy. We then introduce a novel, general technique for excluding geometrical symmetries in constraintprogramming. To our knowledge, this is the first general and declarative technique for excluding symmetries in constraintprogrammingthat can be added to an existing implementation. Finally, we describe a new lower bound on the energy of an HP-protein. Both techniques yield an efficient pruning of the search tree.
暂无评论