For a finite constraint satisfaction problem, remove values violating unary restrictions before starting. The following backtracking algorithm makes independent copies of constraint domains at each branch, so failed forward checking cannot contaminate a sibling branch.
SOLVE(P):
D := domains of P after unary filtering
if some D[X] is empty: return failure
return SEARCH({}, D)
SEARCH(assignment, D):
if every variable is assigned: return assignment
X := SELECT-UNASSIGNED-VARIABLE(assignment, D, P)
for v in ORDER-DOMAIN-VALUES(X, assignment, D, P):
if X=v is compatible with the current assignment:
next_assignment := assignment extended by X=v
next_domains := a deep copy of D
next_domains[X] := {v}
if INFERENCES(X, v, next_assignment, next_domains, P) succeeds:
result := SEARCH(next_assignment, next_domains)
if result is not failure: return result
return failureSELECT-UNASSIGNED-VARIABLE implements minimum remaining values: choose an unassigned variable with the smallest current constraint domain. Break ties by the degree heuristic, choosing the variable constrained to the greatest number of other unassigned variables; a fixed final tie rule makes execution reproducible. ORDER-DOMAIN-VALUES may use any complete ordering; ascending values suffice here.
INFERENCES implements forward checking: for each unassigned neighbor of , remove every value incompatible with , and fail if any constraint domain becomes empty. For higher-arity constraints, reject any completely instantiated violation and use a sound chosen filtering rule; the stated neighbor test is the usual binary case. Forward checking never removes a value used by a possible extension of the current assignment. Exhausting every surviving value therefore makes this finite backtracking procedure both sound and complete.[ref]
CS 188 constraint filtering notes. §2.3, opening paragraphs: filtering neighbors after assignment
[ref]Forward checking makes minimum remaining values respond to current restrictions rather than the original constraint domain sizes. After , its neighbors may have fewer choices, become forced or lose all choices. Minimum remaining values then selects the newly constrained variable early, while an empty constraint domain triggers immediate failure. The two mechanisms expose failure sooner and reduce wasted backtracking.
Forward checking only tests an unassigned neighbor against the newly assigned value. It need not check whether two still-unassigned variables have mutually supporting values. Arc consistency requires every value at either end of each binary constraint to have support in the other constraint domain, and AC-3 propagates deletions until this condition stabilizes or a constraint domain becomes empty.[ref]
For example, let initially have constraint domains with constraints and . Assigning makes forward checking reduce to , but leaves . Arc consistency also deletes from , leaving . Neither procedure alone decides every general constraint satisfaction problem: a triangle of two-valued inequalities satisfies arc consistency but is unsatisfiable.
One solution is . Use ascending value order; after minimum remaining values and the degree heuristic, break any remaining variable tie alphabetically. Apply the unary restrictions first:
Minimum remaining values selects , even though has greater initial vertex degree. Set . Forward checking removes from the three neighbors :Now is the unique minimum remaining values choice. Set . Forward checking removes from , givingSelect and set . Its remaining neighbors are , so forward checking givesThe two remaining variables tie on constraint domain size and each has one unassigned neighbor, so the degree heuristic also ties. Alphabetical order selects ; take . Since is already absent from , forward checking makes no further deletion. Finally choose . No empty constraint domain or violation occurs, so this branch needs no backtracking.
All eight binary constraints are checked explicitly by the unequal value pairsThe unary restrictions also hold. Equalities and are permitted because those pairs have no edges in the constraint graph.
Cutset conditioning selects a cycle cutset : deleting its vertices makes the binary constraint graph a forest. Enumerate assignments to , reject those violating internal constraints, and filter each remaining constraint domain against the chosen cutset values. Solve the residual components by tree-structured constraint satisfaction. Stop at a successful assignment, or report failure after all cutset assignments fail. Completeness follows by considering the restriction of any full solution to ; soundness follows by checking internal, crossing and residual constraints. With maximum constraint domain size and cutset variables, a typical bound is for the residual forest work, with cutset and crossing checks added explicitly.[ref]
Here take . The residual constraint graph has vertices and only edges , a tree rooted at . Choose the consistent cutset values . Filtering against these assignments givesThe upward support pass from deletes , because can only equal . The pass from retains , which has support or . Assign at the root and then supported child values . Together with , this gives the solution in (c).
No singleton cycle cutset exists: deleting or leaves, respectively, a triangle on or ; deleting leaves the cycle in a graph . Thus the two-element choice is also minimum, although the algorithm only requires a valid cutset.
Use an exactly-one constraint for each finite-domain variable and a Boolean clause forbidding each disallowed constraint tuple. Let the variables be , with explicitly listed finite constraint domains , and let constraint have distinct-variable scope and allowed relation . Introduce a Boolean variable for every , interpreted as . The direct SAT encoding of finite-domain constraints isIn the middle logical conjunction, each unordered distinct pair is included once. The first Boolean clause requires at least one value, the pairwise Boolean clauses permit at most one, and a final Boolean clause is false exactly when all coordinates of one forbidden tuple are selected. The formula is in conjunctive normal form. An empty constraint domain produces an empty Boolean clause, correctly making the instance unsatisfiable.
For soundness of the reduction, a solution of the constraint satisfaction problem gives the Boolean valuation exactly when . Every exactly-one constraint holds; a forbidden tuple differs from on at least one scoped coordinate, making its negative Boolean clause true. Thus supplies a satisfying assignment for .
Conversely, a satisfying assignment selects a unique value for every . If a constraint failed, the selected scoped tuple would belong to , and its entire negative Boolean clause would be false. That contradicts satisfiability. Hence is a solution. Decoding takes by scanning the value indicators. This proves has a solution if and only if is satisfiable.
For explicit size accounting, put , and . There are Boolean variables,Boolean clauses, andliteral occurrences. These formulas count nonempty scopes; a false zero-arity constraint contributes an empty Boolean clause, while a true one contributes none. Formula storage is literal-sized records; a bit-level encoding also stores indicator indices. With maximum constraint domain size , constraints and maximum arity , this is bounded by for nontrivial domains and scopes. In the common binary case it is .
The input representation matters: listing all forbidden tuples costs up to tests per constraint. This is polynomial for bounded arity and explicitly represented domains, but can be exponential in the description length of a succinct high-arity constraint. The translation is valid in that case without constituting a polynomial-size reduction. If a compact constraint is supplied as a polynomial-size Boolean circuit, one may instead encode that circuit using auxiliary Boolean variables and local conjunctive normal form equivalences, with size proportional to the circuit. No compact representation is silently assumed.
For the instance in (c), after unary filtering there are indicators. The five at-least-one Boolean clauses, pairwise at-most-one Boolean clauses and forbidden-equality Boolean clauses give Boolean clauses. Setting only true encodes the displayed solution.
The translation gives a sound and complete route through an optimized SAT solver; it trades access to general-purpose SAT machinery against encoding cost and the possible loss of constraint-specific structure. Modern SAT solvers use efficient unit propagation, adaptive branching and clause learning. Learned Boolean clauses can summarize conflicts involving many original variables, allowing later branches to avoid repeating the same failed combination. The reduction also offers a standard, reusable interface: improvements to a SAT solver can benefit many finite-domain constraint satisfaction problems.
The Boolean formula may be much larger than the original constraint satisfaction problem, especially for a succinct high-arity relation. One original variable becomes many indicators, and general branching may lose the interpretation that the minimum remaining values and degree heuristic exploit directly. Native constraint propagation can exploit a relation without enumerating all its forbidden tuples. Even in the binary case, stronger propagation does not follow just from switching to SAT.
For example, take , , and let the only allowed pairs be . The forbidden-pair encoding contains and . If becomes false, arc consistency deletes because it has no support. Yet the direct encoding has no unit Boolean clause forcing : both remain possible individually, so plain unit propagation does not make that deletion. A SAT solver can eventually derive it through additional reasoning or search. Conversely, clause learning can combine information beyond the local consistency enforced by AC-3. Neither approach uniformly dominates: performance depends on representation, propagation strength and the instance's structure; both still face exponential worst-case search on general inputs.
Articles by others on the same topic
There are currently no matching articles.