constraint-propagation-solver

Answer

The implementation is a general-purpose CSP solver with three key algorithms working together:

1. AC-3 Arc Consistency

The ac3() method maintains a queue of arcs (directed edges between variables sharing binary constraints). For each arc (Xi, Xj), _revise() removes values from Xi's domain that have no supporting value in Xj's domain. This propagates through the constraint graph until fixpoint or a domain empties.

def _revise(self, xi, xj, domains, assignment):
    """Remove values of xi that have no support in xj's domain."""
    rel = []
    for idx in self._constraints_by_var[xi]:
        scope, func = self.constraints[idx]
        if xj in scope:
            rel.append((scope, func))
    if not rel:
        return False

    revised = False
    to_remove = []
    for val in domains[xi]:
        supported = False
        for val2 in domains[xj]:
            ok = all(self._check_support(scope, func, xi, val, xj, val2, 
                                         domains, assignment) 
                     for scope, func in rel)
            if ok:
                supported = True
                break
        if not supported:
            to_remove.append(val)
            revised = True
    for val in to_remove:
        domains[xi].remove(val)
    return revised

2. MRV with Degree Tiebreaking

The _select_unassigned_variable() method picks the variable with the smallest remaining domain. When multiple variables tie, it breaks ties by picking the one with the highest degree (most constraints with unassigned variables).

def _select_unassigned_variable(self, assignment, domains):
    unassigned = [v for v in self.variables if v not in assignment]
    min_size = min(len(domains[v]) for v in unassigned)
    candidates = [v for v in unassigned if len(domains[v]) == min_size]
    if len(candidates) == 1:
        return candidates[0]

    def degree(v):
        return sum(1 for n in self._neighbors[v] if n not in assignment)
    return max(candidates, key=degree)

3. Conflict-Directed Backjumping (CBJ)

The _cbj() method implements CBJ with conflict sets. Each variable maintains a set of previously-assigned variables that conflict with it. When all values for a variable fail, it returns its conflict set upward. The parent checks whether the failing variable is in the returned conflict set: if not, it backjumps further up (skipping irrelevant branches); if so, it absorbs the conflicts and tries the next value.

def _cbj(self, assignment, domains):
    if len(assignment) == len(self.variables):
        return assignment

    var = self._select_unassigned_variable(assignment, domains)
    values = self._order_domain_values(var, assignment, domains)

    my_conf = set(nb for nb in self._neighbors[var] if nb in assignment)

    for val in values:
        if not self._is_consistent(var, val, assignment, domains):
            my_conf |= self._get_local_conflicts(var, val, assignment)
            continue

        new_assignment = {**assignment, var: val}
        new_domains = {v: list(domains[v]) for v in self.variables}

        if not self.ac3(new_domains, new_assignment):
            my_conf |= self._get_local_conflicts(var, val, assignment)
            continue

        result = self._cbj(new_assignment, new_domains)

        if isinstance(result, dict):
            return result          # solution found
        if isinstance(result, set):
            if var not in result:
                return result      # backjump — var isn't the culprit
            my_conf |= (result - {var})

    return my_conf if my_conf else set()

The solver's solve() method orchestrates everything: it first filters unary constraints, runs an initial AC-3 pass, then calls _cbj() which integrates all three techniques recursively.