constraint solvers are complex pieces of software and are notoriously difficult to debug. In large part this is due to the difficulty of pinpointing the source of an error in the vast searches these solvers perform, s...
详细信息
ISBN:
(数字)9783319983349
ISBN:
(纸本)9783319983349;9783319983332
constraint solvers are complex pieces of software and are notoriously difficult to debug. In large part this is due to the difficulty of pinpointing the source of an error in the vast searches these solvers perform, since the effect of an error may only come to light long after the error is made. In addition, an error does not necessarily lead to the wrong result, further complicating the debugging process. A major source of errors in a constraint solver is the complex constraint propagation algorithms that provide the inference that controls and directs the search. In this paper we show that metamorphic testing is a principled way to test constraint solvers by comparing two different implementations of the same constraint. Specifically, specialised propagators for the constraint are tested against the general purpose table constraint propagator. We report on metamorphic testing of the constraint solver Minion. We demonstrate that the metamorphic testing method is very effective for finding artificial bugs introduced by random code mutation.
constraintprogramming (CP) and propositional satisfiability (SAT) based framework for modeling and solving pattern mining tasks has gained a considerable audience in recent years. However, this nice declarative and g...
详细信息
ISBN:
(数字)9783319983349
ISBN:
(纸本)9783319983349;9783319983332
constraintprogramming (CP) and propositional satisfiability (SAT) based framework for modeling and solving pattern mining tasks has gained a considerable audience in recent years. However, this nice declarative and generic framework encounters a scaling problem. the huge size of constraints networks/propositional formulas encoding large datasets is identified as the main bottleneck of most existing approaches. In this paper, we propose a parallel SAT based framework for itemset mining problem to push forward the solving efficiency. the proposed approach is based on a divide-and-conquer paradigm, where the transaction database is partitioned using item-based guiding paths. Such decomposition allows us to derive smaller and independent Boolean formulas that can be solved in parallel. the performance and scalability of the proposed algorithm are evaluated through extensive experiments on several datasets. We demonstrate that our partition-based parallel SAT approach outperforms other CP approaches even in the sequential case, while significantly reducing the performances gap with specialized approaches.
constraint acquisition systems such as QuAcq and MultiAcq can assist non-expert users to model their problems as constraint networks by classifying (partial) examples as positive or negative. For each negative example...
详细信息
ISBN:
(数字)9783319983349
ISBN:
(纸本)9783319983349;9783319983332
constraint acquisition systems such as QuAcq and MultiAcq can assist non-expert users to model their problems as constraint networks by classifying (partial) examples as positive or negative. For each negative example, the former focuses on one constraint of the target network, while the latter can learn a maximum number of constraints. Two bottlenecks of the acquisition process where boththese algorithms encounter problems are the large number of queries required to reach convergence, and the high cpu times needed to generate queries, especially near convergence. We propose methods that deal with boththese issues. the first one is an algorithm that blends the main idea of MultiAcq into QuAcq resulting in a method that learns as many constraints as MultiAcq does after a negative example, but with a lower complexity. the second is a technique that helps reduce the number of queries significantly. the third is based on the use of partial queries to cut down the time required for convergence. Experiments demonstrate that our resulting algorithm, which integrates all the new techniques, does not only generate considerably fewer queries than QuAcq and MultiAcq, but it is also by far faster than both of them, both in average query generation time and in total run time.
Tolerant Algebraic Side-Channel Attack (TASCA) is a combination of algebraic and side-channel analysis with error tolerance. Oren et al., used mathematical programming to implement TASCA over a round-limited version o...
详细信息
ISBN:
(数字)9783319983349
ISBN:
(纸本)9783319983349;9783319983332
Tolerant Algebraic Side-Channel Attack (TASCA) is a combination of algebraic and side-channel analysis with error tolerance. Oren et al., used mathematical programming to implement TASCA over a round-limited version of AES. In [7], Liu et al. revisited their results and introduced a TASCA-CP model that delivers solutions to this 1-round relaxation with orders of magnitude improvement in both solving time and memory consumption. this paper extends the result and considers TASCA for the full 10-rounds AES algorithm. Two approaches are introduced: staged and integrated. the staged approach uses TASCA-CP as a spring board to enumerate and check its candidate solutions against the requirements of subsequent rounds. the integrated model formulates all the rounds of AES together with side-channel constraints on all rounds within a single unified optimization model. Empirical results shows both approaches are suitable to find the correct key of AES while the integrated model dominates the staged both in simplicity and solving time.
We study the complexity of the quantified and valued extension of the constraint satisfaction problem (QVCSP) for certain classes of languages. this problem is also known as the weighted constraint satisfaction proble...
详细信息
ISBN:
(数字)9783319983349
ISBN:
(纸本)9783319983349;9783319983332
We study the complexity of the quantified and valued extension of the constraint satisfaction problem (QVCSP) for certain classes of languages. this problem is also known as the weighted constraint satisfaction problem with min-max quantifiers [1]. the multimorphisms that preserve a language is the starting point of our analysis. We establish some situations where a QVCSP is solvable in polynomial time by formulating new algorithms or by extending the usage of collapsibility, a property well known for reducing the complexity of the quantified CSP (QCSP) from Pspace to NP. In contrast, we identify some classes of problems for which the VCSP is tractable but the QVCSP is Pspace-hard. As a main Corollary, we derive an analogue of Shaeffer's dichotomy between P and Pspace for QCSP on Boolean languages and Cohen et al. dichotomy between P and NP-complete for VCSP on Boolean valued languages: we prove that the QVCSP follows a dichotomy between P and Pspace-complete. Finally, we exhibit examples of NP-complete QVCSP for domains of size 3 and more, which suggest at best a trichotomy between P, NP-complete and Pspace-complete for the QVCSP.
Max-sum is a version of Belief Propagation, used for solving DCOPs. On tree-structured problems, Max-sum converges to the optimal solution in linear time. When the constraint graph representing the problem includes mu...
详细信息
ISBN:
(数字)9783319983349
ISBN:
(纸本)9783319983349;9783319983332
Max-sum is a version of Belief Propagation, used for solving DCOPs. On tree-structured problems, Max-sum converges to the optimal solution in linear time. When the constraint graph representing the problem includes multiple cycles, Max-sum might not converge and explore low quality solutions. Damping is a method that increases the chances that Max-sum will converge. Damped Max-sum (DMS) was recently found to produce high quality solutions for DCOP when combined with an anytime framework. We propose a novel method for adjusting the level of asymmetry in the factor graph, in order to achieve a balance between exploitation and exploration, when using Max-sum for solving DCOPs. By converting a standard factor graph to an equivalent split constraint factor graph (SCFG), in which each function-node is split to two function-nodes, we can control the level of asymmetry for each constraint. Our empirical results demonstrate that by applying DMS to SCFGs with a minor level of asymmetry we can find high quality solutions in a small number of iterations, even without using an anytime framework. As part of our investigation of this success, we prove that for a factor-graph with a single constraint, if this constraint is split symmetrically, Max-sum applied to the resulting cycle is guaranteed to converge to the optimal solution and demonstrate that for an asymmetric split, convergence is not guaranteed.
In continuous constraintprogramming, the solving process alternates propagation steps, which reduce the search space according to the constraints, and branching steps. In practice, the solvers spend a lot of computat...
详细信息
ISBN:
(数字)9783319983349
ISBN:
(纸本)9783319983349;9783319983332
In continuous constraintprogramming, the solving process alternates propagation steps, which reduce the search space according to the constraints, and branching steps. In practice, the solvers spend a lot of computation time in propagation to separate feasible and infeasible parts of the search space. the constraint propagators cut the search space into two subspaces: the inconsistent one, which can be discarded, and the consistent one, which may contain solutions and where the search continues. the status of all this consistent subspace is thus indeterminate. In this article, we introduce a new step called elimination. It refines the analysis of the consistent subspace by dividing it into an indeterminate one, where the search must continue, and a satisfied one, where the constraints are always satisfied. the latter can be stored and removed from the search process. Elimination relies on the propagation of the negation of the constraints, and a new difference operator to efficiently compute the obtained set as an union of boxes, thus it uses the same representations and algorithms as those already existing in the solvers. Combined with propagation, elimination allows the solver to focus on the frontiers of the constraints, which is the core difficult part of the problem. We have implemented our method in the AbSolute solver, and present experimental results on classic benchmarks with good performances.
For classical CSPs, the absence of broken triangles on a pair of values allows the merging of these values without changing the satisfiability of the instance, giving experimentally verified reduction in search time. ...
详细信息
ISBN:
(数字)9783319983349
ISBN:
(纸本)9783319983349;9783319983332
For classical CSPs, the absence of broken triangles on a pair of values allows the merging of these values without changing the satisfiability of the instance, giving experimentally verified reduction in search time. We generalise the notion of broken triangles to VCSPs to obtain a tractable value-merging rule which preserves the cost of a solution. We then strengthen this value merging rule by using soft arc consistency to remove soft broken triangles and we show that the combined rule generalises known notions of domain value substitutability and inter-changeability. Unfortunately the combined rules are no longer tractable to apply, but can still have applications as heuristics for reducing the search space. Finally we consider the generalisation of another value-elimination rule for CSPs to binary VCSPs. this new rule properly generalises neighbourhood substitutability and so we expect it will also have practical applications.
Many attempts have been made to apply machine learning techniques to constraint satisfaction problems (CSPs). However, none of them have made use of the recent advances in deep learning. In this paper, we apply deep l...
详细信息
ISBN:
(数字)9783319983349
ISBN:
(纸本)9783319983349;9783319983332
Many attempts have been made to apply machine learning techniques to constraint satisfaction problems (CSPs). However, none of them have made use of the recent advances in deep learning. In this paper, we apply deep learning to predict the satisfiabilities of CSPs. To the best of our knowledge, this is the first effective application of deep learning to CSPs that yields >99.99% prediction accuracy on random Boolean binary CSPs whose constraint tightnesses or constraint densities do not determine their satisfiabilities. We use a deep convolutional neural network on a matrix representation of CSPs. Since it is NP-hard to solve CSPs, labeled data required for training are in general costly to produce and are thus scarce. We address this issue using the asymptotic behavior of generalized Model A, a new random CSP generation model, along with domain adaptation and data augmentation techniques for CSPs. We demonstrate the effectiveness of our deep learning techniques using experiments on random Boolean binary CSPs. While these CSPs are known to be in P, we use them for a proof of concept.
Bounded fractional hypertree width (fhtw) is the most general known structural property that guarantees polynomial-time solvability of the constraint satisfaction problem. Bounded fhtw generalizes other structural pro...
详细信息
ISBN:
(数字)9783319983349
ISBN:
(纸本)9783319983349;9783319983332
Bounded fractional hypertree width (fhtw) is the most general known structural property that guarantees polynomial-time solvability of the constraint satisfaction problem. Bounded fhtw generalizes other structural properties like bounded induced width and bounded hypertree width. We propose, implement and test the first practical algorithm for computing the fhtw and its associated structural decomposition. We provide an extensive empirical evaluation of our method on a large class of benchmark instances which also provides a comparison with known exact decomposition methods for hypertree width. Our approach is based on an efficient encoding of the decomposition problem to SMT (SAT modulo theory) with Linear Arithmetic as implemented in the SMT solver Z3. the encoding is further strengthened by preprocessing and symmetry breaking methods. Our experiments show (i) that fhtw can indeed be computed exactly for a wide range of benchmark instances, and (ii) that state-of-the art SMT techniques can be successfully applied for structural decomposition.
暂无评论