cv01

Cvičenie 1

SAT solverov je veľa, budeme používať MiniSAT. Binárka pre windows sa dá stiahnuť priamo na ich stránke, ale potrebuje ešte 2 knižnice (cygwin1.dll, cygz.dll), všetky tri súbory sa nachádzajú v adresári s nástrojmi.

Vašou hlavnou úlohou na tomto cvičení je:

• vytvoriť si konto na https://github.com/ (ak už nemáte) a poslať mailom na adresu siska@ii.fmph.uniba.sk vaše univerzitné prihlasovacie id (login do AIS-u, v tvare priezviskoCISLO) a prihlasovacie meno do github-u. Do predmetu uveddte "UdVL registracia".
• po vyriešení týchto cvík si odložiť riešenie 2. príkladu (dva textové súbory), na budúcich cvičeniach si ukážeme, ako sa odovzdajú v github-e.

1. príklad

---

Cheme na párty pozvať niekoho z trojice Jim, Kim a Sára, bohužiaľ každý z nich má nejé svoje podmienky.

• Sarah nepôjde na party ak pojde Kim.
• Jim pôjde na párty, len ak pôjde Kim.
• Sara nepôjde bez Jima.

Zapísané v provorádovej logike (premenná kim znamená, že Kim pôjde na párty, atď):

kim → ¬sarah
jim → kim
sarah → jim
kim ∨ jim ∨ sarah

Prerobené do CNF (konjunktívnej normálnej formy):

¬kim ∨ ¬sarah

¬jim ∨ kim

¬sarah ∨ jim

kim ∨ jim ∨ sarah

DIMACS CNF formát

p cnf VARS CLAUSES
1 2 -3 0
...

p cnf 3 4
c -kim v -sarah
-1 -3 0
c -jim v kim
-2 1 0
c -sarah v jim
-3 2 0
c k v j v s
1 2 3 0

Aby bola práca s DIMACS CNF súbormi vo windows jednoduchšia, budeme im dávať príponu .txt, t.j. budeme sa tváriť ako by to boli obyčajné textové súbory.

SAT solver

Spustíme sat solver, ako parameter dáme meno vstupného súboru. MiniSAT normálne iba vypíše, či je vstup splniteľný, ak chceme aj nejaký výstup, tak dáme ešte meno výstupného súboru (MiniSAT ho vytvorí/prepíše.)

$ minisat party.cnf party.out
...
SATISFIABLE
$ cat party.out
SAT
1 -2 -3 0

MiniSAT nájde len nejaké riešenie, ak chceme nájsť ďašie, môžeme mu povedať, že toto konkrétne nechceme (nemajú naraz platiť tieto premenne). Toto riešenie je kim ∧ ¬jim ∧ ¬sarah, znegovaním dostaneme ¬kim ∨ jim ∨ sarah, čo je priamo disjunktívna klauza a môžeme ju pridať k zadaniu:

p cnf 3 5
-1 -3 0
-2 1 0
-3 2 0
1 2 3 0
c nechceme riesenie 1 -2 -3
-1 2 3 0

$ minisat party.cnf party.out
...
SATISFIABLE
$ cat party.out
SAT
1 2 -3 0

Ak to zopakujeme ešte raz, nenájdeme už žiadne riešenie:

p cnf 3 6
-1 -3 0
-2 1 0
-3 2 0
1 2 3 0
c nechceme riesenie 1 -2 -3
-1 2 3 0
c nechceme riesenie 1 2 -3
-1 -2 3 0

$ minisat party.cnf party.out
...
UNSATISFIABLE
$ cat party.out
UNSAT

2. Russian spy puzzle (4b)

---

(Andrei Voronkov, http://www.voronkov.com/lics.cgi)

There are three persons: Stirlitz, Muller, and Eismann. It is known that exactly one of them is Russian, while the other two are Germans. Moreover, every Russian must be a spy.

When Stirlitz meets Muller in a corridor, he makes the following joke: "you know, Muller, you are as German as I am Russian". It is known that Stirlitz always tells the truth when he is joking.

We have to establish that Eismann is not a Russian spy.