Links und Funktionen
Sprachumschaltung

Navigationspfad
You are here: Home / Teaching / Winter 2015/16 / SAT Solving / Solutions / Exercise 1


Inhaltsbereich

Exercise 1

Plain Text icon u01e01.txt — Plain Text, 1 KB (2012 bytes)

File contents

F = (~x /\ (~y \/ (z /\ ~w)) \/ (x /\ (~z \/ (~y /\ w))))

| x     | y     | z     | w     | F(x,y,z,w) | clause                   |
|-------+-------+-------+-------+------------+--------------------------|
| false | false | false | false | true       | ( ~x /\ ~y /\ ~z /\ ~w ) |
| false | false | false | true  | true       | ( ~x /\ ~y /\ ~z /\  w ) |
| false | false | true  | false | true       | ( ~x /\ ~y /\  z /\ ~w ) |
| false | false | true  | true  | true       | ( ~x /\ ~y /\  z /\  w ) |
| false | true  | false | false | false      |                          |
| false | true  | false | true  | false      |                          |
| false | true  | true  | false | true       | ( ~x /\  y /\  z /\ ~w ) |
| false | true  | true  | true  | false      |                          |
| true  | false | false | false | true       | (  x /\ ~y /\ ~z /\ ~w ) |
| true  | false | false | true  | true       | (  x /\ ~y /\ ~z /\  w ) |
| true  | false | true  | false | false      |                          |
| true  | false | true  | true  | true       | (  x /\ ~y /\  z /\  w ) |
| true  | true  | false | false | true       | (  x /\  y /\ ~z /\ ~w ) |
| true  | true  | false | true  | true       | (  x /\  y /\ ~z /\  w ) |
| true  | true  | true  | false | false      |                          |
| true  | true  | true  | true  | false      |                          |

Resulting DNF formula:

   ( ~x /\ ~y /\ ~z /\ ~w )
\/ ( ~x /\ ~y /\ ~z /\ w )
\/ ( ~x /\ ~y /\ z /\ ~w )
\/ ( ~x /\ ~y /\ z /\ w )
\/ ( ~x /\ y /\ z /\ ~w )
\/ ( x /\ ~y /\ ~z /\ ~w )
\/ ( x /\ ~y /\ ~z /\ w )
\/ ( x /\ ~y /\ z /\ w )
\/ ( x /\ y /\ ~z /\ ~w )
\/ ( x /\ y /\ ~z /\ w )

Simplifying:

   ( ~x /\ ~y /\ ~z )
\/ ( ~x /\ ~y /\ z )
\/ ( ~x /\ y /\ z /\ ~w )
\/ ( x /\ ~y /\ ~z /\ ~w )
\/ ( x /\ ~y /\ w )
\/ ( x /\ y /\ ~z )

Simplifying further:

   ( ~x /\ ~y )
\/ ( ~x /\ y /\ z /\ ~w )
\/ ( x /\ ~y /\ ~z /\ ~w )
\/ ( x /\ ~y /\ w )
\/ ( x /\ y /\ ~z )

Document Actions


Funktionsleiste