Logică și structuri discrete - Exerciții cu determinarea realizabilității

1. Determinarea realizabilității Urmăriți codul scris la curs și explicați ce pași se parcurg în determinarea realizabilității unei formule propoziționale.
Folosiți o formulă în CNF produsă de acest generator. Selectați în dreapta Problem Type: Random k-Sat, 3 literale pe clauză, 5 variabile, 6 clauze. În fișierul random_ksat.dimacs generat, fiecare rând încheiat de 0 reprezintă o clauză, întregii negativi reprezintă negații. Deci 3 -6 -1 0 reprezintă p₃ ∨ ¬ p₁ ∨ ¬ p₆.
Puteți să vă ajutați în explicații adăugând tipăriri la codul scris (ex. ce atribuiri se încearcă pentru ce variabile, ce clauze se simplifică) sau doar să urmăriți codul "cu creionul pe hârtie.