diff --git a/sheets/03_card_sat/README.md b/sheets/03_card_sat/README.md index 60e057b9705e01752b5dbbb81eb526a64d645442..b0348c38c8eddebe2df0f76fb4c781a3923a5321 100644 --- a/sheets/03_card_sat/README.md +++ b/sheets/03_card_sat/README.md @@ -14,7 +14,7 @@ In this problem, we are given propositional formula $\phi$ on a set of boolean v Such a formula has the following form: ```math -\phi = \underbrace{(\ell_{1,1} \vee \cdots \vee \ell_{1,k_1})}_{\text{Klausel 1}} \wedge \cdots \wedge \underbrace{(\ell_{m,1} \vee \cdots \vee \ell_{m,k_m})}_{\text{Klausel $m$}}. +\phi = \underbrace{(\ell_{1,1} \vee \cdots \vee \ell_{1,k_1})}_{\text{Clause 1}} \wedge \cdots \wedge \underbrace{(\ell_{m,1} \vee \cdots \vee \ell_{m,k_m})}_{\text{Clause $m$}}. ``` The $\ell_{i,j}$ are so called *literals* and have either the form $x_u$ or $\bar{x}_u := \neg x_u$, i.e., they are either a variable or a negation of it. @@ -26,7 +26,7 @@ And example for such a formula would be The boolean satisfiability problem asks if a given formula $\phi$ is *satisfiable$. A formula is satisfiable if there is a *satifying assignment*, -i.e., a mapping $a: \{x_1,\ldots,x_n\} \to \{\texttt{wahr}, \texttt{falsch}\}$, +i.e., a mapping $a: \{x_1,\ldots,x_n\} \to \{\texttt{true}, \texttt{false}\}$, that assignes every variable a boolean value, such that the formula evaluates to true. For a formula $\phi$ is conjunctive normal form, this implies that every clause needs to be satisfied, i.e., at least on of its literals has been satisfied. @@ -46,7 +46,7 @@ with Gluecard4(with_proof=False) as gc4: gc4.add_clause([1, -2, 3]) gc4.add_clause([2, 4]) if gc4.solve(): - solution = gc4.get_model() + solution = gc4.get_model() # returns [-1, -2, -3, 4] else: print("No solution!") ```