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 propositie kan met een waarheidstabel worden gecontroleerd.

Voorbeelden

Voorbeelden van vervulbare proposities zijn:

$A\vee \mathrm{\neg }B$

$A\vee \mathrm{\neg }A$ Dit is een tautologie, deze propositie is altijd waar.

Voorbeelden van onvervulbare proposities zijn:

$P\wedge \mathrm{\neg }P$

$P\wedge \mathrm{\neg }Q\wedge (P\to Q)$

Een onvervulbare propositie staat ook bekend als een contradictie.

Vervulbaarheidsproblemen

Het vervulbaarheidsprobleem, ook bekend als SAT, uit de complexiteitstheorie bestaat uit het beslissen of een gegeven propositie 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 wordt bekeken.

Er bestaan allerlei varianten van het vervulbaarheidsprobleem, zoals het vervullen van proposities in conjunctieve normaalvorm (CNF-SAT). Hier kan men ook onderscheid maken naar het aantal literalen dat voorkomt in de clausules van de propositie 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 komen er problemen tevoorschijn als MAX 3-SAT waarbij wordt gezocht naar het maximale aantal clausules dat kan worden vervuld in een propositie in conjunctieve normaalvorm met drie literals per clausule.