Rješavanje 3-SAT problema: od iscrpnog pretraživanja do lokalnih heuristika (GSAT, WalkSAT, ILS)

TLDR

• Riječ je o 3-SAT problemu: pronaći dodjelu booleovih varijabli koja zadovoljava sve klauzule.
• Implementirao sam više algoritama: iscrpno pretraživanje, pohlepni uspon (hill climbing), poboljšani hill-climbing s dinamičkim ponderiranjem, GSAT, WalkSAT i Iterated Local Search.
• Fokus mi je bio na tome kako se algoritmi ponašaju kad upadnu u lokalne optimume i koliko pomažu random restarts, noise i perturbacije.

Motivacija

3-SAT je jedan od klasičnih problema kombinatorne optimizacije: jednostavan za objasniti, a brzo postane računalno težak. Super mi je kao poligon za testiranje različitih strategija pretraživanja:

• Što se dogodi kad samo penjem fitness dok ide?
• Kako izgleda izlazak iz lokalnog optimuma pomoću nasumičnosti?
• Koliko pomažu restartovi i heuristike poput GSAT/WalkSAT?

Ovaj projekt mi je bio praktičan način da spojim teoriju (NP-potpunost, pretraživanje prostora) s implementacijom i eksperimentiranjem.

Problem

U 3-SAT imamo booleove varijable i skup klauzula, gdje je svaka klauzula disjunkcija točno tri literala (npr. (x1 ∨ ¬x4 ∨ x7)).

Cilj: naći dodjelu varijabli x ∈ {0,1}^n takvu da su sve klauzule zadovoljene.

Ovo je NP-potpun problem => iscrpno pretraživanje radi kao baseline za male instance, ali skaliranje brzo postane nemoguće.

Format ulaza i evaluacija

Ulazne instance su u DIMACS CNF formatu (npr. uf20-01.cnf).

Interno sam klauzule parsirao u listu literala oblika (indeks_varijable, trazena_vrijednost), gdje:

• pozitivni literal x_i mapira se na (i, 1)
• negativni literal ¬x_i mapira se na (i, 0)

Fitness (dobrota) u većini algoritama je:

• broj zadovoljenih klauzula
• cilj je doći do broj_zadovoljenih = broj_klauzula

Pristup i algoritmi

1) Iscrpno pretraživanje (baseline)

Prođe kroz sve dodjele varijabli 2^n i provjeri zadovoljava li formula sve klauzule. Kao što samo ime kaže, ovo je iscrpno i eksponencijalno. Primjer kada egzaktna metoda nema smisla (za n=20 već ima preko milijun mogućnosti) te se moramo okrenuti heuristikama.

• Prednost: uvijek nađe rješenje ako postoji
• Mana: eksplodira s n (već na n=50 je praktički neizvedivo)

Koristio sam ga kao referencu i sanity-check za male instance.

2) Pohlepni uspon na vrh (hill climbing)

Krenem od nasumične dodjele i gledam susjedstvo dobiveno flipanjem jedne varijable.

• odaberem susjeda s najvećim brojem zadovoljenih klauzula
• ako nema boljeg susjeda → lokalni optimum (stagnacija)

Ovaj pristup zna biti brz, ali je osjetljiv na lokalne optimume.

3) “Ponderirani” hill climbing (dinamičko fokusiranje na teške klauzule)

Ovo je varijanta hill-climbinga u kojoj fitness nije samo “broj zadovoljenih klauzula”, nego uključuje i korekciju koja favorizira zadovoljavanje klauzula koje su često problematične.

Intuicija:

• ako neka klauzula često ostaje nezadovoljena, želim da algoritam počne “više mariti” za nju
• time se ublaži tipičan problem gdje hill climbing ide u slijepu ulicu jer stalno optimizira “lako zadovoljive” dijelove

4) GSAT

Klasičan lokalni SAT algoritam:

• u svakoj iteraciji flipam onu varijablu koja najviše smanjuje broj nezadovoljenih klauzula
• radi se s više restartova (pokušaja) i ograničenim brojem flipova

GSAT je često dobar kompromis: jednostavan, ali znatno robusniji od čistog hill-climbinga.

5) WalkSAT (random walk + greedy)

Ovo mi je jedna od dražih heuristika jer jako jasno pokazuje zašto “malo šuma” pomaže:

• odaberem jednu nezadovoljenu klauzulu
• s vjerojatnošću P flipam slučajnu varijablu iz klauzule (random walk)
• inače flipam varijablu koja daje najbolji lokalni napredak (greedy)

Time algoritam ima mehanizam za izlazak iz lokalnih optimuma bez kompliciranja.

6) Iterated Local Search (ILS)

Ideja:

1. pokrenem lokalnu pretragu (hill climbing) → dobijem lokalno dobro rješenje
2. napravim perturbaciju (flippam dio varijabli)
3. opet lokalna pretraga
4. ako je novo bolje, prihvati (ili zadrži najbolje)

Ovo je praktično hill climbing + kontrolirani reset i često radi iznenađujuće dobro.

Rezultati (uf50-010)

Svaki algoritam sam pokrenuo 20 puta (različiti slučajni startovi). U tablici je wall-clock vrijeme jedne izvedbe.

*Napomena za Hil climbing: kad uspije, medijan je 4.56 s; kad ne uspije, medijan je 56.51 s.

Opažanja

• WalkSAT je uvjerljivo najbrži u ovom eksperimentu: mali medijan i relativno “kruta” distribucija vremena. U praksi mi to izgleda kao najbolji omjer brzine i pouzdanosti na UF50.
• Osnovni hill climbing je “hit or miss”. Ako slučajno krene u dobar bazen atrakcije, riješi brzo; ako zapne, zna potrošiti puno vremena bez rješenja.
• Weighted hill lijepo pokazuje koliko mala promjena u score funkciji može promijeniti stabilnost: ovdje je 20/20 uspjeha, ali i dalje s vidljivom varijansom.
• GSAT radi pouzdano, ali prosječno sporije od Weighted hilla i osjetno sporije od WalkSAT-a. Rekao bih da je to cijena sistematičnijeg biranja flipova.
• ILS ima dobar medijan, ali težak rep (par pokretanja ode ekstremno dugo). To obično znači da bi vrijedilo dodatno tunati perturbaciju (koliko bitova flipati, koliko puta, kad resetirati).

Dodatna zanimljivost: pronađene dodjele su različite (postoji više zadovoljavajućih rješenja), što je vidljivo po različitim 50-bitnim izlazima među pokretanjima.

Zaključak

Za ovu instancu i ovu implementaciju, WalkSAT mi je najpraktičniji izbor: brz je i stabilan kroz ponavljanja. Hill climbing bez mehanizma bijega iz lokalnih optimuma nije dovoljno pouzdan, dok ILS može biti odličan, ali traži tunanje kako bi se izbjegli ekstremni “spori” slučajevi.

Ako ovo budem dalje širio, sljedeći koraci bi mi bili:

• automatizirano tunanje parametara (P, broj flipova, perturbation rate),
• mjerenje i na više UF instanci (ne samo uf50-010),
• i usporedba s jednim pravim SAT solverom kao baseline (čisto za osjećaj razlike).

← Natrag Repo →