Filtering Nogoods Lazily in Dynamic Symmetry Breaking During Search

Introduction

Advantages of dynamic symmetry breaking methods, such as SBDS [Gent and Smith, 2000; Gent, Harvey, and Kelsey, 2002] and SBDD [Fahle, Schamberger, and Sellmann, 2001; Gent et al., 2003], include completeness, ability to break symmetries of arbitrary kinds and compatibility with variable and value heuristics. When considering runtime, dynamic methods often lose out to widely used static methods, such as the LexLeader method [Crawford et al., 1996] and value precedence [Law and Lee, 2006], which require no modifications to the solver and often have less overheads. Based on SBDS, ReSBDS [Lee and Zhu, 2014a] and LReSBDS [Lee and Zhu, 2014b] break additional symmetry compositions thereby, further pruning the solution and search space. Instead of maintaining the large number of symmetry breaking nogoods in the constraint store, the increasing-nogood (incNGs) global constraint [Lee and Zhu, 2014b] collects all nogoods for a symmetry and filters them with an incremental and stronger filtering algorithm. Such recent advances greatly increase the competitiveness of dynamic approaches against the state of the art static methods.

SBDS adds conditional symmetry breaking nogoods dynamically upon backtracking to avoid exploring symmetrically equivalents of visited search space. However, nogoods are weak in pruning and maintaining GAC is not cost effective even when the watched literal technique [Moskewicz et al., 2001] is utilized. In addition, the number of such nogoods is often large, incurring big overheads to the constraint store.

In this work, we propose weak-nogood consistency (WNC), a weaker consistency notion for nogoods to trade pruning power for efficiency. To enforce GAC on a nogood, usual implementation watches two assignments (as literals) of the nogood. We present an efficient lazy propagator to enforce WNC for SBDS (and its variants) using one watched literal. First, our propagator generates the watched assignment on demand from partial assignment of the current search path. Second, the propagator is triggered lazily when the watched assignment becomes true, and effects prunings only when all but the last assignment of the nogood is true.

A similar weaker consistency, generalized weak-incNGs consistency (GWIC), together with a lazy propagator is also proposed for the incNGs constraint [Lee and Zhu, 2014b]. By exploiting the increasing property of the nogoods in incNGs, our lazy propagator watches also one assignment for each global constraint, and operates and benefits from a similar lazy principle. We give formal characterization of the pruning strengths of the proposed propagators, and also the space and time complexities. Various lazy versions of SBDS and its variants are implemented. We give experimentation to demonstrate the efficiency of the lazy versions as compared to state of the art symmetry breaking methods.

Background

A constraint satisfaction problem (CSP) P is a tuple (X,D,C) where X is a finite set of variables {x0, . . . , xn-1}, D is a finite set of domains such that each x ∈ X has a D(x) and C is a set of constraints, each is a subset of the Cartesian product D(xi1 ) × . . . × D(xik ) of the domains of the involved variables. A constraint is generalized arc consistent (GAC) iff when a variable in the scope of a constraint is assigned any value in its domain, there exist compatible values (called supports) in the domains of all the other variables in the scope of the constraint. A CSP is GAC iff every constraint is GAC. An assignment x = v is an equality constraint assigning value v to variable x. A full assignment is a set of assignments, one for each variable in X. A partial assignment is a subset of a full assignment. A solution to P is a full assignment that satisfies every member of C. An assignment x = v is satisfied iff D(x) = {v}. An assignment x = v is falsified iff v ̸∈ D(x). If an assignment is neither satisfied nor falsified, it is unresolved.

A nogood is the negation of a partial assignment which is not in any solution. Nogoods can also be expressed in an equivalent implication form. A directed nogood ng is an implication of the form (xs0 = vs0 ) ∧ . . . ∧ (xsm = vsm ) ⇒ (xk ̸= vk), where the left hand side (LHS) (lhs(ng) ≡ (xs0 = vs0 ) ∧ . . . ∧ (xsm = vsm )) and the right hand side (RHS) (rhs(ng) ≡ (xk ̸= vk)) are defined with respect to the position of ⇒. We call all assignments in the LHS as the LHS assignments and the negation of the RHS as the RHS assignment. The meaning of ng is that the RHS assignment xk = vk is incompatible with the LHS assignments, and vk should be ruled out from D(xk) when the LHS is true. If lhs(ng) is empty, ng is unconditional. Hereafter, directed nogoods are simply called nogoods when the context is clear.

In this paper, we consider search trees with binary branching, in which every non-leaf node has exactly two children. Suppose a non-leaf node P1 has x and v ∈ D(x) as the branching variable and value. The left and right children of P1 are P1 ∪ {x = v} and P1 ∪ {x ̸= v} respectively. We call x = v the branching assignment from P1 to P1∪{x = v} and backtracking assignment from P1∪{x = v} to P1∪{x ̸= v}. We say that backtracking takes place at P1. Each node P1 is associated with a partial assignment A1 which is the set of branching assignments collected from the root P to P1. If a node P0 is in a subtree under node P1, P0 is the descendant node of P1 and P1 is the ancestor node of P0.

We assume that the CSP, except the generated symmetry breaking nogoods, at a search tree node is always made GAC using an AC3-like [Mackworth, 1977] algorithm to coordinate the triggering of the propagators associated with the individual constraints. Consistency Φ1 is stronger than or equal to (≥) consistency Φ2 iff any Φ1-consistent CSP is also Φ2consistent. Consistency Φ1 is strictly stronger than (>) Φ2 if Φ1 ≥ Φ2 but not vice versa. Consistency Φ1 is equivalent to (=) Φ2 if Φ1 ≥ Φ2 and Φ2 ≥ Φ1.

Here we consider symmetry as a property of the set of solutions. A solution symmetry [Rossi, Van Beek, and Walsh, 2006] is a solution-preserving permutation on assignments.

Symmetry breaking method m1 is stronger in nodes (resp. solutions) pruning than method m2, denoted by m1 ⪰n (resp. ⪰s) m2, when all the nodes (resp. solutions) pruned by m2 would also be pruned by m1. Symmetry breaking method m1 is strictly stronger in nodes (resp. solutions) pruning than method m2, denoted by m1 ≻n (resp. ≻s) m2, when m1 ⪰n (resp. ⪰s) m2 and m2 ̸⪰n (resp. ̸⪰s) m1. Note that ⪰n and ≻n imply ⪰s and ≻s respectively.

LexLeader [Crawford et al., 1996] adds one lexicographical ordering constraint [Frisch et al., 2002], ≤lex, per variable symmetry according to a fixed variable order.

Given the set of all symmetries to a CSP, symmetry breaking during search (SBDS) [Gent and Smith, 2000] adds conditional constraints for each symmetry upon backtracking. Consider a node P0 in the search tree with partial assignment A, branching variable x and value v. After backtracking from the node P0 ∪ {x = v}, for each solution symmetry g, SBDS adds the following conditional constraint to the node P0 ∪ {x ̸= v}:

meaning that once A ∧ (x = v) has been searched, its symmetric partial assignment (A ∧ (x = v))g for any g in the symmetry set under this subtree should not be searched at all. Note that the added constraint is a nogood.

Weak-Nogood Consistency

The watched literal technique [Moskewicz et al., 2001] is extended to implementing propagators for CSPs [Gent, Jefferson, and Miguel, 2006]. When an assignment (as a literal) is watched, the satisfaction of the assignment triggers the propagator in the AC-3 like algorithm. To enforce GAC for a nogood, only two assignments that are not satisfied need to be watched [Moskewicz et al., 2001]. Upon each backtracking, SBDS would add new nogoods into the constraint store. Maintaining such a large set of nogoods is costly since the triggers to their propagators are often fruitless. We propose to watch only one assignment to trade pruning power for efficiency by enforcing nogood with a weaker consistency.

A nogood (xs0 = vs0 ) ∧ . . . ∧ (xsm = vsm ) ⇒ (xk ̸= vk) is weak-nogood consistent (WNC) iff (∃i ∈ [0,m], (vsi ̸∈ D(xsi ) ∨ (vsi ∈ D(xsi ) ∧ |D(xsi )| > 1))) ∨ ((∀i ∈ [0, m], D(xsi ) = {vsi }) ∧ vk ̸∈ D(xk)).

A nogood is WNC if either (1) one of the LHS assignments is not satisfied or (2) all LHS assignments are satisfied and its RHS assignment is falsified.

We now compare the consistency level of GAC and WNC.

Theorem 1. GAC>WNC on a nogood.

Proof. We first prove that GAC implies WNC. A nogood is GAC if either (a) it is true or (b) it has at least two unresolved assignments. For (a), either one of the LHS assignments is falsified, or all LHS assignments are satisfied and its RHS assignment is falsified. Both cases satisfy the two conditions of WNC respectively and the nogood is also WNC. For (b), one of the unresolved assignments must be in the LHS. Thus one of the LHS assignments is not satisfied and condition (1) of WNC is satisfied. The nogood is WNC.

To prove GAC is strictly stronger than WNC, consider the nogood ng ≡ (x1 = 1)∧(x2 = 1) ⇒ (x3 ̸= 1) with domains D(x1) = D(x3) = {1},D(x2) = {1, 2}. The nogood is WNC since (x2 = 1) is not satisfied yet but not GAC since 1 from D(x2) has no support.

WNC loses pruning opportunities in which an unresolved LHS assignment can be enforced to be true when all other assignments in this nogood are all satisfied. Experimental results confirm however that such cases happen not very often.

To enforce WNC for a symmetry breaking nogood, we propose a lazy propagator, LazyNgProp, in Algorithm 1. The propagator can end with two different outputs: ENTAILED or WNCed. A stores the current partial assignment. Without loss of generality, we assume that variables in A are in input order 〈x0, . . . , xn-1〉 for ease of explanation. We also assume that a propagator is immediately triggered once when it is first added to the constraint store.

Algorithm 1 LazyNgProp()

Require: A: current partial assignment g: symmetry x: variable of the watched LHS assignment v: value of the watched LHS assignment ˜x: variable of the RHS ˜ v: value of the RHS α = -1: position of the assignment in A whose symmetric assignment is being watched β: the length of the LHS 1: for each (xi = vi) ∈ A and i ∈ [α+1, β) do 2: (xi ′ = vi ′ ) = (xi = vi)g ; 3: if vi ′ ̸∈ D(xi ′ ) then return ENTAILED; 4: else 5: if |D(xi ′ )| > 1 then 6: x = xi ′ ; v = vi ′ ; 7: α = i; 8: watch x = v; 9: return WNCed; 10: prune ˜ v fromD(˜x); 11: return ENTAILED;

Upon each backtracking, we create a propagator for each generated symmetry breaking nogood and make available the symmetry g, the length of the LHS and the RHS ˜x ̸= ˜ v of the associated nogood to the propagator. The pointer α is initialized to -1 meaning that the propagator does not watch any assignment when it is initially triggered. The for-loop in lines 1-9 starts from the current watched assignment to look for the next unresolved assignment to watch. Once found, the nogood is WNC and the propagator can exit (line 9) with WNCed returned. If, however, any LHS assignment is found falsified, the nogood is entailed and can be removed from the constraint store (line 3, exit with ENTAILED). If no unresolved assignments are found, all LHS assignments are satisfied and pruning is effected using the RHS (line 10) and again the nogood is entailed (line 11).

As can be seen in Algorithm 1, LazyNgProp watches only one assignment at a time. Symmetric assignments in the LHS of nogoods are also only computed on demand but not eagerly. In addition, the current partial assignment A can be shared by all propagators and backtrackable.

Theorem 2. LazyNgProp enforces WNC for a nogood.

Proof. If the propagator for a nogood ng returns WNCed at line 9, it has an unresolved assignment x = v being watched. From line 1, we know x = v is in the LHS of ng. Thus condition (1) of WNC is satisfied and ng is WNC. The propagator can return ENTAILED at line 3 or 11. In line 3, condition (1) of WNC is satisfied. In line 11, condition (2) is satisfied since all LHS assignments are satisfied and the RHS assignment is falsified. Again, ng is WNC.

Theorem 3. Given a CSP P = (X, D, C) with |X| = n. The space complexity of LazyNgProp for a nogood is O(1), and the time complexity is O(n).

Proof. LazyNgProp records only the symmetry (just a name or pointer), the LHS watched assignment, the RHS assignment, the LHS watched assignment's corresponding assignment position and the length of the LHS. The total space complexity is O(1). The maximum number of assignments in each nogood is n and we scan the assignments only once in LazyNgProp. The time complexity is O(n).

Theorem 4. Given a CSP P = (X, D, C) with |X| = n and a set of symmetries G. The total space and time complexity of SBDS utilizing LazyNgProp to enforce WNC on all nogoods at each search tree node is O(|G| ∑n-1 i=0 (|D(xi)| - 1) + n) and O(n|G| ∑n-1 i=0 (|D(xi)| - 1)) respectively.

Proof. The total number of nogoods in SBDS is at most |G| ∑n-1 i=0 (|D(xi)| - 1) and the length of a partial assignment can be at most n. While each filtering algorithm has O(1) space complexity, the total space complexity is O(|G| ∑n-1 i=0 (|D(xi)| - 1) + n).

LazyNgProp scans the LHS assignments incrementally during the AC3-like algorithm by maintaining α. The maximum number of such assignments is n. Thus the total time complexity for LazyNgProp to handle all the nogoods in SBDS is O(n|G| ∑n-1 i=0 (|D(xi)| - 1)).

GAC vs WNC in SBDS and Its Variants

In addition to ReSBDS and LReSBDS, Partial SBDS (ParSBDS) [Flener et al., 2002] is SBDS but deals with only a given subset of all symmetries. LDSB [Mears et al., 2013] is a further development of shortcut SBDS [Gent and Smith, 2000] which handles only active symmetries and their compositions. WNC can also be used in ParSBDS, LDSB, ReSBDS and LReSBDS since they generate symmetry breaking nogoods in a similar fashion.

In this section, we compare the node and solution pruning power between GAC and WNC in SBDS and its variants respectively. We denote the methods enforcing WNC with subscript WNC, and those enforcing GAC without a subscript.

In the following, we assume all methods use the same static variable and value ordering heuristics.

Theorem 5. SBDS =s SBDSWNC and SBDS ≻n SBDSWNC.

Proof. Suppose SBDSWNC leaves two symmetric solutions s1 and s2. Suppose further P is their deepest common ancestor node and s1 is searched earlier than s2. Upon backtracking from the left subtree to the right at P, the nogood which prunes the symmetric solution of s1 must be posted. Since LazyNgProp can only postpone some pruning opportunities to deeper nodes, s2 is pruned by the nogood eventually. Thus SBDSWNC has the same solution pruning power as SBDS.

As the entire symmetry group is posted, SBDS would never leave any symmetric subtrees. While SBDSWNC can postpone the pruning opportunity into deeper nodes, it leaves some symmetric parts and prunes less nodes. SBDSWNC can backtrack more and generate more nogoods, but these nogoods break no new symmetries (since all symmetries are broken in SBDS). Thus the search tree of SBDSWNC subsumes that of SBDS.

In partial symmetry breaking, such as ParSBDS and ReSBDS, only a subset of all symmetries is posted. Since WNC is weaker, there are symmetric subtrees that are pruned by GAC but not by WNC. In turn, WNC searches and also backtracks more, thus sometimes posting more nogoods than GAC. Such nogoods can potentially break composition symmetries that are not posted. As a result, it is difficult to compare theoretically the strength of GAC and WNC on ParSBDS, ReSBDS and LReSBDS respectively, but is interesting future work.

Theorem 6. WNC = GAC for unconditional nogoods.

Proof. Unconditional nogoods are simply disequality constraints. WNC and GAC handle them equally.

Theorem 7. LDSB =n (resp. =s) LDSBWNC.

Proof. All symmetry breaking nogoods in LDSB are unconditional since LDSB handles only active symmetries and their compositions. Results follow directly from Theorem 6.

Generalized Weak-incNGs Consistency

Lee and Zhu (2014b) show that the set of symmetry breaking nogoods added by SBDS and its variants for one symmetry at a search node are increasing nogoods. They also give the incNGs global constraint and a filtering algorithm which is stronger than GAC on each nogood. Now we propose a weaker consistency for the incNGs constraint.

A set of directed nogoods Λ is increasing [Lee and Zhu, 2014b] if the nogoods can form a sequence 〈ng0, . . . , ngt〉 where ngi ≡ (Ai ⇒ xki ̸= vki ) such that (i) for any i ∈ [1, t], Ai-1 ⊆ Ai and (ii) no nogoods are implied by another. A nogood ngj in Λ is lower than nogood ngi iff j < i, and ngi is higher than ngj.

A set of increasing nogoods Λ = 〈ng0, . . . , ngt〉 where ngi ≡ (Ai ⇒ xki ̸= vki ) is generalized weak-incNGs consistent (GWIC) iff (∃i ∈ [0, t], ∃(xsi = vsi ) ∈ Ai, ((vsi ̸∈ D(xsi ) ∨ (vsi ∈ D(xsi ) ∧ |D(xsi )| > 1))) ∧ (∀j < i, (∀(xsj = vsj ) ∈ Aj , D(xsj ) = {vsj })∧vkj ̸∈ D(xkj )))∨ ((∀i ∈ [0, t], (∀(xsi = vsi ) ∈ Ai,D(xsi ) = {vsi }) ∧ vki ̸∈ D(xki )). Thus, Λ is GWIC if either (1) one of the LHS assignments of nogood ngi is not satisfied and for each ngj lower than ngi, ngj's LHS assignments are satisfied and its RHS assignment is falsified or (2) the LHS assignments of all nogoods are satisfied and all RHS assignments are falsified. GWIC has the following theorems.

Theorem 8. Given increasing nogoods Λ = 〈ng0, . . . , ngt〉, GWIC on Λ is equivalent to WNC on each ngk, k ∈ [0, t].

Proof. We first prove that if Λ is GWIC, all individual nogoods are WNC. One case is that there exists ngi such that Λ satisfies condition (1) of GWIC. Now all nogoods lower than ngi satisfy condition (2) of WNC, and the remaining nogoods whose LHSs subsume lhs(ngi) satisfy condition (1) of WNC. Thus all nogoods are WNC. Another case is that Λ satisfies condition (2) of GWIC, which implies that all nogoods satisfy condition (2) of WNC.

Secondly, we prove if all individual nogoods are WNC, Λ is GWIC. Suppose we can find a nogood ngj which is the lowest nogood in Λ and satisfies condition (1) of WNC. All nogoods lower than ngj must satisfy condition (2) of WNC since all their LHS assignments must be satisfied. Thus condition (1) of GWIC is satisfied. If we cannot find such an ngj , all nogoods satisfy condition (2) of WNC. Now condition (2) of GWIC is satisfied. Therefore, Λ is GWIC iff all individual nogoods are WNC.

Theorem 9. GAC > GWIC on an incNGs constraint.

Proof. Given increasing nogoods Λ = 〈ng0, . . . , ngt〉. Lee and Zhu (2014b) show that GAC on Λ is strictly stronger than GAC on individual nogoods (ngi), which is strictly stronger than WNC on the individual nogoods (ngi) by Theorem 1. In addition, WNC on the individual nogoods (ngi) is equivalent to GWIC on Λ by Theorem 8. Result follows.

A sequence of increasing nogoods Λ = 〈ng0, . . . , ngt〉 for a symmetry g can be encoded compactly. The increasing property guarantees that lhs(ngj) ⊆ lhs(ngi) for all j < i ≤ t. Thus the LHS assignments of all nogoods are available in lhs(ngt). Suppose Λ is added at an ancestor node P ′ of P and A is the partial assignment of P. We must have lhs(ngt) ⊆ Ag . Therefore, we can always construct (by applying symmetry transformation) lhs(ngt) from the partial assignment at any descendant node of P ′ . We also collect all the backtracking assignments (refer to Section 2) from root to a search node, and call it B. Each backtracking assignment is also associated with its depth, which is the length of the partial assignment associated with the node where backtracking takes place. We can construct (by applying symmetry transformation) rhs(ngk) for k ∈ [0, t] from the backtracking assignments in B. Using A and B together, we can reconstruct all nogoods in Λ using symmetry g.

Section 3 shows that watching one unresolved assignment in the LHS is enough to enforce WNC on a nogood. An important consequence of lhs(ngj) ⊆ lhs(ngi) for all j < i ≤ t in Λ is that watching an assignment in lhs(ng0) implies watching the same assignment in lhs(ng1), . . . , lhs(ngt). In general, when we watch an assignment that first appears only in lhs(ngi), we are also watching the same assignment in lhs(ngi+1), . . . , lhs(ngt). Thus, we can watch only one unresolved assignment for our lazy propagator for Λ. We scan the symmetric assignments of the current partial assignment at each search node to find the first unresolved assignment to watch. During scanning, when we encounter an assignment Γ, there are three possibilities. (a) Γ is satisfied. We should make use of B to look for all nogoods with a true LHS, and enforce the RHSs of all discovered nogoods to be true to effect prunings. Then we continue our previous scanning to the next assignment. (b) Γ is falsified. We can stop scanning since Λ is entailed. (c) Γ is unresolved. We stop scanning and watch Γ, since Λ is now GWIC.

The incNGs constraint grows since nogoods are added dynamically upon backtracking. It can happen that, at one search node, all symmetric equivalents of those in the current assignments A are true. There are no assignments to watch. In such a case, the propagator should still be triggered upon backtracking (when B is updated), which is when a new nogood is added to the propagator.

We now present our lazy propagator, LazyincNGsProp, for the incNGs constraint as shown in Algorithm 2. The propagator can return two different results: ENTAILED or GWICed. A stores the current partial assignment. B stores all backtracking assignments and their depth as a pair from root up to the current search node. If we view A and B as arrays, their indices start from 0. Without loss of generality, we assume that variables in A are in input order 〈x0, . . . , xn-1〉.

Algorithm 2 LazyincNGsProp()

Require:

• A: current partial assignment

B: all backtracking assignments and their depth from root up to the current node g: symmetry x = ⊥: variable of the watched LHS assignment v = ⊥: value of the watched LHS assignment α = -1: position of the assignment in A whose symmetric assignment is being watched β = 0: position of the first assignment in B whose symmetric assignment has not been enforced by this constraint 1: if α = |A| -1 then 2: pruneB(α + 1); 3: else 4: for each (xi = vi) ∈ A and i ∈ [α + 1, |A|) do 5: (xi ′ = vi ′ ) = (xi = vi)g ; 6: if vi ′ ̸∈ D(xi ′ ) then return ENTAILED; 7: else 8: if |D(xi ′ )| > 1 then 9: x = xi ′ ; v = vi ′ ; 10: α = i; 11: watch x = v; 12: return GWICed; 13: pruneB(i + 1); 14: x = ⊥; v = ⊥; α = |A| -1; 15: return GWICed;

Algorithm 3 pruneB(k)

• 1: for each (xj = vj, dj) ∈ B and j ≥ β and dj ≤ k do
• 2: (xj ′ = vj ′ ) = (xj = vj)g ; 3: prune vj ′ fromD(xj ′ ); 4: β = j +1;

For each given symmetry g, an incNGs global constraint would be posted at the root node. We create a propagator LazyincNGsProp and make available the symmetry g to the propagator. This propagator is triggered by the watched assignment x = v. If there are no assignments to watch, it is triggered when B is updated. The pointer α always points to the watched assignment, and is initialized to -1 to watch nothing. If the propagator is triggered by B's update, and no assignments are watched and A is not updated from the last propagation (line 1), this means the LHSs of all increasing nogoods are satisfied and pruneB (line 2) is called to prune all symmetric equivalents of the backtracking assignments in B starting from pointer β whose corresponding nogoods are not enforced yet. After doing that, the constraint is GWIC and the propagator can exit (line 15). If the propagator is triggered by the watched assignment x = v or A's update, the for-loop in lines 4-13 looks for the next unresolved assignment to watch as in Algorithm 1. The only thing to take care is if an assignment in the LHS is satisfied, pruneB (line 13) is called to prune all symmetric equivalents of the backtracking assignments in B starting from pointer β whose LHSs are satisfied and corresponding nogoods are not enforced yet.

As can be seen in Algorithm 2, LazyincNGsProp watches only one assignment at a time, and also gets triggered when B is updated. All symmetric assignments are computed on demand but not eagerly. Note that A and B should be backtrackable and can be shared by all propagators.

Theorem 10. LazyincNGsProp enforces GWIC for an incNGs global constraint.

Proof. The propagator returns GWICed at line 12 or 15. Line 12 is reached when there is an unresolved assignment x = v being watched. Now all nogoods whose LHSs do not contain x = v are true since their LHS assignments are satisfied and their RHSs are enforced at line 2 or 13 by pruneB. For all nogoods containing x = v, x = v must be in their LHSs according to line 4. Thus condition (1) of GWIC is satisfied and the increasing nogoods is GWIC. Line 15 means all LHS assignments of current nogoods are satisfied and all RHS assignments are falsified. Now all nogoods are true. Condition (2) of GWIC is satisfied and this increasing nogoods is GWIC. If the propagator returns ENTAILED at line 6, there exists an ngi such that its LHS contains x′i = v′i and all lower nogoods have their LHS assignments satisfied and RHS assignment falsified. Thus, condition (1) of GWIC is satisfied and this increasing nogoods is GWIC.

Theorem 11. Given a CSP P = (X,D,C) with |X| = n. The space complexity of LazyincNGsProp for an incNGs global constraint is O(1), and the time complexity is O(∑n-1 i=0 |D(xi)| -n/2).

Proof. LazyincNGsProp needs to record the symmetry, the LHS watched assignment, two pointers α and β. The total space complexity is O(1). There are at most n + ∑n-1 i=0 (|D(xi)| - 1) number of symmetric assignments to generate and ∑n-1 i=0 (|D(xi)| - 1) to prune. The time complexity is O(∑n-1 i=0 |D(xi)| -n/2).

Experimental Results

This section gives three experiments, all with matrix symmetries (variable symmetries). Our method works for arbitrary symmetries, but better as the number of symmetry grows. Matrix symmetries are common in many CSP models and their numbers are exponential with problem size. We first solve the benchmarks using the efficient and widely used static method Doublelex [Flener et al., 2002], and also LexLeader to break a much larger subset of symmetries. We then report the results of two dynamic methods ParSBDS and LReSBDS. Each dynamic method would be implemented with the four propagators: GAC on each nogood (GAC), the filtering algorithm of incNGs given by Lee and Zhu [2014b] (incNGs), WNC on each nogood (WNC) and GWIC on each incNGs constraint (GWIC).

We also did extra experiments to find the best subset of matrix symmetries for each method. ParSBDS is given any two rows or columns being permutable and the Cartesian products of these two subsets. LReSBDS and LexLeader can break the entire row symmetries and column symmetries by only posting adjacent rows or columns being permutable with the input order variable heuristic [Lee and Zhu, 2014a]. We thus only post adjacent rows or columns being permutable and the Cartesian products of any two rows or columns being permutable to LReSBDS and LexLeader. LDSB and ReSBDS are discarded in the comparison since LReSBDS is substantially more efficient [Lee and Zhu, 2014a; 2014b] than these two methods. All experiments are conducted using Gecode Solver 4.2.0 on Xeon E5620 2.4GHz processors with 7GB.

Due to the many columns, each table is split into three rows. The first column always gives the instance parameters. In addition, #s denotes the number of solutions, #f denotes the number of failures and t denotes the runtimes. Since WNC and GWIC have the same pruning power, we show their solutions and failures together and use tW and tG to denote the runtime of WNC and GWIC respectively. The search time out limit is 1 hour. An entry with the symbol " - " indicates that memory is exhausted. The best results are highlighted in bold. Unless otherwise specified, search is defaulted to input variable order and minimum value order.

Error Correcting Code-Lee Distance (ECCLD)

Each ECCLD instance is parameterized by (n, c, b). We use the same model by Lee and Zhu (2014a).

Table 1 shows the results for ECCLD. ParSBDSWNC is 1.35 times faster than ParSBDSGAC on average. LReSBDSWNC does not perform well since the number of extra nogoods added by LReSBDS to prune extra composition symmetries is big and the symmetries are broken late. ParSBDSGWIC and LReSBDSGWIC run 1.13 and 1.15 times faster than ParSBDSincNGs and LReSBDSincNGs on average respectively. The improvement is not that much due to the small number of given symmetries. When we compare the number of failures for ParSBDS and LReSBDS, WNC and GWIC increase only slightly the search tree size. This shows our weaker consistencies lose few pruning opportunities. LReSBDSGWIC performs the best and runs 1.50 and 2.67 times faster than LexLeader and DoubleLex on average respectively. ParSBDSGWIC performs slightly slower than LReSBDSGWIC due to its bigger search tree size and more symmetries to handle. Thus, laziness can save us time comparing with other symmetry breaking methods.

Cover Array Problem (CA)

CA instances are parameterized by (t, k, g, b) We use the same model by Lee and Zhu (2014b).

Table 2 shows the results for CA. ParSBDSWNC is 1.61 times faster than ParSBDSGAC on average. LReSBDSWNC still does not perform well. ParSBDSGWIC and LReSBDSGWIC run 1.62 and 1.75 times faster than ParSBDSincNGs and LReSBDSincNGs on average respectively. For LReSBDS, WNC and GWIC only slightly increase the search tree size. LReSBDSGWIC performs the best and runs 1.67 and 1.82 times faster than LexLeader and DoubleLex on average respectively. This again shows the advantage of our lazy incNGs propagator.

Balanced Incomplete Block Design (BIBD)

A BIBD instance can be determined by its parameters (v, k, λ). We use the same model by Lee and Zhu (2014b). The value ordering is maximum value ordering and DoubleLex orders rows and columns decreasingly.

Table 3 shows the results for BIBD. ParSBDSWNC and LReSBDSWNC run 16.67 and 4.07 times faster than ParSBDSGAC and LReSBDSGAC on average respectively. One reason for the improvement is the reduction of overhead. The other reason for the good efficiency of ParSBDSWNC is that it prunes symmetries late and can break much more composition symmetries. ParSBDSGWIC and LReSBDSGWIC run 1.90 and 1.34 times faster than ParSBDSincNGs and LReSBDSincNGs on average respectively. The search tree size by enforcing WNC and GWIC still does not increase too much more than GAC. LReSBDSGWIC performs the best and runs 7.90 and 1.12 times faster than LexLeader and DoubleLex on average respectively. From the above, we can conclude that laziness can save much time and memory comparing with other symmetry breaking methods.

Conclusion and Future Work

Our contributions are four fold. First, we propose WNC for nogoods and give a lazy propagator to symmetry breaking nogoods added by SBDS-based methods. We give also the space and time complexities of the WNC lazy propagator. Second, we propose GWIC for incNGs global constraint and also give a lazy propagator and its space and time complexities. Third, we prove that GWIC on a conjunction is equivalent to WNC on the individual nogoods. Fourth, we use experiments to show the lazy methods' pruning loss is small while the gain in efficiency is worthwhile.

The improvement from the original incNGs to the lazy version is not as good as that from GAC on nogoods to WNC on nogoods. That is because the global constraint version must be incremental in nature to cater for the addition of new nogoods, and is triggered every time when new nogoods are generated, which is often. So it is not as lazy as we hope it to be. This points to new research opportunities to investigate how best to incorporate laziness into incNGs constraints.

Other possibilities include investigating symmetric nogoods collected from restarts [Lecoutre and Tabary, 2011] and detecting symmetry dynamically.