Vervulbaarheid
In dit artikel zullen we alles met betrekking tot Vervulbaarheid onderzoeken. Van het historische belang tot de relevantie ervan in de huidige samenleving, via de vele facetten en toepassingen ervan. We zullen de impact ervan op verschillende gebieden gedetailleerd analyseren, evenals de controverses die het in de loop van de tijd heeft opgeroepen. We zullen leren over de meningen van experts en de ervaringen van degenen die de invloed ervan van dichtbij hebben ervaren. Vervulbaarheid is een spannend onderwerp en van groot belang voor het begrijpen van onze wereld. Daarom nodigen we je uit om je te verdiepen in deze volledige analyse die we voor je hebben voorbereid.
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:
- Dit is een tautologie, deze propositie is altijd waar.
Voorbeelden van onvervulbare proposities zijn:
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.[1] 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.