MAKEFILE:

build:

Instructiunea de build compileaza fisierele java.

run:

Instructiunea de run executa codul java, pasand ca argumente numele fisierelor de Input si Output

Codul:

Codul este scris in java. Avem doua fisiere, Main si Table. Table este o clasa In care salvez formula ce trebuie analizata intr-un format usor de manipulat.

In Main avem functiile:

• int[] recurenceStart(Table formula)

  • este wrapperul functiei recursive

• int recurse_func(Table formula, int[] partialAssignment)

• Aici se intampla verificarile, euristicile si recursia

• int verifyFalseClauses(Table formula, int[] partialAssignment)

  • Aici verific daca atribuirea mea partiala falsifica vreo clauza din formula
  • Daca da, in functia recurse_func voi marca nodul curent ca deadNode, trecand la urmatorul

• int verifyUnitaryClauses(Table formula, int[] partialAssignment)

  • Aici se aplica euristicile de tip Unit Propagation.
  • Dupa ce gasim o clauza unitara si inseram elementul nou in atribuirea partiala,
  • verificam daca s-a falsificat vreo clauza ca urmare. Daca nu, continuam procesul.

File IO este manevrat de functia main, iar ca rezultat al apelului catre recurenceStart se decide daca scriem "s Unsatisfiable" sau "s Satisfiable" si asignarea gasita (aceasta fiind returnata de functie)