Algorytm, którego kod jest zamieszczony w dodatku C, służy do rozwiązywania
problemu Exact 3-SAT (X3SAT). Został on opisany w [5]. Ogólny problem
SAT (także 3SAT i X3SAT) polega na szukaniu takiego wartościowania zmiennych
logicznych w danej formule logicznej, które spełnia tą formułę. Jest to problem
z klasy NP i nie jest znany algorytm działający w czasie wielomianowym, który
go rozwiązuje. Dzięki kilku obserwacjom i umiejętnej redukcji klauzul autorom
tej pracy udało się stworzyć algorytm rozwiązujący problem X3SAT i działający
w czasie
, gdzie n jest liczbą zmiennych występujących
w formule.
Przedstawiona w pracy implementacja tego algorytmu jako parametry przyjmuje
liczbę dostępnych procesorów wirtualnych (zmienna proc_num), liczbę
klauzul w formule (zmienna length). Właściwą formułę należy umieścić
w tablicy formula w następujący sposób: wartość danej komórki to numer
zmiennej przy czym jeśli jest ona ujemna, oznacza to zanegowanie odpowiedniej
zmiennej. W przedstawionej implementacji formuły mogą mieć maksymalnie 1024
klauzule, a największy numer zmiennej to 4095. Rzeczywista liczba procesorów
wirtualnych, jaka zostanie użyta wynosi
,
gdzie proc_num jest liczbą procesorów podaną jako parametr.
Jeśli istnieje wartościowanie będące rozwiązaniem danego problemu, to zmienna
answer przyjmuje wartość 1, a w tablicy assignment zapisuje się
wartości logiczne odpowiadające zmiennym
.
Jeśli rozwiązanie zadania nie istnieje, to zmienna answer będzie miała
wartość 0.