Zadanie 4 (semestralne!)

 

Problem spełnialności zbioru klauzul w rachunku zdań jest jednym z klasycznych problemów przeszukiwania z więziami. Istnieją różne metody dla tego problemu, np. rezolucja lub system tablicowy, ale do tej pory podejście traktujące ten problem jako problem przeszukiwania z więziami jest uznane jako najefektywniejsze. Zobacz The Quest for Efficient Boolean Satisfiability Solvers.

 

Formalnie, problem spełnialności zbioru klauzul w rachunku zdań (SAT) jest wyrażony następująco: Dany jest skończony zbiór klauzul, gdzie każda klauzula ma postać

L1 Ú L2 Ú ... Ú Lk

i każdy Li jest literałem, czyli atom lub negacja atomu. Czy istnieje wartościowanie (boolowskie) dla atomów takie, że wszystkie klauzule danego zbioru są prawdziwe przy tym wartościowaniu?

Problem 3SAT jest podobne do problemu SAT, ale z dodatkowym ograniczeniem, że każda klauzula ma dokładnie 3 literały.

 

Dla tego problemu, jak zwykle, można zastosować przeszukiwanie przyrostowe z powracaniem (ang. DFS with backtracking).  Najistotniejsze tutaj są wybór zmiennej, sprawdzenie wprzód, sprawdzenie spójności łukowej, itd.

 

Dane wejściowe są zapisane w pliku tekstowym z takimi konwencjami:

-         Komentarze zaczynają się na literę „c”.

-         Gdzieś na początku pliku (tzn. przed wystąpieniami klauzul) jest informacja o liczbie zmiennych i liczbie klauzul w postaci

p cnf  <liczba zmiennych>  <liczba klauzul>

-         Każda klauzula jest wymieniona w jednej linii zakończonej (spacją i) 0.

-         Zmienne są ponumerowane od 1. Pozytywna liczba reprezentuje pozytywny literał, a negatywna liczba reprezentuje negatywny literału odpowiedniego atomu.

-         Przedostatnia linia w pliku zawiera jedynie znak %. (Po co? Nie wiem! Ale tak jest przyjęte w pewnych zbiorach testów.)

-         Ostatnia linia w pliku zawiera jedynie 0.

 

Na przykład:

 

c To są dane testowe, z 5 zmiennymi i 3 klauzulami

c Każda klauzula ma 3 literały.

p cnf 4 3

1 –2 3 0

2 –3 –4 0

-1 3 4 0

%

0

 

Napisać program rozwiązujący problem 3SAT w dowolnym języku programowania (dostępnym na Wydziale).

Na Internecie dostępne są niektóre programy dla tego problemu; zobacz SAT Competition 2004. Wolno je obejrzeć ale nie wolno kopiować kodu. W szczególności, wymagam wyjaśnienia (pisemnego lub ustnego) dla każdego fragmentu kodu.

Przygotowane testy można znaleźć na stronie SATLIB - Benchmark Problems.