Satisfiabiliteit

Satisfiabiliteit, in het bijzonder satisfieerbaarheid van proposionele logica, verwijst naar de eigenschap van een proposionele formule om waar te worden onder een toewijzing van waarheidswaarden aan de variabelen. Een formule is satisfieerbaar als er zo’n toewijzing bestaat waardoor de formule waar wordt; is zo’n toewijzing er niet, dan is de formule niet satisfieerbaar. Vaak wordt CNF (conjunctieve normaalvorm) gebruikt omdat veel algoritmen en toepassingen CNF vereisen.

Het SAT-probleem (satisfiability) vraagt of een gegeven proposionele formule satisfieerbaar is. Het wordt vooral onderzocht wanneer de formule in CNF is weergegeven. Algemeen geldt: SAT is NP-compleet; speciale varianten als 3-SAT zijn ook NP-compleet, terwijl 2-SAT in lineaire tijd kan worden opgelost.

In de praktijk worden algoritmen zoals DPLL en CDCL gebruikt in moderne SAT-solveren. Deze solvers combineren backtracking met clausule-leren om efficiënte oplossingen te vinden, ook voor grote en complexe formules. Hoewel er waarschijnlijk geen polynomiaal algoritme voor alle gevallen bestaat, werken deze solvers vaak erg snel op realistische problemen.

Toepassingen van satisfiabiliteit zijn onder meer hardware- en softwareverificatie, formele specificatie, planning en constraint programming. SAT kan ook worden gebruikt als bouwsteen voor optimalisatie en voor het oplossen van puzzels en deductieve problemen.

Historisch gezien werd de NP-complete eigenschap van SAT in 1971 aangetoond door Stephen Cook (het Cook–Levin-theorema, met onafhankelijk werk van Leonid Levin). Het concept van satisfiability heeft sindsdien uitgebreid onderzoekers en toepassingen geïnspireerd.