Vervulbaarheid

Uit Wikipedia, de vrije encyclopedie
Ga naar: navigatie, zoeken

In de klassieke logica is een propositie vervulbaar als er een toekenning, waar of onwaar, bestaat van de atomaire formules in die propositie zodat de propositie waar is. Als er geen toekenning bestaat, dan is de propositie onvervulbaar. Een onvervulbare propositie wordt ook wel een contradictie genoemd. De vervulbaarheid van een formule kan bijvoorbeeld met een waarheidstabel worden gecontroleerd.

Voorbeelden[bewerken]

Voorbeelden van vervulbare formules zijn:

A \vee \neg B
A \vee \neg A (een tautologie, deze formule is altijd waar)

Voorbeelden van onvervulbare formules zijn:

P \wedge \neg P
P \wedge \neg Q \wedge (P \rightarrow Q)

Een onvervulbare formule staat ook bekend als een contradictie.

Vervulbaarheidsproblemen[bewerken]

1rightarrow blue.svg Zie Vervulbaarheidsprobleem voor het hoofdartikel over dit onderwerp.

Het vervulbaarheidsprobleem, ook bekend als SAT, uit de complexiteitstheorie bestaat uit het beslissen of een gegeven formule wel of niet vervulbaar is. Voor het vervulbaarheidsprobleem bestaan allerlei algoritmen, zoals resolutie en het DPLL-algoritme. Uit bepaalde representaties, zoals een binair beslissingsdiagram, kan ook de vervulbaarheid van een propositie worden afgelezen. Het vervulbaarheidsprobleem is NP-volledig en het eerste probleem waarvoor NP-volledigheid werd aangetoond. Een ander vervulbaarheidsprobleem is Horn-vervulbaarheid (HORNSAT) waarbij de vervulbaarheid van een conjunctie van Horn-clausules bekeken wordt.

Er bestaan allerlei varianten van het vervulbaarheidsprobleem, zoals het vervullen van formules in conjunctieve normaalvorm (CNF-SAT). Hier kan men ook onderscheid maken naar het aantal literalen dat voorkomt in de clausules van de formule in conjunctieve normaalvorm. Gangbare vormen zijn 2-SAT met twee literalen per clausule en 3-SAT met drie literalen of meer algemeen, k-SAT met k literalen per clausule. Een gerelateerd probleem is MAX-SAT waarbij wordt gezocht naar het maximale aantal clausules dat kan worden vervuld.[1] Deze voorwaarden kunnen worden gecombineerd; op deze manier verkrijgt men problemen als MAX 3-SAT waarbij wordt gezocht naar het maximale aantal clausules dat kan worden vervuld in een formule in conjunctieve normaalvorm met drie literals per clausule.

Bronnen, noten en/of referenties