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
:- op(400,xfy,/\). % konjunkce
:- op(350,xfy,\/). % disjunkce
Pro ohodnocení máme definovaný operátor
:-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