Efficient Singleton Consistency by Combining Forward Checking and Bound Consistency

2014 ◽  
Vol 23 (04) ◽  
pp. 1460017
Author(s):  
Jinsong Guo ◽  
Hongbo Li ◽  
Zhanshan Li ◽  
Yonggang Zhang ◽  
Xianghua Jia

Maintaining local consistencies can improve the efficiencies of the search algorithms solving constraint satisfaction problems (CSPs). Comparing with arc consistency which is the most widely used local consistency, stronger local consistencies can make the search space smaller while they require higher computational cost. In this paper, we make an attempt on the compromise between the pruning ability and the computational cost. A new local consistency called singleton strong bound consistency (SSBC) and its light version, light SSBC, are proposed. The search algorithm maintaining light SSBC can outperform MAC on a considerable number of problems.

Author(s):  
Marlene Arangú ◽  
Miguel Salido

A fine-grained arc-consistency algorithm for non-normalized constraint satisfaction problems Constraint programming is a powerful software technology for solving numerous real-life problems. Many of these problems can be modeled as Constraint Satisfaction Problems (CSPs) and solved using constraint programming techniques. However, solving a CSP is NP-complete so filtering techniques to reduce the search space are still necessary. Arc-consistency algorithms are widely used to prune the search space. The concept of arc-consistency is bidirectional, i.e., it must be ensured in both directions of the constraint (direct and inverse constraints). Two of the most well-known and frequently used arc-consistency algorithms for filtering CSPs are AC3 and AC4. These algorithms repeatedly carry out revisions and require support checks for identifying and deleting all unsupported values from the domains. Nevertheless, many revisions are ineffective, i.e., they cannot delete any value and consume a lot of checks and time. In this paper, we present AC4-OP, an optimized version of AC4 that manages the binary and non-normalized constraints in only one direction, storing the inverse founded supports for their later evaluation. Thus, it reduces the propagation phase avoiding unnecessary or ineffective checking. The use of AC4-OP reduces the number of constraint checks by 50% while pruning the same search space as AC4. The evaluation section shows the improvement of AC4-OP over AC4, AC6 and AC7 in random and non-normalized instances.


2001 ◽  
Vol 1 (6) ◽  
pp. 713-750 ◽  
Author(s):  
KRZYSZTOF R. APT ◽  
ERIC MONFROY

We study here a natural situation when constraint programming can be entirely reduced to rule-based programming. To this end we explain first how one can compute on constraint satisfaction problems using rules represented by simple first-order formulas. Then we consider constraint satisfaction problems that are based on predefined, explicitly given constraints. To solve them we first derive rules from these explicitly given constraints and limit the computation process to a repeated application of these rules, combined with labeling. We consider two types of rule here. The first type, that we call equality rules, leads to a new notion of local consistency, called rule consistency that turns out to be weaker than arc consistency for constraints of arbitrary arity (called hyper-arc consistency in Marriott & Stuckey (1998)). For Boolean constraints rule consistency coincides with the closure under the well-known propagation rules for Boolean constraints. The second type of rules, that we call membership rules, yields a rule-based characterization of arc consistency. To show feasibility of this rule-based approach to constraint programming, we show how both types of rules can be automatically generated, as CHR rules of Frühwirth (1995). This yields an implementation of this approach to programming by means of constraint logic programming. We illustrate the usefulness of this approach to constraint programming by discussing various examples, including Boolean constraints, two typical examples of many valued logics, constraints dealing with Waltz's language for describing polyhedral scenes, and Allen's qualitative approach to temporal logic.


2020 ◽  
Vol 174 (3-4) ◽  
pp. 311-344
Author(s):  
Richard J. Wallace

Algorithms based on singleton arc consistency (SAC) show considerable promise for improving backtrack search algorithms for constraint satisfaction problems (CSPs). The drawback is that even the most efficient of them is still comparatively expensive. Even when limited to preprocessing, they give overall improvement only when problems are quite difficult to solve with more typical procedures such as maintained arc consistency (MAC). The present work examines a form of partial SAC and neighbourhood SAC (NSAC) in which a subset of the variables in a CSP are chosen to be made SAC-consistent or neighbourhood-SAC-consistent. Such consistencies, despite their partial character, are still well-characterized in that algorithms have unique fixpoints. Heuristic strategies for choosing an effective subset of variables are described and tested, the best being choice by highest degree and a more complex strategy of choosing by constraint weight after random probing. Experimental results justify the claim that these methods can be nearly as effective as the corresponding full version of the algorithm in terms of values discarded or problems proven unsatisfiable, while significantly reducing the effort required to achieve this.


2008 ◽  
Vol 105 (40) ◽  
pp. 15253-15257 ◽  
Author(s):  
Mikko Alava ◽  
John Ardelius ◽  
Erik Aurell ◽  
Petteri Kaski ◽  
Supriya Krishnamurthy ◽  
...  

We study the performance of stochastic local search algorithms for random instances of the K-satisfiability (K-SAT) problem. We present a stochastic local search algorithm, ChainSAT, which moves in the energy landscape of a problem instance by never going upwards in energy. ChainSAT is a focused algorithm in the sense that it focuses on variables occurring in unsatisfied clauses. We show by extensive numerical investigations that ChainSAT and other focused algorithms solve large K-SAT instances almost surely in linear time, up to high clause-to-variable ratios α; for example, for K = 4 we observe linear-time performance well beyond the recently postulated clustering and condensation transitions in the solution space. The performance of ChainSAT is a surprise given that by design the algorithm gets trapped into the first local energy minimum it encounters, yet no such minima are encountered. We also study the geometry of the solution space as accessed by stochastic local search algorithms.


2020 ◽  
Vol 34 (02) ◽  
pp. 1644-1651
Author(s):  
Yuki Satake ◽  
Hiroshi Unno ◽  
Hinata Yanagi

In this paper, we present a novel constraint solving method for a class of predicate Constraint Satisfaction Problems (pCSP) where each constraint is represented by an arbitrary clause of first-order predicate logic over predicate variables. The class of pCSP properly subsumes the well-studied class of Constrained Horn Clauses (CHCs) where each constraint is restricted to a Horn clause. The class of CHCs has been widely applied to verification of linear-time safety properties of programs in different paradigms. In this paper, we show that pCSP further widens the applicability to verification of branching-time safety properties of programs that exhibit finitely-branching non-determinism. Solving pCSP (and CHCs) however is challenging because the search space of solutions is often very large (or unbounded), high-dimensional, and non-smooth. To address these challenges, our method naturally combines techniques studied separately in different literatures: counterexample guided inductive synthesis (CEGIS) and probabilistic inference in graphical models. We have implemented the presented method and obtained promising results on existing benchmarks as well as new ones that are beyond the scope of existing CHC solvers.


2001 ◽  
Vol 14 ◽  
pp. 53-81 ◽  
Author(s):  
X. Chen ◽  
P. Van Beek

In recent years, many improvements to backtracking algorithms for solving constraint satisfaction problems have been proposed. The techniques for improving backtracking algorithms can be conveniently classified as look-ahead schemes and look-back schemes. Unfortunately, look-ahead and look-back schemes are not entirely orthogonal as it has been observed empirically that the enhancement of look-ahead techniques is sometimes counterproductive to the effects of look-back techniques. In this paper, we focus on the relationship between the two most important look-ahead techniques---using a variable ordering heuristic and maintaining a level of local consistency during the backtracking search---and the look-back technique of conflict-directed backjumping (CBJ). We show that there exists a ``perfect'' dynamic variable ordering such that CBJ becomes redundant. We also show theoretically that as the level of local consistency that is maintained in the backtracking search is increased, the less that backjumping will be an improvement. Our theoretical results partially explain why a backtracking algorithm doing more in the look-ahead phase cannot benefit more from the backjumping look-back scheme. Finally, we show empirically that adding CBJ to a backtracking algorithm that maintains generalized arc consistency (GAC), an algorithm that we refer to as GAC-CBJ, can still provide orders of magnitude speedups. Our empirical results contrast with Bessiere and Regin's conclusion (1996) that CBJ is useless to an algorithm that maintains arc consistency.


Author(s):  
Tad Hogg

Phase transitions have long been studied empirically in various combinatorial searches and theoretically in simplified models [91, 264, 301, 490]. The analogy with statistical physics [397], explored throughout this volume, shows how the many local choices made during search relate to global properties such as the resulting search cost. These studies have led to a better understanding of typical search behaviors [514] and improved search methods [195, 247, 261, 432, 433]. Among the current research questions in this field are the range of algorithms exhibiting the transition behavior and the algorithm-independent problem properties associated with the difficult instances concentrated near the transition. Towards this end, the present chapter examines quantum computer [123, 126, 158, 486] algorithms for nondeterministic polynomial (NP) combinatorial search problems [191]. As with many conventional methods, they exhibit the easy-hard-easy pattern of computational cost as the degree of constraint in the problems varies. We describe how properties of the search space affect the algorithms and identify an additional structural property, the energy gap, motivated by one quantum algorithm but applicable to a variety of techniques, both quantum and classical. Thus, the study of quantum search algorithms not only extends the range of algorithms exhibiting phase transitions, but also helps identify underlying structural properties. Specifically, the next two sections describe a class of hard search problems and the form of quantum search algorithms proposed to date. The remainder of the chapter presents algorithm behaviors, relevant problem structure, arid an approximate asymptotic analysis of their cost scaling. The final section discusses various open issues in designing and evaluating quantum algorithms, and relating their behavior to problem structure. The k-satisfiability (k -SAT) problem, as discussed earlier in this volume, consists of n Boolean variables and m clauses. A clause is a logical OR of k variables, each of which may be negated. A solution is an assignment, that is, a value for each variable, TRUE or FALSE, satisfying all the clauses. An assignment is said to conflict with any clause it does not satisfy.


2020 ◽  
Vol 11 (2) ◽  
pp. 192-207 ◽  
Author(s):  
Patrick Kenekayoro ◽  
Promise Mebine ◽  
Bodouowei Godswill Zipamone

The student project allocation problem is a well-known constraint satisfaction problem that involves assigning students to projects or supervisors based on a number of criteria. This study investigates the use of population-based strategies inspired from physical phenomena (gravitational search algorithm), evolutionary strategies (genetic algorithm), and swarm intelligence (ant colony optimization) to solve the Student Project Allocation problem for a case study from a real university. A population of solutions to the Student Project Allocation problem is represented as lists of integers, and the individuals in the population share information through population-based heuristics to find more optimal solutions. All three techniques produced satisfactory results and the adapted gravitational search algorithm for discrete variables will be useful for other constraint satisfaction problems. However, the ant colony optimization algorithm outperformed the genetic and gravitational search algorithms for finding optimal solutions to the student project allocation problem in this study.


Author(s):  
S. Nagarajan ◽  
S. D. Goodwin ◽  
A. Sattar

Many extensions to existing binary constraint satisfaction algorithms have been proposed that directly deal with nonbinary constraints. Another choice is to perform a structural transformation of the representation of the problem, so that the resulting problem is a binary CSP except that now the original constraints which were nonbinary are replaced by binary compatibility constraints between relations. A lot of recent work has focussed on comparing different levels of local consistency enforceable in the nonbinary representation with the dual representation. In this paper we present extensions to the standard dual encoding that can compactly represent the given CSP using an equivalent dual encoding that contains all the original solutions to the CSP, using constraint coverings. We show how enforcing arc consistency in these constraint covering based encodings, strictly dominates enforcement of generalized arc consistency (GAC) on the primal nonbinary encoding.


Sign in / Sign up

Export Citation Format

Share Document