Constraint satisfaction · Part 1

A constraint satisfaction problem (CSP) describes choices and the rules those choices must obey. We first build a model, then compare two ways to use it: search through assignments, and propagation through domains.

The running example uses variables X₁, X₂ and X₃, each initially allowed values 0, 1 and 2. Its rules are X₁ < 2, X₂ > 0 and X₃ < X₁. We will use the same example throughout the lecture so that the behavior of each algorithm can be compared directly.

By the end, distinguish a complete solution from a partially assigned context and from a collection of pruned domains. These are different objects, and the algorithms return different kinds of answers.

In a timetable model, each course has a variable representing its time slot. The domain lists the slots that the course may use. A constraint between courses that share students or a lecturer prevents simultaneous teaching. Room choices can be modeled with additional variables and capacity or availability rules.

The same modeling pattern applies to robot planning: variables may describe task times or locations, while constraints express precedence, deadlines and reachable locations. In scene understanding, variables can be labels for image regions, with rules describing compatible spatial relationships.

A hard constraint decides whether an assignment is legal. A preference ranks legal assignments, for example by minimizing timetable gaps. Preferences require an objective, weights or a soft-constraint model; they are not automatically equivalent to hard true/false rules.

A variable represents one decision. Its domain is the set of values permitted for that decision. The notation dom(X) names the domain of variable X, and X ∈ dom(X) says that the chosen value must belong to this set. A binary decision might have domain {0,1}; a color choice might have domain {red,green,blue}.

If there are n variables and each has d choices, there are dⁿ total assignments before checking constraints. This follows from choosing a value independently at each position: d × d × … × d, with n factors. For the course example, n=3 and d=3, giving 27 candidates. Ten binary variables give 2¹⁰=1024 candidates.

If the domain sizes differ, multiply the actual sizes. Two variables with three and two choices give 3×2=6 candidates. A compact list of variables and domains may describe a very large search space; the small description does not imply an easy problem.

Before checking constraints, the assignment space is the Cartesian product of the variable domains: one choice for X₁, one for X₂, and so on. Its size is the product of the domain sizes. This counts candidates, not necessarily solutions.

The symbol ∏ denotes multiplication over an index. In ∏ᵢ₌₁ⁿ |dom(Xᵢ)|, i runs from 1 to n, n is the number of variables, and |dom(Xᵢ)| is the number of values available to Xᵢ. When all sizes equal d, this is dⁿ.

For dom(X₁)={0,1,2} and dom(X₂)={“a”,“b”}, the six tuples are (0,“a”), (0,“b”), (1,“a”), (1,“b”), (2,“a”) and (2,“b”). The string values “a” and “b” are ordinary domain values; they are not names for assignment objects.

An atomic assignment gives one variable a value, such as X₁=1. A partial assignment, also called a context, combines such pairs for some of the variables. We use A for a context; the remaining variables have not been decided yet.

A total assignment gives a value to every variable. We use a for a total assignment. The tuple (1,2,0) is shorthand for X₁=1, X₂=2 and X₃=0, in that fixed variable order. A question mark in a teaching diagram represents an unassigned variable; it is not a new value in the domain.

Completeness of an assignment is separate from correctness. The complete tuple (2,1,0) uses allowed domain values but violates X₁ < 2. The tuple (1,2,0) satisfies all three course rules and is a solution.

In the course’s broad definition, a partial assignment may select any subset of variables, including the full set. An assignment with some variables still missing is more specifically a proper partial assignment. Atomic and total assignments are therefore special cases of partial assignments.

An atomic assignment is one pair X=x, with x∈dom(X). A partial assignment is a collection of such pairs that assigns at most one value to each selected variable. Its selected-variable set is a subset of the problem’s variable set. A total assignment is the special case in which every variable is selected. Thus atomic and total assignments are also partial assignments in the broad mathematical sense.

For an assignment a and a set S of assigned variables, a[S] is the restriction to S: retain exactly the pairs for variables in S. For a={X₁=1,X₂=2,X₃=0} and S={X₁,X₃}, this gives a[S]={X₁=1,X₃=0}. The variable X₂ disappears from the restricted assignment; its original value is not changed.

The course also writes a[X] for the current value of a single variable X. Here a[X₂]=2 is a value, while a[{X₂}]={X₂=2} is a one-pair assignment. The braces distinguish a variable lookup from a restriction to a variable set.

Restriction lets a constraint inspect exactly the variables in its scope. The expression a[scope(c)] will therefore be the input to the evaluation function on the next slides.

A constraint has a scope: the set of variables whose values it needs. Unary, binary and ternary constraints use one, two and three variables respectively. The ternary sum on this slide is an illustration of scope; it is not one of the three rules in the running course CSP.

A fully assigned scope allows ordinary true/false evaluation. With X₁=1 and X₂=2, the unary rule X₁ < 2 is true, but X₃ < X₁ is pending because X₃ has no value. If X₃=0 is added, the binary rule is true and X₁+X₂=X₃ is false.

In the reference notation, ε is the evaluation function: it returns 1 for a satisfied constraint and 0 for a violated constraint when all variables in the scope have values. “Pending” is the lab’s label for an incomplete scope, not a third mathematical truth value. Plain backtracking tests complete scopes; stronger propagation may reason about possible values before they are assigned.

For a named rule c, its scope is written scope(c), and its arity is |scope(c)|. The bars |S| denote the size of a set S. For c: X₁+X₂=X₃, scope(c)={X₁,X₂,X₃} and the arity is 3.

A constraint c is a condition on its scope, the variables it uses. Its arity is |scope(c)|, the number of distinct variables in that scope. Unary, binary and ternary constraints have arities one, two and three.

The evaluation function ε(a,c) returns 1 when the supplied scoped assignment satisfies c, and 0 when it violates c. Its assignment argument must provide all variables in scope(c). If a larger assignment is available, first restrict it and write ε(a[scope(c)],c). We consistently place the assignment first and the constraint second.

For c given by X₃<X₁, the pair {X₁=1,X₃=0} evaluates to 1, whereas {X₁=0,X₃=1} evaluates to 0. With only X₁ assigned, this evaluation cannot yet be performed: X₃ is missing.

The lab describes an incomplete scope as pending. That is a statement about whether we have enough input, not a third numerical output of ε. In particular, an incomplete assignment must not automatically receive evaluation 0.

Logical connectives combine statements into a larger condition. The symbol ∧ means AND, also called conjunction: the combined condition is true only if every part is true. The symbol ∨ means OR, also called disjunction: the combined condition is true if at least one part is true. This OR is inclusive, so it is also true when both parts are true.

The course CSP has variables X₁,X₂,X₃ with domains {0,1,2}. Its three constraints must hold together: (X₁ < 2) ∧ (X₂ > 0) ∧ (X₃ < X₁). Parentheses group the individual statements; ∧ connects them. Writing the constraints as a comma-separated set or list is shorthand for requiring all of them, rather than choosing just one.

Take the total assignment (1,0,0), in order X₁,X₂,X₃. The three course rules give true, false, true. Their conjunction is therefore false: this candidate is not a solution, even though two rules hold.

For a separate OR illustration, consider (X₁=1) ∨ (X₂=2). At (1,0,0), the left statement is true and the right is false, so the OR is true. At (1,2,0), both are true and the OR is still true. At (0,0,0), both are false and the OR is false. This example is not an additional constraint in the course CSP; satisfying it alone does not establish a course solution.

A CSP takes the conjunction of all its constraints. Within one constraint, AND and OR may be combined to describe the permitted alternatives. For example, the course solutions can be written as (X₁=1) ∧ ((X₂=1) ∨ (X₂=2)) ∧ (X₃=0). The outer AND fixes X₁ and X₃; the grouped OR permits either remaining X₂ value. Without parentheses, AND is conventionally read before OR; explicit grouping makes the intended rule easier to see.

The truth table uses r and s to stand for statements, not CSP variables. It assumes their inputs are available so each statement has a true/false value. With a partial context, a rule whose scope is incomplete remains pending, as in the evaluation examples. The logical symbols do not turn a missing value into false.

Do not confuse ∧ and ∨, which combine statements, with ∩ and ∪, which combine sets. For example, X₂∈{1,2} describes a choice from a set and is equivalent to (X₂=1) ∨ (X₂=2); it does not assign the set {1,2} as X₂’s value.

A constraint satisfaction problem is the tuple P=(𝓧,dom,𝓒). The set 𝓧={X₁,…,Xₙ} contains n variables. The function dom associates each variable X with an allowed-value set dom(X). The set 𝓒={c₁,…,cₘ} contains m constraints. The indices i and j can select a variable Xᵢ or a constraint cⱼ.

The notation X↦dom(X) describes the domain function’s action. dom is the mapping; dom(X) is one set returned by it. For example, dom(X₁)={0,1,2}. A constraint’s scope must contain only problem variables: scope(c)⊆𝓧.

A candidate assignment must use legal domain values. Being total only says that all variables have values; it does not yet say that those values satisfy the constraints. The formal solution test adds that second requirement.

These packs use finite domains when claiming exhaustive termination or enumerating all solutions. A model may otherwise admit infinite domains, for which the finite search guarantees do not automatically apply.

We write P=(𝓧,dom,𝓒). P names the whole problem, 𝓧 is its set of variables, dom associates each variable with its allowed values, and 𝓒 is its set of constraints. In dom(Xᵢ), i is a variable index: here i is 1, 2 or 3.

The course problem uses 𝓧={X₁,X₂,X₃}, dom(Xᵢ)={0,1,2}, and three constraints: X₁ < 2, X₂ > 0 and X₃ < X₁. A solution must choose domain values and satisfy every constraint at once.

The first rule restricts X₁ to 0 or 1. If X₁=0, no allowed X₃ is smaller. Therefore X₁=1 and X₃=0. The second rule leaves X₂=1 or X₂=2. The two solutions are consequently (1,1,0) and (1,2,0). We can either find one solution or enumerate all solutions; the stopping rule must match that goal.

Written as one condition, the three course constraints are (X₁ < 2) ∧ (X₂ > 0) ∧ (X₃ < X₁). Their AND requires all three. Equivalently, the complete solution set is described by (X₁=1) ∧ ((X₂=1) ∨ (X₂=2)) ∧ (X₃=0): X₁ is 1, X₃ is 0, and X₂ may be 1 or 2. The OR is inside the X₂ alternatives; it does not replace the AND across constraints.

A CSP solution is a total assignment a that uses a value from dom(X) for every X∈𝓧 and satisfies every c∈𝓒. The universal quantifier ∀ expresses “for every”; the membership sign ∈ expresses “belongs to”.

To read the formula, take each constraint c in turn. Compute scope(c), retain the corresponding pairs a[scope(c)], and evaluate ε on those pairs and c. Every result must be 1. The rule is an AND (∧) over the constraint set: all evaluations must be 1. It is not an OR (∨), which would only require one of them to be 1.

For the course candidate (1,1,0), the three evaluations are 1,1,1, so it is a solution. The tuple (2,1,0) uses allowed domain values but gives 0 for X₁<2, so it is not a solution even though its other two evaluations are 1.

The domain check is a separate premise. A tuple using an out-of-domain value is not a valid candidate even if some constraints happen to hold. Finding one such legal, all-ones assignment proves that the CSP is satisfiable; finding every one requires further exploration.

Begin with X₁=1 and the other two variables unassigned. X₁ < 2 is true. X₂ > 0 and X₃ < X₁ are pending because their scopes are incomplete. Pending does not mean violated.

Adding X₃=0 makes X₃ < X₁ true. Adding X₂=2 completes the assignment and makes X₂ > 0 true, so the lab reports a solution. Now change X₁ to 2: the assignment remains total, but the unary constraint fails.

Use the lab to separate three questions: is every variable assigned, which rules can be evaluated, and do all evaluated rules hold? These are the checks used in the recursive search that follows.

Generate-and-test enumerates total assignments and evaluates all constraints for each one. A candidate is a solution only when every rule holds. To find all solutions, continue through the entire Cartesian product of domains. To find one solution, stop on the first success.

This method is simple and complete for finite domains, but it can do unnecessary work. With fifteen variables and four choices each, there are over one billion candidates before applying the rules.

In the course example, all nine assignments beginning with X₁=2 fail the same unary rule. Generate-and-test may complete and reject them separately. Backtracking can recognize that failure once and discard the whole branch.

Backtracking explores a tree of partial assignments. The root is the empty context; each edge adds one variable–value pair. A node is rejected as soon as a constraint with a complete scope is false. Descendants inherit that violation, so none can be a solution.

For X₁=2, the rule X₁ < 2 is immediately false, and the nine combinations of X₂ and X₃ are skipped. For X₁=0, the unary rule is true and X₃ < X₁ is pending. Plain backtracking continues until X₃ receives a value, at which point every allowed value fails. Propagation can detect this impossibility earlier.

Undoing a choice restores the previous context so another value can be tried. Depth-first search follows one branch at a time and then returns to alternatives. If all branches of a finite problem are explored, backtracking finds all solutions or proves there are none.

The DFS solver maintains a partial assignment A called the context. Write vars(A) for the variables that already have values. For example, A={X₁=1,X₃=0} has vars(A)={X₁,X₃}.

The course’s notation c≡A means that c can be evaluated in A. Formally, scope(c)⊆vars(A). The subset relation ⊆ allows equality: having exactly the needed variables is enough. This use of ≡ denotes evaluability, not truth, logical equivalence or equality of the two objects.

In a separate illustrative rule c: X₁=X₃, the context {X₁=1,X₃=0} supplies the whole scope, so c≡A holds; the rule itself is false and ε(A[scope(c)],c)=0. A rule using the unassigned X₂ is not evaluable in that context.

The eligible set 𝓒ₑ={c∈𝓒 | c≡A} collects all rules that can currently be tested. DFS first rejects the context if any of those evaluations is 0. If all are 1, their truth cannot be undone by assigning previously unassigned variables, so the recursive call may omit those checked rules.

This is the course DFS solver with one consistent evaluation convention: ε(assignment,constraint). The inputs 𝓧 and 𝓒 shrink during recursion; A grows. Initially they contain all problem variables and constraints, with A=∅, the empty context.

Compute 𝓒ₑ, the constraints whose scopes are assigned. If any evaluates to 0, return ∅, the empty solution set. If no variable remains and no checked rule failed, return {A}, a set containing the completed assignment. These two return values are not interchangeable.

Otherwise select X and explore every x∈dom(X). The set difference 𝓧∖{X} removes the variable just assigned. The difference 𝓒∖𝓒ₑ removes rules already checked true. The union A∪{X=x} extends the context because X was previously unassigned. Each branch uses an independent extension, or the implementation must undo it afterward.

The solution set s begins empty and is enlarged by union with each recursive result. Exploring all values therefore collects all solutions. Retesting already true constraints, as the lab’s engine may do for display, is equivalent but can perform redundant checks.

The interactive tree preserves the course example and its variable order X₁, X₂, X₃. A node contains the partial assignment reached so far; its rule results explain whether the solver continues, prunes, or records a solution. Hovering or focusing a node exposes these details.

Use Step to follow the traversal. On a failed node, compare the scope of the violated rule with the variables already assigned. On a solution node, check that all three values are present and all rules hold.

The solver continues after the first solution because this lab enumerates all solutions. Reversing value order changes the traversal and the order in which the two solutions appear, but not the solution set.

Variable ordering chooses which unassigned variable to consider next. Minimum remaining values (MRV) selects a variable with the smallest current domain, aiming to expose a failure with fewer alternatives. If two variables tie, a degree heuristic can favor the variable involved in more constraints on other unassigned variables.

Value ordering chooses which value to try first. A least-constraining value leaves the most options for other variables. With A≠B, dom(A)={1,2} and dom(B)={1,3}, trying A=1 removes B=1, whereas A=2 removes neither B value. Trying 2 first therefore preserves more flexibility.

These heuristics can reduce work or bring a first solution forward, but they do not delete legal solutions. When all alternatives are eventually explored, the answer set is unchanged. The course DFS lab uses a fixed variable order to keep its traversal easy to follow.

DFS can be inefficient in some cases because it may rediscover the same failure for several choices of another variable. This motivates the transition in the original course’s §2.3.3: rather than waiting for each complete rule scope to be assigned, reason about which values still have any chance of satisfying the rule.

Consider two variables A and B with dom(A)=dom(B)={1,2,3,4} and the constraint A<B. These rename the original section’s X₁ and X₂. Suppose ordinary DFS assigns A first and chooses A=4. Because B is still unassigned, this binary rule is not yet evaluable in the context. DFS then tries B=1, B=2, B=3 and B=4. The corresponding tests 4<1, 4<2, 4<3 and 4<4 all fail, so it rejects four completions of the same hopeless A choice.

A consistency algorithm reasons over the domains instead: is there any allowed B greater than 4? There is none, so 4 can be removed from dom(A) before branching on A. This single filtering step excludes every completion with A=4. It is safe because no solution could have used that value. The next slide also considers the other direction: B=1 has no smaller allowed A and can be deleted from dom(B).

More generally, consistency algorithms shrink domains by enforcing a stated local consistency property. A sound deletion removes a value only when it cannot participate in any satisfying combination for the checked constraint, thereby preserving every solution. The output is usually smaller domains, rather than a set of complete solution assignments. This adds reasoning to ordinary DFS; methods that already combine search with propagation perform such checks during search.

Constraint propagation repeats these deductions as domains change. Deleting a value can remove a partner needed by another variable, making an earlier check outdated. The propagation algorithm schedules the affected checks again. A consistency property describes what must hold; a consistency algorithm describes how to enforce it.

The following examples first make filtering visible, then introduce the constraint network, support, arc consistency and the generalized arc consistency (GAC) worklist. Unary consistency checks one variable’s values; binary arc consistency checks partner values; GAC handles constraints of any scope size. Here an arc is a variable–constraint pair. Because these are local checks, nonempty filtered domains need not establish that one assignment satisfies all constraints together. Part 2 adds domain splitting to explore unresolved choices systematically.

Propagation draws consequences from constraints and current domains before choosing a complete assignment. For A < B with both domains {1,2,3,4}, A=4 is impossible because no allowed B is larger. B=1 is impossible because no allowed A is smaller.

After removing those values, dom(A)={1,2,3} and dom(B)={2,3,4}. Every actual solution of this one-constraint problem is preserved: a deleted value could not participate in any satisfying pair.

Propagation can substantially reduce branching, but checking supports has a computational cost. Its usefulness depends on the constraints, their scope sizes and the domains. The pruned domains describe remaining possibilities; they do not assert that every combination of those values is a solution.

Terminology varies between sources: filtering the domain for a unary constraint is often called domain consistency. The illustrated A<B rule is binary; GAC generalizes the support test to constraints of any arity.

Generalized arc consistency (GAC) is the support requirement enforced by the GAC filtering algorithm. For each rule involving a variable, every retained value must have at least one satisfying combination of values for the other variables in that rule. This combination is a support, also called a witness.

Generalized means that the rule can involve any number of variables. A binary rule needs a partner value; a larger scope needs a jointly satisfying combination for all the other variables. A unary rule has no partners, so its own value must satisfy the rule.

The next sections give each idea a separate role: the network identifies which variable–rule pairs exist, the support example illustrates a witness, the formula defines arc consistency, and the worklist and pseudocode specify how to enforce it. The outcomes section explains what the filtered domains establish.

The consistency-algorithms section motivates filtering. A constraint network now makes that filtering systematic: its variable–constraint edges identify the support checks that GAC must perform. The next support example explains what one such check asks before the general arc-consistency formula is introduced.

A constraint network is bipartite: one set of nodes represents variables and the other represents constraints. A link joins variable X to constraint c exactly when X is in the scope of c. There are no variable–variable or constraint–constraint links in this representation.

In the course CSP, X₁ touches its unary rule and the binary rule X₃ < X₁. X₂ touches its unary rule, and X₃ touches the binary rule. A k-ary constraint has scope size k and therefore k incident links. Here k=1 for a unary rule and k=2 for the binary rule.

Propagation revises a variable with respect to a constraint along such a link. The work item (X,c) is often called an arc. Processing an arc does not remove the link from the CSP; it checks whether that variable’s remaining values have support for that rule.

The course defines a constraint network as G=(V,U,E₀). The variable vertices are V=𝓧; the constraint vertices are U=𝓒. The edge set E₀ is a subset of the Cartesian product V×U, the set of all pairs with one member from each vertex set.

An edge (X,c) belongs to E₀ exactly when X belongs to scope(c). Thus the graph is bipartite: every edge joins the variable side to the constraint side. It contains no edge within either side in this representation.

For the chain with variables A,B,C and constraints c₁:A<B and c₂:B<C, there are four edges: (A,c₁), (B,c₁), (B,c₂) and (C,c₂). Each binary rule has two incident edges. A k-ary rule has k such edges.

The course later reuses the letter E₀ for the GAC worklist. To keep the edge set distinct from the changing worklist, these slides call the worklist E₀. Initially E₀=E₀; later E₀ contains only checks still to be processed. The lab’s conflict score E₀(a) is another context-specific notation and is mapped to h(a) in Part 2.

E₀ is the complete, fixed set of network edges. The GAC algorithm starts its pending worklist E with a copy of E₀. Processing a pair removes it from E, not from the network.

A value x of variable X has support for constraint c if at least one combination of values for the other variables in c’s scope satisfies c together with X=x. All those partner values must come from their current domains. For a unary constraint there are no partner variables: the value itself either satisfies the rule or does not.

With A < B and dom(B)={1,2,3,4}, A=2 is supported by B=3 or B=4. B=1 and B=2 do not work with A=2, but those failures do not justify deleting A=2 while a good partner remains. A=4 has no support and can be removed.

Use the explorer to remove B=3 and B=4. A=2 then loses all support. Removing only one of them still leaves a witness. This is an existential test: for each value there must be some satisfying tuple, not a requirement that all tuples work.

Supports are relative to current domains and can disappear after other constraints prune partner values. This is why propagation must revisit earlier checks.

Given a constraint network G and a constraint c with scope(c)={X,Y₁,…,Yₖ}, the edge (X,c) is arc consistent if every allowed value x of X has at least one combination of values yᵢ from dom(Yᵢ) that satisfies c. X is the checked variable; the Yᵢ are its k partners in that rule. Lowercase letters denote values, and the rule has arity k+1.

Read the quantifiers in order: ∀x considers every allowed X value, ∃y₁,…,yₖ finds one allowed partner combination for that value, and ε(...,c)=1 requires that combination to satisfy c. Different x values may use different witnesses. Neither every partner combination nor one common witness for all x is required.

For A<B with both domains {1,2,3,4}, A=1 can use B=2, A=2 can use B=3, and A=3 can use B=4. A=4 has no larger B and is removed. Checking B against the same rule is a separate edge test: it removes B=1.

A network is generalized arc consistent when every variable–constraint edge passes this support test. For a unary rule, there are no partner variables; the checked value itself must satisfy the rule.

E is the set of pending variable–constraint checks, using the old material’s notation. E₀ names the initial complete edge set of the constraint network; begin a full GAC run with E←E₀. The old material uses E for both roles, whereas the subscript 0 here makes the fixed starting set explicit. Taking a pair out of E does not delete a constraint or network edge.

A work item (X,c) means to check the allowed values of variable X against constraint c. For c:A<B, the initial worklist is {(A,c),(B,c)}. Selecting (A,c) leaves {(B,c)} pending. E is a set, so adding a pair that is already pending does not duplicate it.

N_X, read “N subscript capital X”, contains the values retained during the current check against c. Capital X names the variable; lowercase x denotes a candidate value. The bar in the definition means “such that”. N_X is recomputed using the current partner domains for each selected pair. It is not a separate permanent domain.

The pseudocode uses c′ for another constraint in 𝓒 and Z for another variable. The prime in c′ labels a different rule; it is not a derivative. These names identify checks that may have lost a supporting value when dom(X) shrank.

The procedure GAC(dom,E) takes the current domain mapping and a set of pending checks, and returns the pruned domain mapping. The variables 𝓧 and constraints 𝓒 stay fixed. This is shorthand for the old material’s GAC(𝓧,𝓒,E), with the changing domains passed explicitly. For a complete initial pass, set E to a copy of E₀, the full edge set.

Lines 02–04 are the main loop. While checks remain, select and remove one pair (X,c), then compute N_X using the support definition from the preceding section. A value is retained if some allowed combination of the other variables makes c true with that value. The code abbreviates the quantified test as “x has support for c”.

Lines 05–06 test whether filtering actually removed anything. If N_X equals dom(X), no domain update or rechecking is needed; continue with the next pending pair. If it is a proper subset, replace dom(X) with N_X.

Line 07 returns immediately when the revised domain is empty. That is enough to reject the current branch, so further filtering is unnecessary. The old pseudocode can continue until its worklist is empty; this early exit is the same sound stopping choice used by the interactive example.

Lines 08–09 add affected pairs back to E after a deletion. Another variable Z may have depended on a removed X value to satisfy another rule c′ containing both variables. The update selects c′≠c, Z≠X and {X,Z}⊆scope(c′). The dedicated rechecking section explains this selection after the worked example.

Line 10 returns when E is empty. With finite domains, only finitely many values can be deleted, and every deletion schedules finitely many checks. When all such checks are processed, filtering has reached a fixed point. The outcomes section distinguishes failure, a determined solution and remaining choices.

The course CSP starts with variables X₁,X₂,X₃, each having domain {0,1,2}, and constraints (X₁<2) ∧ (X₂>0) ∧ (X₃<X₁). E contains the pending (variable,constraint) checks. Use Next to process one pair at a time.

For the selected pair (X,c), the panel compares dom(X) before revision with N_X, the values kept by that check. The network shows the domain after dom(X)←N_X. For the first check X₁<2, the panel shows dom(X)={0,1,2} before and N_X={0,1} kept. The support panel gives a witness for each retained value. Use Next to compute a check, or Back to inspect an earlier revision.

After a deletion, an update box displays the instantiated E←E∪{...} operation. Worklist entries marked “Added now” are new; entries marked “Already pending” were already scheduled and are not duplicated. In the chain, watch (A,A<B) return after B loses 4. With no affected pairs in other rules, the box shows E←E∪∅.

At the course fixed point, the domains are {1}, {1,2} and {0}. Select the chain to see a previously checked pair return to E after it loses a supporting partner. The next slide explains that example. Select the contradiction to see why a nonempty fixed point alone need not establish a solution.

Use the chain A<B and B<C, with all domains initially {1,2,3,4}. After A<B is checked, A=4 and B=1 are removed. At that moment A=3 still has its sole supporting partner B=4.

Checking B against B<C then removes B=4, since no allowed C is larger. The old support for A=3 disappears. Put (A,A<B) back into E; processing it again removes A=3.

Continuing propagation reaches dom(A)={1,2}, dom(B)={2,3} and dom(C)={3,4}. One pass through the original pairs is insufficient: a later deletion can invalidate an earlier successful check. The next section translates this example into the set update used in the pseudocode.

The scheduling update in lines 08–09 keeps the checks already in E and adds pairs (Z,c′) that may have lost support. Here X is the variable whose domain shrank and c is the rule just checked. The other constraint c′ ranges over 𝓒, and Z ranges over its variables.

All three filters must hold: c′≠c selects a different rule, Z≠X selects another variable, and {X,Z}⊆scope(c′) requires that both variables occur in that rule. Union ∪ combines the pending sets; ∧ joins the logical requirements. In the chain example, the mapping is X=B, c:B<C, Z=A and c′:A<B, giving the work item (A,A<B).

The current constraint c can be excluded because an X value removed for having no support in c cannot have been a valid witness for another value in that same rule. Other constraints may have used that X value successfully. This argument assumes that revision removes exactly the values without support in c.

Adding a pair repeats a support check; it does not restore any deleted domain value. A pair already pending is added only once because E is a set. This is why the algorithm can propagate later deletions through the network without repeating every check after every change.

An empty domain means no value for that variable can be part of a solution under the current branch restrictions. Because GAC removes only unsupported values, the branch can be rejected. If this occurs at the root, the whole CSP has no solution.

If every domain contains exactly one value and all constraints are GAC-consistent, those values determine a solution. Each constraint’s only possible scoped tuple must satisfy it; otherwise a value would have no support.

If the domains are all nonempty but at least one has several values, GAC alone is inconclusive. The course example’s domains {1}, {1,2}, {0} lead to two solutions, while the next example has no solution despite nonempty domains.

A fixed point describes the end of propagation, not the end of the entire search. Domain splitting in Part 2 turns remaining alternatives into separate branches and applies propagation to each.

All three variables have domain {1,2,3,4}. The constraints are X₁=X₂, X₂=X₃ and X₁≠X₃. Each value has an equal partner for an equality, and a different partner for the inequality, so GAC removes nothing.

The witnesses are independent. For example, (X₁,X₂)=(1,1) satisfies the first rule, (X₂,X₃)=(1,1) satisfies the second, and (X₁,X₃)=(1,2) satisfies the third. These separate pairs are not one consistent assignment: they give different requirements for X₃.

Globally, the two equalities imply X₁=X₃. The inequality demands the opposite, so no solution exists. This counterexample proves that nonempty GAC-consistent domains do not generally establish satisfiability.

Local consistency checks only scoped supports. Search or stronger consistency reasoning is needed when those local choices must be made compatible across several constraints.

The combined requirement is (X₁=X₂) ∧ (X₂=X₃) ∧ (X₁≠X₃). The conjunction symbol ∧ requires one shared total assignment to satisfy all three statements. Independent witnesses for individual constraints do not make their conjunction satisfiable.

Practice explaining the lecture with the same three-variable example. First list the choices and rules. Next show why backtracking rejects X₁=2 without trying its completions. Then show how propagation also rules out X₁=0.

Finally distinguish what each method returns. Backtracking records complete solutions; GAC returns domains. A nonempty collection of domains may describe several solutions or none, so a solver must justify its conclusion.