We present a method for solving weighted constraint Satisfaction Problems, based on translation into a constraint Optimization Problem and iterative calls to an SMT solver, with successively tighter bounds of the obje...
详细信息
ISBN:
(纸本)9783319104287;9783319104270
We present a method for solving weighted constraint Satisfaction Problems, based on translation into a constraint Optimization Problem and iterative calls to an SMT solver, with successively tighter bounds of the objective function. the novelty of the method herewith described lies in representing the bound constraint as a shared Binary Decision Diagram, which in turn is translated into SAT. this offers two benefits: first, BDDs built for previous bounds can be used to build the BDDs for new (tighter) bounds, considerably reducing the BDD construction time;second, as a by-product, many clauses asserted to the solver in previous iterations can be reused. the reported experimentation on the WSimply system shows that this technique has better performance in general than other methods implemented in the system. Moreover, withthe new technique WSimply outperforms some state-of-the-art solvers in most of the studied instances.
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 Handling Rules (CHR) is a high-level language for writing constraint solvers either from scratch or by modifying existing solvers. An important property of any constraint solver is confluence: the result of...
详细信息
ISBN:
(纸本)3540652248
constraint Handling Rules (CHR) is a high-level language for writing constraint solvers either from scratch or by modifying existing solvers. An important property of any constraint solver is confluence: the result of a computation should be independent from the order in which constraints arrive and in which rules are applied. In previous work [1], a sufficient and necessary condition for the confluence of terminating CHR programs was given by adapting and extending results about conditional term rewriting systems. In this paper we investigate so-called completion methods that make a non-confluent CHR program confluent by adding new rules. As it turns out, completion can also exhibit inconsistency of a CHR program. Moreover, as shown in this paper, completion can be used to define new constraints in terms of already existing constraints and to derive constraint solvers for them.
We investigate utilizing the integer programming (IP) technique of reduced cost fixing to improve maximum satisfiability (MaxSAT) solving. In particular, we show how reduced cost fixing can be used within the implicit...
详细信息
ISBN:
(纸本)9783319661582;9783319661575
We investigate utilizing the integer programming (IP) technique of reduced cost fixing to improve maximum satisfiability (MaxSAT) solving. In particular, we show how reduced cost fixing can be used within the implicit hitting set approach (IHS) for solving MaxSAT. Solvers based on IHS have proved to be quite effective for MaxSAT, especially on problems with a variety of clause weights. the unique feature of IHS solvers is that they utilize both SAT and IP techniques. We show how reduced cost fixing can be used in this framework to conclude that some soft clauses can be left falsified or forced to be satisfied without influencing the optimal cost. Applying these forcings simplifies the remaining problem. We provide an extensive empirical study showing that reduced cost fixing employed in this manner can be useful in improving the state-of-the-art in MaxSAT solving especially on hard instances arising from real-world application domains.
We propose a framework to construct web-oriented user interfaces in a high-level way by exploiting declarative programming techniques. Such user interfaces are intended to manipulate complex data in a type-safe way, i...
详细信息
In practice, SQL programmers often encounter queries which are hard to formulate using SQL statements. Many of them do not know if the queries are too hard beyond their capabilities, or they are the limitations of the...
详细信息
In this paper we show that the clique concept can be exploited in order to solve Max-CSP. We present a clique inference process which leads to construct linear systems useful for computing new lower bounds. the clique...
详细信息
ISBN:
(纸本)3540462678
In this paper we show that the clique concept can be exploited in order to solve Max-CSP. We present a clique inference process which leads to construct linear systems useful for computing new lower bounds. the clique inference process is introduced in the PFC-MPRDAC [5] algorithm and the obtained algorithm is called PFC-MPRDAC+CBB (CBB for Clique Based Bound). the carried out experiments have shown that PFC-MPRDAC+CBB leads to obtain very encouraging results.
We propose an adaptation of the Embarrassingly Parallel Search (EPS) method for data centers. EPS is a simple but efficient method for parallel solving of CSPs. EPS decomposes the problem in many distinct subproblems ...
详细信息
ISBN:
(纸本)9783319104287;9783319104270
We propose an adaptation of the Embarrassingly Parallel Search (EPS) method for data centers. EPS is a simple but efficient method for parallel solving of CSPs. EPS decomposes the problem in many distinct subproblems which are then solved independently by workers. EPS performed well on multicores machines (40), but some issues arise when using more cores in a datacenter. Here, we identify the decomposition as the cause of the degradation and propose a parallel decomposition to address this issue. thanks to it, EPS gives almost linear speedup and outperforms work stealing by orders of magnitude using the Gecode solver.
the length-lex representation for set variables orders all subsets of a given universe of values according to cardinality and lexicography. To achieve length-lex bounds consistency for Knapsack constraints it has been...
详细信息
ISBN:
(纸本)9783642042430
the length-lex representation for set variables orders all subsets of a given universe of values according to cardinality and lexicography. To achieve length-lex bounds consistency for Knapsack constraints it has been proposed to decompose the constraint into two sum constraints. We provide theoretical and practical evidence which shows that decomposition increases the problem of computing a fixpoint which is intrinsic to the length-lex representation: 1. the fixpoint problem for this domain representation is NP-hard in general. 2. For a tractable sub-family of Knapsack decomposition takes more time than exponential brute-force enumeration. 3. Experimental results on decomposed Knapsack constraints show that exponential-time fixpoint computation is the rule and not some pathological exception.
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.
暂无评论