Problém vážené splnitelnosti booleovské formule

Úloha z předmětu 36PAA

Martin Tůma

Zadání

Je dána booleovská formule F proměnnných X=(x1,x2,...,xn) v konjunktivní normální formě (tj. součin součtů). Dále jsou dány celočíselné kladné váhy W=(w1,w2,...,wn). Najděte ohodnocení Y=(y1,y2,...,yn) proměnných x1,x2,...,xn tak, aby F(Y)=1 a součet vah proměnných, které jsou ohodnoceny jedničkou, byl maximální.

Je přípustné se omezit na formule, v nichž má každá formule právě 3 literály (problém 3 SAT). Takto omezený problém je stejně těžký, ale možná se lépe programuje a lépe se posuzuje obtížnost instance (viz Selmanova prezentace [1]).

Řešení

Pro řešení problému byla, stejně jako v úloze 5 [2] zvolena iterativní heuristika - simulované ochlazování. Stručný popis metody je popsán v protokolu k úloze 5, podrobně pak problematiku popisuje například [3]. Teoretický rozbor řešení se tak nadále věnuje pouze vlastnostem specifickým pro daný problém (3 SAT).

Cenová funkce

Pro porovnání 2 stavů ze stavového prostoru úlohy je zapotřebí zkonstruovat funkci, která umí jednotlivé stavy kvalitativně ohodnotit. Na rozdíl od problému batohu si však u váženého 3 SATu nevystačíme s pouhým porovnáním dosažené váhy, ale v potaz je třeba brát i podmínku splnitelnosti formule. Navržena byla proto následující cenová funkce:

cenová funkce

kde CX je počet splněných klauzulí stavu X, Ctotal počet klauzulí formule F, WX váha stavu X a Wtotal suma vah všech proměnných formule F. Konstanta k1 nastavuje poměr vlivu kriterií (splnitelnost/max. váha) na výslednou cenu, konstanta k2 pak výslednou cenu upravuje vzhledem k použité teplotě ochlazování (je tedy spíše parametrem simulovaného ochlazování, než heuristické funkce).

Strategie nastavení parametrů

Při svých experimentech jsem nejprve hledal optimální parametry cenové funkce a až poté nastavoval ostatní parametry (výchozí a koncovou teplotu, počet "cyklů ekvilibria" a koeficient ochlazování). Při nastavování jsem vycházel ze zkušeností s nastavením parametrů u problému batohu. Stejně jako v případě batohu, i u váženého 3 SAT problému se nejlepším vodítkem pro nastavení parametrů ukázal být graf vývoje řešení (hodnoty lze z programu získat odkomentováním definice makra PROGRESS).

Pomocí něj lze pro danou třídu stejně velkých instancí nejlépe nastavit nutnou délku ochlazování tak, aby algoritmus na konci dokonvergoval k nějakému řešení, a následně podle výsledků donastavit počet "cyklů ekvilibria" (určuje "hustotu" testovaných stavů) tak, aby se výsledky blížily požadovaným.

Experimenty

Testovací data

Měření probíhala na souboru 50 instancí velikosti 20/75 (proměnné/klauzule) ke kterým jsou známa optimální řešení (práce Martina Prchlíka, kterému tímto děkuji). Dále pak (po změně parametrů) proběhla měření na menších souborech 10 instancí velikosti 75/325 a 100/430. Tyto testy jsou však jen orientační pro odhad možností metody, neboť u těchto instancí nejsou známa optimální řešení. Váhy pro všechny testovací soubory byly generovány jako náhodná čísla s rovnoměrným rozložením v intervalu <0,200>.

Všechny testovací úlohy byly získány modifikací1 příslušných úloh z DIMACS archivu [4] (názvy souborů odpovídají až na příponu původním datovým souborům z archivu)

1Formát je oproti originálnímu DIMACS cnf formátu poněkud upraven a vypadá takto: První řádka udává počet proměnných, počet klauzulí a počet proměnných na klauzuli. Poté následují jednotlivé klauzule - jedna na řádku - a nakonec řádek s váhami proměnných.

Naměřené hodnoty

Parametry cenové funkce

k1 [-] T [%] ηø [%] ηmax [%]
0.88 520.00 0.00
0.90 600.02 0.58
0.92 820.00 0.00
0.94 920.3810.20
0.961000.5512.44
0.981000.51 9.15

Graf 1: Závislost úspěšnosti nalezení řešení (T) a relativní chyby nalezených řešení na parametru k1 cenové funkce.

Výsledky potvrdily předpokládanou vysokou složitost nalezení vůbec nějakého řešení - koeficient k1 musí být pro správnou funkci heuristiky nastaven velmi vysoko. Pro další experimenty byla zvolena hodnota 0.95. Koeficient k2 byl "empiricky" - dle počtu příjmaných horších nových stavů (pozorovatelné v grafu vývoje řešení) - nastaven na hodnotu 1000.

Vývoj řešení

Výsledné nastavení parametrů algoritmu pro instance 20/75: Výchozí teplota: 1000, koncová teplota: 1, koeficient ochlazování: 0.85, počet iterací vnitřního cyklu: 1000. Grafy udávají vývoj instance uf20-01.3sat, nicméně u ostatních instancí je průběh obdobný.

[naměřená data].

Graf 2: Vývoj hodnoty cenové funkce aktuálního stavu řešení v závislosti na iteraci algoritmu.

Graf 3: Vývoj počtu splněných kluzulí aktuálního stavu řešení v závislosti na iteraci algoritmu.

Graf 4: Vývoj váhy aktuálního stavu řešení v závislosti na iteraci algoritmu.

Výsledky na instancích 20/75

S nastavením uvedeným v předchozích dvou částech dává program tyto výsledky: počet vyřešených instancí: 100%, průměrná relativní chyba: 0,35%, maximální relativní chyba: 10,20%.

Časová složitost na jednu instanci (aritmetický průměr) při tomto nastavení je na testovací konfiguraci: CPU Celeron M 1466MHz, OS Linux, GCC 4.2.0 (-O3 -march=pentium-m) 78ms.

Experimenty na "větších" instancích

U instancí velikosti 75/325 a 100/430 se ukázalo, že při zvoleném koeficientu k1=0.95 řeší program příliš malé procento instancí - <50% (a to prakticky nezávisle na nastavení ostatních parametrů v "rozumných" mezích). Na instancích 75/325 jsem proto provedl nové měření počtu nalezených řešení v závislosti na k1:

Nastavení algoritmu: výchozí teplota: 10000, koncová teplota: 0.1, cyklů ekvilibria: 5000, koeficient ochlazování: 0.9.

k10.950.960.97 0.980.991.00
T [%] 3040507060 70

Tabulka 1: Závislost úspěšnosti nalezení řešení instancí 75/325 na parametru k1 cenové funkce.

Graf 5: Vývoj počtu splněných kluzulí aktuálního stavu řešení v závislosti na iteraci algoritmu. (uf75-052.3sat, k1=0.98)

"Ideální" koeficient k1 pro instance 75/325 tedy leží okolo hodnoty 0.98. Výpočetní složitost jedné instance je při výše daném nastavení 3,5s.

Na instancích 100/425 pak bylo s nastavením: výchozí teplota: 10000, koncová teplota: 0.1, cyklů ekvilibria: 10000, koeficient ochlazování: 0.9 a k1: 0.98 dosaženo úspěšnosti 70% při časové složitosti 8.8s (106 navštívených stavů).

Graf 6: Vývoj počtu splněných kluzulí aktuálního stavu řešení při různé inicializaci generátoru náhodných čísel.

Závěr

Navržené řešení problému splnitelnosti vážené splnitelnosti booleovské formule je, minimálně pro "malé" instance, velice dobře použitelné. U instancí s 20 proměnnými a 75 klauzulemi byla úspěšnost vyřešení formulí 100% při průměrné relativní chybě řešení 0.35% a časové složitosti 78ms.

Pro větší instance (75/325 a 100/430) nalezl algoritmus řešení u 70% úloh s časovou složitostí 3,5s, respektivě 8.8s. Ohodnotit "kvalitu" řešení je však velmi obtížné, neboť optimální řešení nejsou známa.

Měření na těchto instancích ukázala (vynechání vlivu váhy nastavením k1 na 1), že již pouhé nalezení řešení booleovské formule je velmi složitý problém. Již řešení samotné formule existuje velice málo. Na druhou stranu lze předpokládat a za určitých předpokladů i dokázat2, že s rostoucím počtem proměnných budou nalezená neoptimální řešení při rovnoměrném rozložení vah stále blíže optimu.

2Pokud budeme ohodnocení proměnné ve formuli uvažovat jako náhodnou veličinu s alternativním rozdělením a p=1/2 bude se podle zákona velkých čísel počet 1 a počet 0 za předpokladu rovnoměrného rozdělení proměnných v klauzulích s rostoucím počtem proměnných n lišit stále méně a méně. Za předpokladu rovnoměrného rozdělení vah se pak suma vah (ohodnocení formule) bude s rostoucím n stále více blížit n/2·EXw a to jak u optimálního řešení, tak u nalezených neoptimálních řešení. Nalezené i optimální řešení tak budou s rostoucím n stále "blížeji u sebe".

Reference

[1] http://www.cs.cornell.edu/home/selman/papers-ftp/ai-phys1.ppt
[2] http://tumic.wz.cz/fel/online/36PAA/5/
[3] http://service.felk.cvut.cz/courses/36PAA/prez/PAA8ochl.pdf
[4] http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html

Přílohy

1. sat.c - Program pro řešení metodou simulovaného ochlazování.
2. stats.sh - Skript na výpočet statistik.
3. data.tar.bz2 - Archiv s testovacími daty.