Skip to content
Snippets Groups Projects
Commit 1d7602ee authored by Gabriel Gehrke's avatar Gabriel Gehrke
Browse files

minor translation fixes

parent d623c04b
No related branches found
No related tags found
No related merge requests found
......@@ -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!")
```
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment