2SAT pgSQL < Sonstiges < Hochschule < Informatik < Vorhilfe
|
| Status: |
(Frage) beantwortet  | | Datum: | 09:47 Di 23.01.2007 | | Autor: | tommy987 |
| Aufgabe | Entwirf eine pgSQL-Funktion feasible(), die in polynomieller Zeit berechnet ob eine gegebene 2SAT-Formel erfüllbar ist.
2SAT-Details
Eine 2SAT-Formel ist eine konjunktive Normalform in der jede Klausel aus genau zwei Literalen besteht. Die Thematik wurde in der Vorlesung vom 11. Jänner näher behandelt. Dort - z. B. in den Powerpoint-Folien - findet sich auch ein entsprechender polynomieller Algorithmus.
SQL-Details
Die zu untersuchende Formel ist in Form eines Tables mit folgender Definition gegeben:
create table input (
literal1 integer,
literal2 integer
);
Die Literale werden also durch ganze Zahlen dargestellt: Positive Literale durch Zahlen größer Null, negative Literale durch Zahlen kleiner Null. Zum Beispiel steht...
literal1 literal2
1 2
-1 -3
-2 3
...für die Formel (a ∨ b) ∧ (¬ a ∨ ¬ c) ∧ (¬ b ∨ c). (Streng genommen ist die Variablenbezeichnung natürlich nicht eindeutig. Allerdings ist das für die Erfüllbarkeit auch nicht von Bedeutung.)
Ein Aufruf von select feasible() würde nun true zurückliefern. Beachte, dass die entsprechende Variablenbelegung - in diesem Fall z. B. a=F, b=c=T - nicht gefragt ist. Es geht nur darum, ob die Formel erfüllbar ist! |
Wie setzt ich da an?? Dem Problem steh ich etwas planlos gegenüber!
lg Thomas
|
|
| |
|
Moin Thomas,
ich kann Dir ad hoc nur was zu dem Problem 2SAT schreiben, zB warum es in P ist - falls das Teil Deiner Frage ist.
Du definierst zu gegebener 2SAT-Formel einen Graphen, der für jede vorkommende Variable [mm] x_i [/mm] einen Knoten [mm] x_i [/mm] und einen Knoten [mm] \overline{x_i} [/mm] hat, und für jede Klausel [mm] x_i^{\alpha}\vee x_j^{\beta} [/mm] mit [mm] \alpha,\beta\in\{0,1\} [/mm] und
[mm] x_i^{1}=x_i, x_i^0=\neg x_i
[/mm]
kriegt der Graph die gerichteten Kanten [mm] (x_i^{1-\alpha},x_j^{\beta}) [/mm] und [mm] (x_j^{1-\beta},x_i^{\alpha}),
[/mm]
dann ist die Formel genau dann erfüllbar, wenn es keine Variable [mm] x_i [/mm] gibt, so daß [mm] x_i [/mm] und [mm] \neg x_i [/mm] auf einem gerichteten kreis in dem Graphen liegen, so dass Du 2SAT also durch Kreissuche mittels BFS lösen kannst.
Gruss,
Mathias
|
|
|
|
