import ast

"""
Explanation: If we want to have reproducible results, the environment variable PYTHONHASHSEED has to be set to a fixed value, for example to 0.
Below we check that this environment is set so that results are reproducible.
In order to set this variable we have to use the following sequence of commands in the anaconda shell.
conda activate ai
conda env config vars set PYTHONHASHSEED=0
conda activate ai
It is necessary to reactivate the environment ai for the setting to take effect.
Consistency Checking
Utility Functions
End of explanation
"""


def collect_variables(expression): 
    tree      = ast.parse(expression)
    Variables = { node.id for node in ast.walk(tree) 
                          if  isinstance(node, ast.Name) 
                          if node.id not in dir(__builtins__)
                }
    return frozenset(Variables)

"""
Explanation: The function collect_variables(expr) takes a string expr that can be interpreted as a Python expression as input and collects all variables occurring in expr.  It takes care to eliminate the function symbols from the names returned by extract_variables.
End of explanation
"""


def arb(S):
    for x in S:
        return x

"""
Explanation: The function arb(S) takes a set S as input and returns an arbitrary element from 
this set.
End of explanation
"""


class Backtrack(Exception):
    pass

"""
Explanation: Backtracking is simulated by raising the Backtrack exception.  We define this new class of exceptions so that we can distinguish Backtrack exceptions from ordinary exceptions.  This is done by creating a new, empty class that is derived from the class Exception.
End of explanation
"""


def union(L):
    return { x for S in L
               for x in S
           }

union([ {1, 2}, {'a', 'b'}, {1, 'a'} ])

"""
Explanation: Given a list of sets L, the function union(L) returns the set of all elements occurring in some set $S$ that is itself a member of the list L, i.e. we have
$$ \texttt{union}(L) = { x \mid \exists S \in L : x \in L }. $$
End of explanation
"""


def solve(P, check_consistency=True, lcv=False):
    Variables, Values, Constraints = P
    VarsInConstrs  = union([ collect_variables(f) for f in Constraints ])
    MisspelledVars = (VarsInConstrs - Variables) | (Variables - VarsInConstrs)
    if MisspelledVars:
        print("Did you misspell any of the following Variables?")
        for v in MisspelledVars:
            print(v)
    ValuesPerVar = { x: Values for x in Variables }
    Annotated    = { f: collect_variables(f) for f in Constraints }
    UnaryConstrs = { (f, V) for f, V in Annotated.items() if len(V) == 1 }
    OtherConstrs = { (f, V) for f, V in Annotated.items() if len(V) >= 2 }
    Connected    = {}
    Var2Formulas = variables_2_formulas(OtherConstrs)
    for x in Variables:
        Connected[x] = union([ V for f, V in Annotated.items() if x in V ]) - { x }
    try:
        for f, V in UnaryConstrs:
            var               = arb(V)
            ValuesPerVar[var] = solve_unary(f, var, ValuesPerVar[var])
        if check_consistency:
            enforce_consistency(ValuesPerVar, Var2Formulas, Annotated, Connected)
            for x, Values in ValuesPerVar.items():
                print(f'{x}: {Values}')
        return backtrack_search({}, ValuesPerVar, OtherConstrs, lcv)
    except Backtrack:
        return None

"""
Explanation: A Constraint Propagation Solver with Consistency Maintenance
The procedure solve(P, check_consistency) takes two arguments:
* P is a constraint satisfaction problem 
  Here P is a triple of the form 
  $$ \mathcal{P} = \langle \mathtt{Variables}, \mathtt{Values}, \mathtt{Constraints} \rangle $$
  where 
  - $\mathtt{Variables}$ is a set of strings which serve as variables,
  - $\mathtt{Values}$ is a set of values that can be assigned 
    to the variables in the set $\mathtt{Variables}$.
  - $\mathtt{Constraints}$ is a set of formulas from first order logic.
    Each of these formulas is  called a constraint of $\mathcal{P}$.
* check_consistency is a Boolean flag.  If this flag is True, then consistency maintenance is used
  as a preprocessing step.
Before trying to solve the given CSP, solve checks whether the set of variables occurring in
the constraints is the same as the set Variables.  If this is not the case, then this is most likely due to
a spelling error and a warning message is printed.  Then, the function solve converts the CSP P into an augmented CSP where every constraint $f$ is annotated with the variables occurring in $f$.  Furthermore, the function solve maintains the following data structures:

VarsInConstrs is the set of all variables occurring in any constraint.
ValuesPerVar is a dictionary mapping variables to sets of values.  For every variable x occurring in a constraint of P, the expression ValuesPerVar[x] is the set of values that can be used to instantiate the variable x.  Initially, ValuesPerVar[x] is set to Values, but as the search for a solution proceeds, the sets ValuesPerVar[x] are reduced by removing any values that cannot be part of a solution.
Annotated is a dictionary.  For every constraint f we have that Annotated[f] is the set of all variables occurring in f.
UnaryConstrs is a set of pairs of the form (f, V) where f is a constraint containing only a single variable and V is the set containing just this variable.
OtherConstrs is a set of pairs of the form (f, V) where f is a constraint containing more than one variable and V is the set of all variables occurring in f.
Connected is a dictionary mapping variables to sets of variables.  If x is a variable, then  Connected[x] is the set of those variables y such that there is a constraint f that mentions both the variable x and the variable y.
Var2Formulas is a dictionary mapping variables to sets of formulas.  For every variable x, Var2Formulas[x] is the set of all those non-unary constraints f such that x occurs in f.

The unary constraints are immediately solved.  After that, the function enforce_consistency performs 
consistency maintenance:
Formally, we define that a value $v$ is consistent for a variable $x$ with respect to a constraint $f$
iff the partial assignment ${ x \mapsto v }$ can be extended to an assignment $A$ satisfying the constraint $f$,
i.e. for every variable $\texttt{y}_i$ occurring in f there is a value $w_i \in \texttt{ValuesPerVar}[y]$ such that
$$ \texttt{eval}\bigl(f, { x \mapsto v, y_1 \mapsto w_1, \cdots, y_n \mapsto w_n}\bigr) = \texttt{True}. $$
The call to enforce_consistency shrinks the sets ValuesPerVars[x] until all values in ValuesPerVars[x]
are consistent with respect to all constraints.
Finally, backtrack_search is called to solve the remaining constraint satisfaction problem by the means of both backtracking and
constraint propagation.  Furthermore, the most constrained variable heuristic and the least constraining value heuristic are used.
End of explanation
"""


def variables_2_formulas(Constraints):
    Dictionary = {}
    for f, Vars in Constraints:
        for x in Vars: 
            if x in Dictionary: # Dictionary[x] is already defined
                Dictionary[x] |= { f }
            else:               # Dictionary[x] is not yet defined
                Dictionary[x]  = { f }
    return Dictionary

"""
Explanation: The function variables_2_formulas takes a set of annotated constraints as input.  An annotated constraint is a pair of the form
(f, V) where f is a formula and V is the set of variables occurring in f.  The function returns
a dictionary that maps every variable x to the set of those constraints f such that x occurs in f.
End of explanation
"""


def enforce_consistency(ValuesPerVar, Var2Formulas, Annotated, Connected):
    UncheckedVars = set(Var2Formulas.keys())
    while UncheckedVars:
        variable    = UncheckedVars.pop()
        Constraints = Var2Formulas[variable]
        Values      = ValuesPerVar[variable]
        RemovedVals = set()
        for f in Constraints:
            OtherVars = Annotated[f] - { variable }
            for value in Values:
                if not exists_values(variable, value, f, OtherVars, ValuesPerVar):
                    RemovedVals   |= { value }
                    UncheckedVars |= Connected[variable]
        Remaining = Values - RemovedVals
        if not Remaining: # the problem is unsolvable
            raise Backtrack()
        ValuesPerVar[variable] = Remaining

"""
Explanation: The function enforce_consistency takes 4 arguments:
- ValuesPerVar is a dictionary.  For every variable x we have that ValuesPerVar[x] is the set of values that can be substituted for x.
- Var2Formulas is a dictionary.  For every variable x we have that Var2Formulas[x] is the set of those formulas that mention the variable x.
- Annotated is a dictionary.  For every constraint F, Annotated[F] is the set of variables occurring in F.
- Connected is a dictionary.  For every variable x we have that Connected[x] is the set of those variables y that are directly connected with the variable x.  Two variables x and y are directly connected if there is a constraint F such that both x and y occur in F.  In this case, F is connecting x and y.
The function enforce_consistency shrinks the sets ValuesPerVar[x] such that the values in ValuesPerVar[x] are consistent for x for all constraints.
End of explanation
"""


def exists_values(var, val, f, Vars, ValuesPerVar):
    Assignments = all_assignments(set(Vars), ValuesPerVar)
    return any(eval(f, extend(A, var, val)) for A in Assignments)

"""
Explanation: The procedure exists_values takes five arguments:
- var is a variable, 
- val is a value val, 
- f   is a constraint,
- Vars is the set Vars of those variables in f that are different from var, and
- ValuesPerVar is a dictionary.  For every variable x we have that ValuesPerVar[x] is the set of those values that still may be tried for x.
The function checks whether there is a value for var such that the other variables occurring in the constraint f can be set to values such that the constraint f is satisfied.
End of explanation
"""


def extend(A, x, v):
    B = A.copy()
    B[x] = v
    return B

"""
Explanation: The function extend takes three arguments:
- A is a dictionary,
- x is a variable such that A[x]is not yet defined,
- v is some value.
It returns a new dictionary B such that B[x] = v and B[y] = A[y] for all y != x.
End of explanation
"""


def all_assignments(Variables, ValuesPerVar):
    if not Variables:
        return [ {} ]  # list containing empty assignment
    var         = Variables.pop()
    Values      = ValuesPerVar[var]
    Assignments = all_assignments(Variables, ValuesPerVar)
    return [ extend(A, var, val) for A in Assignments 
                                 for val in ValuesPerVar[var]
           ]

ValuesPerVar = { 'x': {1, 2}, 'y': {2, 3} }
Variables    = { 'x', 'y' }
all_assignments(Variables, ValuesPerVar)

"""
Explanation: The function all_assignments returns the list of all possible assignments for the variables in the set Vars.
For every variable x, the values for x are taken from ValuesPerVar[x].
End of explanation
"""


def solve_unary(f, x, Values):
    Legal = { value for value in Values if  eval(f, { x: value }) }
    if not Legal:
        raise Backtrack()
    return Legal

"""
Explanation: The function solve_unary takes a unary constraint f, a variable x and the set of values Values that can be assigned to x.  It returns the subset of values that can be substituted for x such that $f[x\mapsto v]$ evaluates as True.
End of explanation
"""


def backtrack_search(Assignment, ValuesPerVar, Constraints, lcv):
    if len(Assignment) == len(ValuesPerVar):
        return Assignment
    x = most_constrained_variable(Assignment, ValuesPerVar)
    if lcv and len(ValuesPerVar[x]) > 1:
        ValueList = least_constraining(x, ValuesPerVar, Assignment, Constraints)
    else:
        ValueList = ValuesPerVar[x]
    for v in ValueList:
        try:
            NewValues = propagate(x, v, Assignment, Constraints, ValuesPerVar)
            NewAssign = Assignment.copy()
            NewAssign[x] = v
            return backtrack_search(NewAssign, NewValues, Constraints, lcv)
        except Backtrack:
            continue
    raise Backtrack()

"""
Explanation: The function backtrack_search takes three arguments:
- Assignment is a partial variable assignment that is represented as a
   dictionary.  Initially, this assignment will be the  empty dictionary.   
   Every recursive call of backtrack_search adds the assignment of one 
   variable to  the given assignment. 
- ValuesPerVar is a dictionary.  For every variable x, ValuesPerVar[x] is the set of values that still might be assigned to x.
- Constraints is a set of pairs of the form (f, V) where f is a constraint and V is the set of variables occurring in f.
The function backtrack_search uses the most constrained variable heuristic in order to choose the next variable.  It uses the least constraining value heuristic to choose the value that is assigned to this variable.
End of explanation
"""


def most_constrained_variable(Assignment, ValuesPerVar):
    Unassigned = { (x, len(U)) for x, U in ValuesPerVar.items()
                               if  x not in Assignment
                 }
    minSize = min(lenU for x, lenU in Unassigned)
    for x, lenU in Unassigned:
        if lenU == minSize:
            return x

"""
Explanation: The function most_constrained_variable takes two parameters:
- Assigment is a partial variable assignment that assigns values to variables.  It is represented as a dictionary.
- ValuesPerVar is a dictionary that has variables as keys.  For every variable x, ValuesPerVar[x] is the set of values that 
  can still be assigned to the variable x.
The function returns an unassigned variable x such that the number of values in ValuesPerVar[x] is minimal among all other unassigned variables.
Hence, this variable is a most constraint variable.
* In order to find this variable, the set Unassigned is computed.  This is a set of pairs of the form (x, n) 
  where x is a variable that is not yet assigned and n is the number of values that can still be assigned to x.
* minSize is the number of values that can be assigned to a most constrained variable.
End of explanation
"""


import math

"""
Explanation: The module math is needed because it provides math.inf, which represents $\infty$.
End of explanation
"""


def least_constraining(x, ValuesPerVar, Assignment, Constraints):
    NumbersValues = []
    for value in ValuesPerVar[x]:
        ReducedValues = ValuesPerVar.copy()
        num_removed = number_removed_values(x, value, Assignment, ReducedValues, Constraints)
        if num_removed != math.inf:
            NumbersValues.append( (num_removed, value) )
    NumbersValues.sort(key=lambda p: p[0])
    return [val for _, val in NumbersValues]

"""
Explanation: The function least_constraining takes four arguments:
* x is a variable. 
* ValuesPerVar is a dictionary.  For every variable var, ValuesPerVar[var] is the set of values that can be assigned to var.
* Assignment is a partial variable assignment.
* Constraints is a set of annotated constraints.
This function returns a list of values that can be substituted for the variable x.
This list is sorted so that the least constraining values are at the beginning of this list.
End of explanation
"""


def number_removed_values(x, value, Assignment, ValuesPerVar, Constraints):
    count     = 0   # number of values removed from ValuesPerVar
    BoundVars = set(Assignment.keys())
    for f, Vars in Constraints:
        if x in Vars:
            UnboundVars = Vars - BoundVars - { x }
            if len(UnboundVars) == 1:
                y = arb(UnboundVars)
                Legal = set()
                for w in ValuesPerVar[y]:
                    NewAssign = Assignment.copy()
                    NewAssign[x] = value
                    NewAssign[y] = w
                    if eval(f, NewAssign):
                        Legal.add(w)
                    else:
                        count += 1
                if not Legal:
                    count = math.inf
                ValuesPerVar[x] = Legal
    return count           

"""
Explanation: The function number_removed_values takes 5 arguments:
- x is a variable that has not yet been assigned a value.
- value is a value that is to be assigned to the variable x.
- Assignment is a partial variable assignment that does not assign a value to x.
- ValuesPerVar is a dictionary that has variables as keys.  For every variable x, ValuesPerVar[x] is the set of values that 
  can still be assigned to the variable x.
- Constraints is a set of pairs of the form (f, V) where f is a constraint and V is the set of variables occurring in f.
This function returns the number of values that need to be removed from the set ValuesPerVar[y] for those variables y that are 
different from x if we assign value to the variable x.  If the assignment { x: value } results in any of the sets ValuesPerVar[y]
becoming empty, then the function returns math.inf in order to signal that the assignment { x: value } leads to an unsolvable problem.
End of explanation
"""


def propagate(x, v, Assignment, Constraints, ValuesPerVar):
    ValuesDict = ValuesPerVar.copy()
    ValuesDict[x] = { v }
    BoundVars = set(Assignment.keys())
    for F, Vars in Constraints:
        if x in Vars:
            UnboundVars = Vars - BoundVars - { x }
            if len(UnboundVars) == 1:
                y = arb(UnboundVars)
                Legal = set()
                for w in ValuesDict[y]:
                    NewAssign = Assignment.copy()
                    NewAssign[x] = v
                    NewAssign[y] = w
                    if eval(F, NewAssign):
                        Legal.add(w)
                if not Legal:
                    raise Backtrack()
                ValuesDict[y] = Legal
    return ValuesDict

"""
Explanation: The function propagate takes five arguments:
- x is a variable,
- v is a value that is supposed to be assigned to x.
- Assignment is a partial assignment that contains assignments for variables that are different from x.
- Constraints is a set of annotated constraints.
- ValuesPerVar is a dictionary assigning sets of values to all variables.  For every unassigned variable z,  ValuesPerVar[z] is the set of values that still might be assigned to z.
The purpose of the function  propagate is to compute how the sets ValuesPerVar[z] can be shrunk when the value v is assigned to the variable x.  The dictionary ValuesPerVar with appropriately reduced sets ValuesPerVar[z] is returned.
End of explanation
"""


%%capture
%run N-Queens-Problem-CSP.ipynb

P = create_csp(8)

"""
Explanation: Solving the Eight-Queens-Puzzle
End of explanation
"""


%%time
Solution = solve(P, check_consistency=True)
Solution
print(f'Solution = {Solution}')

show_solution(Solution)

%%time
Solution = solve(P, check_consistency=False)
print(f'Solution = {Solution}')

P = create_csp(32)

"""
Explanation: The consistency solver takes about 23 milliseconds on my desktop to solve the eight queens puzzle.  Hence, for the eight queens puzzle, consistency maintenance does not help.
End of explanation
"""


%%time
Solution = solve(P, check_consistency=True)
print(f'Solution = {Solution}')

"""
Explanation: The 32-queens-problem can be solved in 1 second.
End of explanation
"""


%run Zebra.ipynb

zebra = zebra_csp()

"""
Explanation: Solving the Zebra Puzzle
End of explanation
"""


%%time
Solution = solve(zebra, check_consistency=False)

show_solution(Solution)

"""
Explanation: The consistency solver takes about 11 milliseconds to solve the zebra puzzle without consistency maintenance.
End of explanation
"""


%%time
Solution = solve(zebra, check_consistency=True)

"""
Explanation: For the Zebra puzzle, consistency maintenance does not decrease the running time.
End of explanation
"""


%run Sudoku.ipynb

csp = sudoku_csp(Sudoku)

%%time
Solution = solve(csp, check_consistency=False)

show_solution(Solution)

"""
Explanation: Solving a Sudoku Puzzle
End of explanation
"""


%%time
Solution = solve(csp, check_consistency=True)

"""
Explanation: For the sudoku, consistency maintenance does not decrease the running time.
End of explanation
"""


%run Crypto-Arithmetic.ipynb

csp = crypto_csp()

"""
Explanation: Solving a Crypto-Arithmetic Puzzle
End of explanation
"""


%%time
Solution = solve(csp, check_consistency=True)

show_solution(Solution)

"""
Explanation: With consistency checking the time to solve the crypto arithmetic puzzle is reduced to less than 150 milliseconds.
End of explanation
"""


%%time
Solution = solve(csp, check_consistency=False)

csp = crypto_csp_hard()
csp

%%time
Solution = solve(csp, check_consistency=True)

"""
Explanation: Without consistency checking, the problem takes 1.45 seconds.
End of explanation
"""


%%time
Solution = solve(csp, check_consistency=False)

"""
Explanation: For the hard version of the crypto-arithmetic puzzle, consistency maintenance decreases the total running time considerably.
End of explanation
"""


