Prax 2: lihtsa DPLL lahendaja realiseerimine

Ülesande sisuks on lihtsa DPLL lahendaja realiseerimine nullist.

Sisendiks oleks lahendajal triviaalses DIMACS formaadis CNF (conjunctive normal form ehk disjunktsioonide konjunktsioon) fail, näiteks:

c Example CNF format file
c
p cnf 4 3
1 3 -4 0
4 0 2
-3

Näiteid ja lisajuttu leiad: http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html

Sinu programm peaks töötama lihtsalt käsurealt, võtma faili sisse, andma välja tulemuse ja soovitavalt veidi statistikat.

Tehnoloogia on vaba. Hea mõte on kasutada mõnda kiiremat, kompileeritud keelt a la C, C++, Java, C#.

Lahendaja peaks kindlasti sisaldama:

• unit clausede propageerijat (ühikresolutsiooni tegemine)
• rekursiivset splittijat (dpll põhiidee)

Mõistlik oleks realiseerida lahendaja nii, et ta ei genereeri füüsiliselt uusi disjunkte, vaid

• muutujate teadaolevad väärtused on integer massiivis
• muutujatel on küljes pointerite massiivid disjunktidele, kus ta esineb (eraldi negatiivsete ja positiivsete jaoks)
• disjunktidel on küljes counterid seni määramata positiivsete ja määramata negatiivsete literaalide kohta

Kui tahad teha eriti vinget tõestajat (ei ole kohustuslik), tasub tutvuda:

• eriti soovitav: http://minisat.se/Papers.html
• Eugene Goldbergi loengutega loeng1, loeng2,loeng3
• ja/või googeldada ja otsida zChaffi ja SATO jne kohta artikleid.

Valmis saadud lahendajaga tuleks veidi eksperimenteerida:

• loomulikult katsetada lihtsatel näidetel, et kas käib õieti
• katsetada keerukamate näidete peal, et millistega veel hakkama saab ntx 5 sek vältel ja millistega mitte