<jupyter_start><jupyter_text>E<NAME>i The following exercise is taken from the book "99 Logeleien von Zweistein".This book has been published 1968.  It is written by <NAME>. ---The gentlemen Amann, Bemann, Cemann and Demann are called - not necessarily in the same order - by their first names Erich, Fritz, Gustav and Heiner. They are all married to exactly one woman. We also know the following about them and their wives:- Either Amann's first name is Heiner, or Bemann's wife is Inge.- If Cemann is married to Josefa, then - **and only in this case** - Klara's husband is **not** called Fritz.- If Josefa's husband is **not** called Erich, then Inge is married to Fritz.- If Luise's husband is called Fritz, then Klara's husband's first name is **not** Gustav.- If the wife of Fritz is called Inge, then Erich is **not** married to Josefa.- If Fritz is **not** married to Luise, then Gustav's wife's name is Klara.- Either Demann is married to Luise, or Cemann is called Gustav.*What are the full fullnames of these gentlemen, and what are their wives' first names?*--- We are going to solve this problem by coding it in propositional logic and we will solve the resulting set of clauses using the Davis-Putnam algorithm.  In order to code the problem, we will use the following propositional variables:- $\texttt{Name}$ for any male first name $x$ and any surname $z$ expresses  that the gentleman with first name $x$ has surname $z$.- $\texttt{Ehe}$ for any male first name $x$ and any female first name $y$ expresses  that the gentleman with first name $x$ is married to the woman with first name $y$. We are using the symbols $\texttt{}$ as part of the propositional variables because we want to show the structure of these variables and the parser for propositional logic accepts these symbols as part of propositional variables.<jupyter_code>Vornamen  = { "Erich",  "Fritz", "Gustav", "Heiner" }
Nachnamen = { "Amann", "Bemann", "Cemann", "Demann" }
Frauen    = { "Inge",  "Josefa", "Klara",  "Luise"  }
%run ../Davis-Putnam.ipynb<jupyter_output><empty_output><jupyter_text>The function $\texttt{makeVar}(f, x, y)$ creates a propositional variable of the form $\texttt{f}$.<jupyter_code>def makeVar(f, x, y):
    return f + '<' + x + ',' + y + '>'
makeVar('Ehe', 'Heiner', 'Klara')<jupyter_output><empty_output><jupyter_text>Given a set of propositional variables $S$, the function $\texttt{atMostOne}(S)$ computes a set of clauses expressing the fact that at most one of the variables of $S$ is True.<jupyter_code>def atMostOne(S): 
    return { frozenset({('¬',p), ('¬', q)}) for p in S
                                            for q in S 
                                            if  p != q 
           }<jupyter_output><empty_output><jupyter_text>Given a set of propositional variables $S$, the function $\texttt{atLeastOne}(S)$ computes a set of clauses expressing the fact that at least one of the variables of $S$ is True.<jupyter_code>def atLeastOne(S):
    return { frozenset(S) }<jupyter_output><empty_output><jupyter_text>$S$ is a set of propositional variables. The expression $\texttt{exactlyOne}(S)$ creates a set of clauses.  This set expresses the fact that exactly one of the variables in the set $S$ is true.<jupyter_code>def exactlyOne(S):
    return atMostOne(S) | atLeastOne(S)<jupyter_output><empty_output><jupyter_text>For two sets $A$ and $B$ that have the same number of elements and a function symbol $f$, the procedure $\texttt{bijective}(A, B, f)$ computes a set of clauses that is equivalent to the formula$$   \bigl(\forall x \in A: \exists! y \in B: f\langle x, y\rangle\bigr) \wedge     \bigl(\forall y \in B: \exists! x \in A: f\langle x, y\rangle\bigr)$$Here the expression $f\langle x,y\rangle$ is the name of a propositional variable and the expression $\exists!x:p(x)$ is to be read as "There exists exactly one $x$ such that $p(x)$ holds".<jupyter_code>def bijective(A, B, f):
    "your code here"<jupyter_output><empty_output><jupyter_text>For example, the function call `bijective({'a', 'b'}, {'x', 'y'}, 'f')` returns the following set of clauses:```{frozenset({('¬', 'f'), ('¬', 'f')}), frozenset({('¬', 'f'), ('¬', 'f')}), frozenset({'f', 'f'}), frozenset({'f', 'f'}), frozenset({'f', 'f'}), frozenset({'f', 'f'}), frozenset({('¬', 'f'), ('¬', 'f')}), frozenset({('¬', 'f'), ('¬', 'f')})}``` The function $\texttt{setToFormula}(S)$ converts the set of formulas $S$ from propositional logic into a conjunction of these formulas.  Since the formulas in $S$ can be complex, we have to ensure that everything is properly parenthesized.<jupyter_code>def setToFormula(S):
    if len(S) == 1:
        return '(' + S.pop() + ')'
    formula = S.pop()
    return f'({formula})' + ' ∧ ' + setToFormula(S)
setToFormula({'a', 'b', 'c'})<jupyter_output><empty_output><jupyter_text>The function $\texttt{isWifeOf}(y, z)$ returns a formula that is true if $y$ is the wife of $z$.  Here, $y$ is the first name of a woman, while $z$ is the last name of a man. The formula is returned as a string.<jupyter_code>def isWifeOf(y, z):
    return setToFormula({f"Name<{x},{z}> → Ehe<{x},{y}>" for x in Vornamen })
isWifeOf("Inge", "Amann")
import propLogParser as plp
run ../CNF.ipynb<jupyter_output><empty_output><jupyter_text>The function $\texttt{parseAndNormalize}(s)$ takes a string $s$, parses this string as a propositional formula and then turns this formula into a set of clauses.<jupyter_code>def parseAndNormalize(s):
    nestedTuple = plp.LogicParser(s).parse()
    Clauses     = normalize(nestedTuple)
    return Clauses
parseAndNormalize('a ↔ ¬b')<jupyter_output><empty_output><jupyter_text>The function `exclusiveOr(a, b)` computes the *exclusive or* of the formulas $a$ and $b$, which are given as strings. The resulting formula itself is converted into CNF.<jupyter_code>def exclusiveOr(a, b):
    formula     = f'(({a}) ↔ ¬({b}))'
    return parseAndNormalize(formula)
exclusiveOr('p', 'q')<jupyter_output><empty_output><jupyter_text>Below, you might need the following symbols: ¬, ∧, ∨, →, ↔<jupyter_code>def computeClauses():
    # Jedem männlichen Vornamen ist genau ein Nachname zugeordnet und umgekehrt.
    Clauses  = "your code here"
    # Jeder Mann ist mit genau einer Frau verheiratet und umgekehrt.
    Clauses |= "your code here"
    # Entweder ist Amanns Vorname Heiner, oder <NAME> heisst Inge.
    Clauses |= "your code here"
    # Wenn Cemann mit Josefa verheiratet ist, dann – und nur in diesem Falle –
    # heisst <NAME> nicht Fritz.
    Clauses |= "your code here"
    # Wenn <NAME> nicht Erich heisst, dann ist Inge mit Fritz verheiratet.
    Clauses |= "your code here"
    # Wenn <NAME> heisst, dann ist der Vorname von <NAME> nicht Gustav.
    Clauses |= "your code here"
    # Wenn die Frau von Fritz Inge heisst, dann ist Erich nicht mit Josefa verheiratet.
    Clauses |= "your code here"
    # Wenn Fritz nicht mit Luise verheiratet ist, dann heisst Gustavs Frau Klara.
    Clauses |= "your code here"
    # Entweder ist Demann mit Luise verheiratet, oder <NAME>isst Gustav.
    Clauses |= "your code here"
    return Clauses
Clauses = computeClauses()
Clauses<jupyter_output><empty_output><jupyter_text>There are 176 different clauses.<jupyter_code>len(Clauses)
def compute_solution():
    Clauses = computeClauses()
    Result  = solve(Clauses, set())
    return Result
Solution = compute_solution()
import re

def extractFirst(s):
        m = re.search('<([A-Za-z]+),', s)
        return m.group(1)

def extractSecond(s):
        m = re.search(',([A-Za-z]+)>', s)
        return m.group(1)
def displaySolution(Solution):
    Married = {}
    Names   = {}
    for Unit in Solution:
        for l in Unit:
            if isinstance(l, str):
                if l[:3] == "Ehe":
                    x = extractFirst(l)
                    y = extractSecond(l)
                    Married[x] = y
                elif l[:4] == "Name":
                    x = extractFirst(l)
                    y = extractSecond(l)
                    Names[x] = y
    for x in Married:
        print(f"{x} {Names[x]} is married to {Married[x]}.")
displaySolution(Solution)<jupyter_output><empty_output><jupyter_text>Checking the Uniqueness of the Solution<jupyter_code>def arb(S):
    for x in S:
        return x<jupyter_output><empty_output><jupyter_text>Given a set of unit clauses $U$, the function $\texttt{checkUniqueness}(U)$ returns a clause that is the negation of the set $U$.<jupyter_code>def negateSolution(UnitClauses):
    return { complement(arb(unit)) for unit in UnitClauses }
negateSolution({ frozenset({'a'}), frozenset({('¬', 'b')}) }) 
def checkUniqueness(Solution, Clauses):
    negation = negateSolution(Solution)
    Clauses.add(frozenset(negation))
    alternative = solve(Clauses, set())
    if alternative == { frozenset() }:
        print("Well done: The solution is unique!")
    else:
        print("ERROR: The solution is not unique!")
checkUniqueness(Solution, Clauses)<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.12764064932177008, 'fraction_numerical': 0.00155659328441183, 'mean_word_length': 3.896570495372891, 'pattern_counts': {'":': 2, '<': 69, '<?xml version=': 0, '>': 69, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '14', 'dir': 'jupyter-structured-clean-dedup', 'id': '21102', 'license': 'MIT', 'n_tokens_mistral': 2979, 'n_tokens_neox': 2870, 'n_words': 1060, 'path': 'Python/Exercises/Blatt-08.ipynb', 'repo_name': 'adroi3/Logic', 'size': '9045'}