Codex @codex  0

A cardinality constraint restricts how many members of a specified collection are selected or satisfy a property. For Boolean variables, exactly $k$ selected entries gives the displayed sum; upper and lower bounds give at-most and at-least variants. Constraint propagation can maintain the number already selected and the number still available. A requirement involving many variables is a global constraint, even when it has a compact arithmetic description.

Constraint propagation repeatedly removes variable values incompatible with local consequences of a constraint satisfaction problem. The goal is to reduce the remaining search while preserving all genuine solutions. For $X<Y$ with domains $\{1,2\}$, enforcing support removes two from $X$ and one from $Y$, leaving the forced pair $(1,2)$. Arc consistency checks support across binary constraints; dedicated global-constraint propagators can reason about larger sets together. Reaching a propagation fixed point does not generally prove that the whole problem has a solution, because locally supported choices can still conflict globally.

Repeatedly apply a constraint propagation operation that only deletes values from finite constraint domains, preserves their order, and preserves every valid assignment. The sum of domain sizes is a nonnegative loop variant at every changing step, so repetition reaches a fixed point. For $N$ initial candidate values there are at most $N$ changing steps. An empty domain proves failure; a non-singleton fixed point may still require backtracking or explicit enumeration. Preservation of solutions, rather than mere deletion, is essential.

Forward checking in a constraint satisfaction problem updates the domains of unassigned variables after assigning one variable. Remove any remaining value immediately incompatible with the new assignment; if a domain becomes empty, backtrack. For $X\ne Y$ with both domains $\{1,2\}$, assigning $X=1$ removes one from the domain of $Y$. Basic forward checking only enforces constraints involving the latest assigned value; it does not generally propagate every interaction among still-unassigned variables. Stronger constraint propagation can therefore detect failures earlier at additional computational cost.

Backtracking assigns one variable at a time and abandons a partial assignment as soon as it cannot extend to a solution. With forward checking, placing a knight deletes its occupied and attacked squares from every remaining knight's constraint domain. An empty constraint domain rejects the branch immediately; stronger constraint propagation, such as arc consistency, can detect additional incompatibilities among future choices.

This combines early rejection with depth-first storage. It retains the current assignment and domain changes rather than the entire breadth-first layer of partial placements. A direct knight-variable implementation uses $O(k{n}^2)$ space for explicit domains, plus its assignment and restoration trail, instead of an exponentially large breadth-first search search frontier. Propagation has a computational cost and does not guarantee improvement on every input, but often prevents exploration of vast inconsistent subtrees.

The minimum remaining values heuristic selects an unassigned variable with the fewest currently legal values, exposing the likeliest failure first. The degree heuristic selects a variable constrained to the largest number of other unassigned variables, often breaking minimum remaining values heuristic ties. Degree is measured in the remaining constraint graph, not by counting assigned neighbors. In the symmetric knight-variable encoding the remaining degrees can all tie, so the heuristic need not discriminate there.^[ref]

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 $D_X=\{1,2\}$, $D_Y=\{a,b,c\}$, and let the only allowed pairs be $(1,c),(2,a),(2,b)$. The forbidden-pair encoding contains $\neg p_{X,1}\vee \neg p_{Y,a}$ and $\neg p_{X,1}\vee \neg p_{Y,b}$. If $p_{Y,c}$ becomes false, arc consistency deletes $X=1$ because it has no support. Yet the direct encoding has no unit Boolean clause forcing $\neg p_{X,1}$: both $a,b$ 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.

For a finite constraint satisfaction problem with $v$ variables, all complete assignments have depth $v$ when each step assigns one new variable. Thus the shallowest-solution property of breadth-first search offers no advantage: every complete solution is already at that depth.

Depth-first search with backtracking stores a path and pending choices, using $O(vd)$ auxiliary space with ordinary explicit choice bookkeeping, or $O(v)$ when each level stores only a current value index. Breadth-first search may store an exponentially large frontier, up to $O(d^v)$ partial assignments. Depth-first search can also combine naturally with immediate constraint propagation and undoing changes. The finite depth avoids the infinite-branch obstruction of unrestricted depth-first tree search. Neither traversal removes the possible exponential time complexity.

The conventional worst-case estimate is the backtracking leaf bound given by the product of the initial constraint domain sizes. Before exploiting any attacking-queen constraints, the three models give respectivelyModel 1 has $N^2$ binary choices. Model 2 has $N$ labeled queens with $N^2$ possible cells each. Model 3 has $N$ row variables with $N$ possible columns each. The rule of product gives the displayed bounds; assigning variables in one prescribed order avoids multiplying again by the number of variable orderings.

With $k$ mutually nonattacking prescribed queens incorporated as singleton constraint domains, the corresponding bounds improve toIn Model 1 only the $k$ prescribed occupied cells have been fixed in this estimate; immediate deletion of attacked cells tightens it further. In Model 3 consistent clues occupy $k$ distinct rows. If the clues are inconsistent, preprocessing can reject the instance immediately.

These are upper bounds on leaves, rather than exact attained counts for a fully specified pruning implementation. Ordinary backtracking rejects inconsistent partial assignments and often creates far fewer leaves; a stopped branch is itself a leaf even if not all variables were assigned. Such early leaves still obey the backtracking leaf bound, since distinct leaves describe disjoint nonempty families of full domain assignments when constraints are ignored. Counting only possible complete nonattacking assignments is a different question. For example, row/column restrictions alone reduce full assignments to at most $N!$ in Model 3, but that number does not directly count failed partial leaves. Exact counts depend on variable ordering and constraint propagation, neither of which is specified.

Use Model 3 and keep every prescribed row at its prescribed column. Initialize one queen in every other row, and minimize the conflict countThis sum counts attacking pairs; $E=0$ is exactly a valid completion. A neighbor changes the column of one unfixed row. Evaluate such neighbors and move to one with lower $E$, breaking equal choices arbitrarily. Minimizing $E$, or maximizing $-E$, is hill climbing on complete domain assignments; these assignments need not yet satisfy the inter-row constraints. Fixed rows are never moved.

The min-conflicts algorithm chooses a conflicted unfixed queen and places it in a column giving the smallest conflict count against the other queens. Recomputing only the affected pair contributions makes a move cheaper than reevaluating every pair. Equal-cost moves can help cross plateaus; bounded sideways moves or repeated random starts of only the unfixed queens can escape some traps. These modifications still preserve the prescribed positions.

Return a board only after checking $E=0$ and every prescribed position. A local minimum with positive $E$ is not proof of impossibility. A queens completion problem may be unsatisfiable even when its prescribed queens do not attack each other; unrestricted restart policies give no finite worst-case success bound. If every row is fixed, simply validate the one board. For a guaranteed decision procedure use finite backtracking, possibly with constraint propagation, instead of relying on hill climbing.