Cvičenie 4

Riešenie tejto úlohy odvzajte v moodli do 30.10.2014 13:09:59.

Vyriešte úlohu o gazdovi, koze, kapuste a vlku pomocu SAT solvera (treba aj "dekodér" výstupu). Váš program by mal na vstupe dostať dlĺžku plánu, ktoý má hľadať a vypísať postupnosť akcií, alebo že plán tej dĺžky neexistuje. (Nevadí, ak bude vypisovať aj nejaké informácie navyše, napríklad stav v každom kroku riešenia a pod.)

Niekoľko poznámok, ktoré by mohli pomôct:

Najjednoduchšie je použiť reprezentáciu so 4 fluentami a 8 akciami s tým, že každá akcia má len jednu sadu podmienok kedy sa môže vykonať a vždy má rovnaký efekt (prevezenie doľava a doprava sú teda rôzne akcie). (Toto je ten "jednoduchší" jazyk ako jazyk A, ktorý sme si hovorili na prednáške).

Vo vstupe pre SAT solver sú premenné reprezentované číslami, takže pomožu správne pomocné funkcie a konštanty, ktoré uľahčia preklad z mien fluentov a akcií do čísel a naopak. Potrebujem vlastne 4*(N+1) premenných pre fluenty tvaru vlavo_KTO_I pre 0 <= I <= N a 2*4*N premenných pre akcie tvaru prevez_KAM_KTO_I pre 0 <= I < N-1 (N je dĺžka plánu, ktorý hľadáme).

Formuly pre počiatočný a koncový stav, efekty acií a frame problem (zotrvačnosť nemenených fluentov) boli na prednáške. Formuly pre obmedzenia úlohy (kto nemôže ostať bez gazdu na tom istom brehu) sa buď zahrnúť do predpokladov akcií ale tiež ľahko napísať pre každý stav I:
formula ¬(vlavo_vlk_i∧vlavo_kapusta_i∧¬vlavo_gazda_i) hovorí, že sa nesmie stať (taká interpr. nebude naším modelom) aby vlk a kapusta boli v i-tom kroku vľavo bez gazdu.

Formalizácia z prednášky:

• fi - fluent f platí v kroku i
• ¬fi - fluent f neplatí v kroku i
• ai - akcia a sa vykoná v kroku i
• počiatočný stav: f0 ak f má platiť, ¬f0 ak nemá.
• koncový stav podobne s fN
• v každom kroku aspoň jedna akcia:
  a0i ∨ a1i ∨ ... ∨ ami
• v každom kroku max jedna akcia: ¬aji ∨ ¬aki pre každú dvojicu rôznych akcií aj a ak
• podmienky pre vykonanie akcie: ai→(p1i ∧ p2i ∧...) ak p1, p2, ... sú podmienky pre vykonanie akcie a
• effekty akcií: ai→(e1i+1 ∧ e2i+1 ∧...) ak e1, e2, ... sú efekty akcie a
• "Explanatory frame axioms":
  (¬fi ∧ fi+1) → ⋁ {aji | f ∈ effects+(aj}
(fi ∧ ¬fi+1) → ⋁ {aji | f ∈ effects-(aj}
  kde effects+(a) sú kladné efekty akcie aa effects-(a) sú záporné.