Neue Frage
1

Davis-Putnam Procedure

gefragt 2017-08-06 12:33:35 +0200

blackmamba Gravatar-Bild

aktualisiert 2017-08-06 12:34:56 +0200

I do not understand the Davis-Putnam Procedure.

Here is the question:

{{a}, {b, !d, !a}, {c, !d, !b}, {d, c, a, !b}, {d, c, b}, {c, !d, !b}, {d, c, !b, !a}, {c, a, !b}}. Name the literals that need to be satisfied according to Unit-Propagation

{{a}, {b, !d, !a}, {c, !d, !b}, {d, c, a, !b}, {d, c, b}, {c, !d, !b}, {d, c, !b, !a}, {c, a, !b}}.Name the literals that need to be satisfied according to Pure-Literal-Rule

Can anyone explain this in detail?

bearbeiten retag Als beleidigend melden schließen löschen

2 Antworten

2

geantwortet 2017-08-14 20:57:56 +0200

PS Gravatar-Bild

Recall that a set of clauses represents a CNF, i.e., we consider the conjunction of the clauses and each clause is the disjunction of its contained literals. Now, if there is a unit clause, i.e., a clause that only contains a single literal $\ell$, then the entire CNF is a formula of the form $\ell\wedge\varphi$. To satisfy it, we must obviously make $\ell$ true. For this reason, the unit propagation rule assigns now a truth value to the variable in $\ell$.

In the example {{a}, {b, !d, !a}, {c, !d, !b}, {d, c, a, !b}, {d, c, b}, {c, !d, !b}, {d, c, !b, !a}, {c, a, !b}}, there is only the unit clause {a} so that we have to assign a:=1 due to the unit clause rule.

For the pure literal rule, assume that there are no clauses that contain $x$. Hence, there are only clauses that have no occurrence of $x$, and there are clauses that contain $\neg x$. This means that our formula is equivalent to $\varphi \wedge (\neg x\vee \psi)$. To satisfy it, we have to satisfy $\varphi$ and one of $\neg x$ and $\psi$. Therefore, any assignment of $\varphi \wedge \neg x$ is also one for the considered formula, and any assignment of the considered formula can be modified in $x$ to become one of $\varphi \wedge \neg x$ (since $x$ does neither occur in $\varphi$ nor in $\psi$). Hence, the search for a satisfying assignment can now ignore $\psi$, and just assigns $x:=0$ and continues the search with the clauses that have no occurrences of $x$ (i.e., our formula $\varphi$).

Analogous arguments apply if there are no clauses that contain $\neg x$. In that case, the pure literal rule simply assigns $x:=1$ and continues the search with the clauses that have no occurrences of $\neg x$.

In the example, {{a}, {b, !d, !a}, {c, !d, !b}, {d, c, a, !b}, {d, c, b}, {c, !d, !b}, {d, c, !b, !a}, {c, a, !b}}, we check all variables for having pure literals only:

  • a has positive and negative occurrences
  • b occurs positively in {b, !d, !a} and negatively in {c, !d, !b}
  • c has only positive occurrences
  • d has positive and negative occurrences

Hence, the pure literal rule can assign c:=1 and continues with the clause set {{a}, {b, !d, !a}}. Recall that the unit clause rule assigns furthermore a:=1, so that we are only left with {{b, !d}} which can be satisfied by b:=1 or d:=0. So, we easily find a satisfying assignment by the two propagation rules.

bearbeiten Als beleidigend melden löschen publish Link mehr
1

geantwortet 2017-08-07 11:06:13 +0200

The Davis-Putnam Procedure is introduced and explained in the VRS-chapter on propositional logic starting from slide 83. Basically, the procedure works tree-like and adds more and tries to refine partial assignments until there is a solution. The case splits add two children to a node. One of them setting a variable $x$ to true, the other one setting $x$ to false.

The smart part about the Davis-Purnam Procedure is the application of rules. We mainly consider unit propagation and pure literal. The idea is that we only add one instead of two children. We set a variable $x$ to true or false with the semantics “If there is a satisfying assignment, then we still find one if we set $x$ to that value.“

The unit propagation rule searches for units. Units are clauses that consist of only one literal. A satisfying assignment satisfies all clauses of the CNF. Hence, it has to satisfy the only literal of the unit clause.

The pure literal rule searches for literals that either occur with or without negation in the whole clause. All clauses containing this literal can not be left unsatisfied, if the literal is satisfied. Thus, every satisfying assignment stays satisfying fixing the variable so that the pure literal is satisfied.

The exercise you posted is about a single step in the Davis-Putnam procedure. You are asked to find unit clauses and pure literals of the given formula.

bearbeiten Als beleidigend melden löschen publish Link mehr

Ihre Antwort

Du kannst deinen Eintrag bereits als Gast verfassen. Deine Antwort wird zwischengespeichert, bis du dich eingeloggt oder registriert hast.
Bitte nur konstruktive Antworten auf diese konkrete Frage posten.
Falls du eine Frage stellen willst, dann stelle eine neue Frage.
Für kurze Diskussionen und Nachfragen benutze bitte die Kommentar-Funktion.
Deine Fragen und Antworten kannst du jederzeit nachbearbeiten und verbessern.
Gute Fragen und Antworten kannst du mit einem Upvote oder Downvote bewerten.

Schreibe deine Antwort auf diese Frage

[Vorschau ausblenden]

Fragen-Tools

Beobachten
1 Follower

Statistik

Gefragt: 2017-08-06 12:33:35 +0200

Gesehen: 56 mal

Letztes Update: Aug 14