Vervulbaarheid

In de klassieke propositielogica is een propositie vervulbaar als er een toekenning van waarheidswaardes aan de atomaire formules van die propositie bestaat zodat de propositie waar is. Als zo'n toekenning niet bestaat is de propositie onvervulbaar. Een onvervulbare propositie wordt wel een contradictie genoemd. De vervulbaarheid van een formule kan met een waarheidstabel worden gecontroleerd.

Voorbeelden

Voorbeelden van vervulbare formules zijn:

$A\lor \neg B$

$A\lor \neg A$ (een tautologie, deze formule is altijd waar)

Voorbeelden van onvervulbare formules zijn:

$P\land \neg P$

$P\land \neg Q\land (P\to Q)$

Een onvervulbare formule staat ook bekend als een contradictie.

Vervulbaarheidsproblemen

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. 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