Programul implementeaza algoritmul DPLL + unit propagation. Principalele functii sunt:
- is_clause_satisfied, care verifica daca o clauza este satisfacuta sub un anumit set de literali. Aceasta functie poate returna 3 valori: Yes (setul continue un literal care valideaza clauza), No (niciun literal din clauza nu se gaseste in set) si UndefinedYet ( exita literali in clauza care inca nu sunt definiti the set).
- is_clause_unitary, care verifica daca clauza este unitara si in caz afirmativ returneaza literalul clauzei care inca nu este definit de setul dat.
- check_and_remove_clauses, care itereaza peste o lista de clauze, verifica daca sunt satisfacute sau nu folosind functia is_clause_satisfied si daca cea din urma returneaza valoarea 'Yes' clauza este elimitata din lista, intrucat va fi satisfacuta de orice set care include setul de literali curent.
- dpll, care implementeaza algoritmul dat, urmand pseudocodul dat in cerinta temei.