Vervulbaarheidsprobleem

In de complexiteitstheorie verwijst het vervulbaarheidsprobleem (ook bekend als SAT, van het Engelse satisfiability) naar het bepalen of een logische propositie vervuld kan worden; een propositie kan vervuld worden als er een toekenning van waar of onwaar aan de atomaire formules bestaat zodanig dat de gehele propositie waar is.

Definitie

Het vervulbaarheidsprobleem is een beslissingsprobleem, een ja/nee-probleem, met als invoer een logische propositie. Het probleem is nu: bestaat er een toekenning van waar of onwaar aan de atomaire formules zodanig dat de gehele propositie waar is? De propositie $(p_{1}\vee p_{2})\wedge (\neg p_{1}\vee p_{3})\wedge (p_{2}\vee p_{5})$ is bijvoorbeeld vervulbaar want de propositie kan vervuld worden met p₂ = waar en p₃ = waar.

Veelgebruikte termen op dit gebied zijn:

• Literaal: een atomaire formule of de negatie ervan, bijvoorbeeld $p$ en $\neg p$.
• Clausule: een disjunctie van literals, bijvoorbeeld $p_{1}\vee p_{2}\vee \neg p_{3}$.
• Conjunctieve normaalvorm: een conjunctie van clausules, bijvoorbeeld $(p_{1}\vee p_{2})\wedge (\neg p_{1}\vee p_{3})\wedge (p_{2}\vee p_{5})$.

Toepassingen

Het kunnen oplossen van vervulbaarheidsproblemen is van belang in vele gebieden van de informatica, zoals theoretische informatica, algoritmiek, kunstmatige intelligentie, ontwerp van hardware en verificatie van hardware en software. Veel wiskundige en praktische problemen, zoals het kleuren van grafen en het plannen van taken, kunnen gecodeerd worden als een vervulbaarheidsprobleem. Hierbij geeft men een manier om het probleem te coderen als een logische propositie. Deze propositie kan bestudeerd worden door een algoritme dat de vervulbaarheid onderzoekt. Als de propositie vervulbaar blijkt dan bestaat er ook een oplossing voor het oorspronkelijke probleem.

Varianten

Er bestaan allerlei varianten van het vervulbaarheidsprobleem, zoals CNF-SAT (is een formule in conjunctieve normaalvorm vervulbaar?) of k-SAT (is een formule in conjunctieve normaalvorm met exact k literals per clausule vervulbaar?). Veel bestudeerde varianten van k-SAT zijn 2-SAT en 3-SAT. Aangezien elke propositionele formule omgeschreven kan worden naar conjunctieve normaalvorm, wordt veel onderzoek verricht naar het vervullen van formules in die vorm. Wanneer men de vervulbaarheid van een conjunctie van Horn-clausules onderzoekt, spreekt men van het probleem HORNSAT (Horn-vervulbaarheid).

Een gerelateerd probleem is MAX-SAT waarbij gezocht wordt naar het maximale aantal clausules in een formule in een conjunctieve normaalvorm dat vervuld kan worden. Deze voorwaarden kunnen gecombineerd worden; op deze manier verkrijgt men problemen als MAX-3-SAT waarbij gezocht wordt naar het maximale aantal clausules dat vervuld kan worden in een formule in conjunctieve normaalvorm met drie literals per clausule.

NP-volledigheid

Het vervulbaarheidsprobleem is een NP-volledig beslissingsprobleem. Het is tevens het eerste probleem waarvoor NP-volledigheid werd aangetoond, namelijk door Stephen Cook in 1971. Ook de variant waarbij men formules in conjunctieve normaalvorm beschouwt die exact drie literals hebben per clausule is NP-volledig (3-SAT). Het probleem 2-SAT is niet NP-volledig maar NL-volledig; het probleem 2-SAT kan ook in polynomiale tijd opgelost worden. Het probleem HORNSAT is P-volledig. Er bestaat hiervoor een algoritme dat het probleem in polynomiale tijd oplost.

Het probleem MAX-SAT is NP-moeilijk. De variant MAX-k-SAT is NP-moeilijk voor k ≥ 2.

Oplossen

Er bestaan allerlei algoritmen voor het oplossen van vervulbaarheidsproblemen, zoals resolutie en het DPLL-algoritme. Een computerprogramma of algoritme voor het oplossen van een vervulbaarheidsprobleem heet een SAT solver. Het is soms ook mogelijk om de vervulbaarheid van een logische formule te bepalen aan de hand van een representatie, zoals een binair beslissingsdiagram.

Enkele algoritmen en/of computerprogramma's zijn: BerkMin, Chaff, DPLL-algoritme, GRASP, march_dl, MiniSAT, POSIT, rel_sat, resolutie en SATO.

Twee gangbare aanpakken zijn "conflict-driven" en "look-ahead": bij conflict-driven detecteert men wanneer het vervullen niet meer mogelijk is en men keert terug naar een eerder punt in het algoritme om vanaf daar de zoektocht te vervolgen. Bij look-ahead tracht men de zoekruimte zo klein mogelijk te houden door vooruit te kijken. Dit is kostbaar qua rekentijd maar kan het algoritme wel in de richting van een goede oplossing sturen.

Lokaal zoeken

Er bestaan ook stochastische zoekalgoritmen voor het vervulbaarheidsprobleem, zoals GSAT, CSAT, WalkSAT en Novelty. Het is niet gegarandeerd dat deze algoritmen een oplossing zullen vinden als het bestaat. Het is ook niet mogelijk de onvervulbaarheid van een formule te bepalen met behulp van deze algoritmen (tenzij men alle mogelijke toekenningen onderzoekt). Deze algoritmen beschouwen toekenningen van waar of onwaar aan alle atomaire formules; dit is de zoekruimte van het algoritme. Door herhaaldelijk een waarheidswaarde om te draaien (door bijvoorbeeld p = waar om te zetten naar p = onwaar) tracht het algoritme meer clausules waar te maken. De algoritmen variëren in bijvoorbeeld welke atomaire formule gekozen wordt om de waarheidswaarde van te veranderen.

De algoritmen beginnen met een willekeurige toekenning van waar en onwaar en de waarheidswaarden worden een vooraf bepaald aantal keer veranderd. Als het niet gelukt is de gehele formule waar te maken, begint het algoritme opnieuw met een nieuwe willekeurige toekenning van waar of onwaar aan alle atomaire formules. De zoektocht begint dan opnieuw maar dan vanuit een ander startpunt in de zoekruimte.

Externe links

• (en) The international SAT Competitions web page, jaarlijkse wedstrijden
• (en) The International Conferences on Theory and Applications of Satisfiability Testing (SAT)

Bronnen, noten en/of referenties