Napište predikát dpll(F,V)
, který pro formuli F v CNF najde pomocí algoritmu DPLL ohodnocení V, pokud existuje ohodnocení, pokud neexistuje, predikát selže (tj. vrátí no)
Pro formuli máme definované tři spojky
:- op(300,fx,~). % negace
Pro ohodnocení máme definovaný operátor
:- op(400,xfy,/\). % konjunkce
:- op(350,xfy,\/). % disjunkce
:-op(450,xfy,/).
Příklad volání:
?-dpll((a\/b\/ ~c)/\(~a\/b)/\c,V).
V=[a/1,b/1,c/1].
do V se nemusí ohodnotit všechny proměnné, stačí jen ty, které splňují formuli. Tj pro následující formuli stačí, aby to vrátilo jen ohodnocení jedné z nich
?-dpll((a\/b\/ ~c),V).
V=[a/1].
Dobrý materiál na sat solver naleznete také na slidech k Umělé inteligenci. Nemusí to být extra vychytané, stačí základní algoritmus.
Deadline: 5.5. 20:00