1. Problemen weergeven als Booleaanse formules:

* Codering: Het kernidee van het gebruik van SAT-oplossers is coderen een bepaald probleem (bijvoorbeeld planning, circuitontwerp, planning) in een Booleaanse formule in Conjunctive Normal Form (CNF). Dit omvat het identificeren van de beslissingsvariabelen van het probleem en het weergeven van de beperkingen op deze variabelen als logische clausules. Het mooie ligt in het feit dat in dit formaat een grote verscheidenheid aan problemen kan worden uitgedrukt.

* Conjunctieve normale vorm (CNF): Bijna alle SAT-oplossers werken met formules in CNF. CNF is een logische formule die een conjunctie (AND) is van clausules, waarbij elke clausule een disjunctie (OR) is van letterlijke waarden. Een letterlijke is een variabele of de ontkenning ervan. Bijvoorbeeld:`(x OF NIET y OF z) EN (NIET x OF y)`. Door lid te zijn van CNF wordt het zoekproces gestructureerder en efficiënter.

2. Davis-Putnam-Logemann-Loveland (DPLL) algoritme:

* Op zoek gebaseerde aanpak: DPLL is het fundamentele algoritme voor het oplossen van SAT-problemen. Het is een compleet zoekalgoritme dat systematisch de ruimte van mogelijke variabeletoewijzingen verkent.

* Besluit: Het algoritme kiest een variabele die momenteel niet is toegewezen en wijst deze 'TRUE' of 'FALSE' toe. Deze keuze creëert twee takken in de zoekboom.

* Eenheidsvoortplanting: Nadat een beslissing is genomen, voert DPLL eenheidspropagatie uit. Een eenheidsclausule is een clausule die slechts één niet-toegewezen letterlijke waarde bevat. Als er een eenheidsclausule bestaat (bijvoorbeeld `x`), *moet* het algoritme de variabele `x` toewijzen aan de waarde die de clausule waar maakt (in dit geval `x =TRUE`). De voortplanting van eenheden kan in cascade plaatsvinden, wat leidt tot verdere toewijzing van variabelen. Dit is van cruciaal belang om het probleem te vereenvoudigen en onnodig zoeken te voorkomen.

* Pure letterlijke eliminatie: Een zuivere letterlijke waarde is een letterlijke waarde die in slechts één polariteit (positief of negatief) in de formule voorkomt. Als er een zuivere letterlijke waarde bestaat, kan hieraan een waarde worden toegewezen om ervoor te zorgen dat alle clausules die deze waarde bevatten waar zijn. Dit vereenvoudigt de formule zonder de vervulbaarheid aan te tasten.

* Teruggaan: Als een tak van de zoekopdracht tot een conflict leidt (d.w.z. een clausule wordt onwaar), *gaat het algoritme *terug*. Dit betekent dat je de laatste beslissing ongedaan maakt en de tegenovergestelde opdracht probeert. Het hele proces gaat door totdat er een bevredigende opdracht is gevonden (de formule is SAT) of alle mogelijke opdrachten zijn uitgeput (de formule is UNSAT).

3. Conflictgestuurd leren van clausules (CDCL):

* Leren van conflicten: Moderne SAT-oplossers zijn gebaseerd op CDCL, een uitbreiding van DPLL. De belangrijkste innovatie is dat wanneer zich een conflict voordoet, de oplosser de redenen voor het conflict analyseert en een nieuwe clausule leert (een conflictclausule) die voorkomt dat hetzelfde conflict zich in de toekomst opnieuw voordoet.

* Conflictanalyse: Het proces van conflictanalyse maakt gebruik van de implicatiegrafiek (een grafiek die de afhankelijkheden tussen variabele toewijzingen weergeeft) om een ​​subset van de beslissingen te bepalen die tot het conflict hebben geleid.

* Clausule leren: De conflictclausule wordt aan de formule toegevoegd, meestal met behulp van het "First Unique Implication Point (UIP)" -schema. De resulterende clausule is een logisch gevolg van de oorspronkelijke formule, dus het toevoegen ervan verandert niets aan de vervulbaarheid.

* Niet-chronologische backtracking (backjumping): CDCL-oplossers kunnen niet-chronologisch teruggaan. In plaats van alleen maar de laatste beslissing ongedaan te maken, kunnen ze terugspringen naar een eerder beslissingsniveau dat verantwoordelijk was voor het conflict. Hierdoor kan de oplosser de zoekruimte efficiënter verkennen.

* Clausuleverwijdering: Om te voorkomen dat de formule te groot wordt, verwijderen oplossers periodiek enkele van de geleerde clausules. Heuristieken worden gebruikt om te beslissen welke clausules moeten worden verwijderd, waarbij de noodzaak om nuttige informatie te onthouden in evenwicht wordt gebracht met de noodzaak om de formule beheersbaar te houden.

4. Variabele ordeningsheuristieken (vertakkingsheuristieken):

* Impact op efficiëntie: De volgorde waarin variabelen worden geselecteerd voor besluitvorming (vertakking) heeft een dramatische invloed op de prestaties van SAT-oplossers. Goede heuristieken kunnen de omvang van de zoekboom aanzienlijk verkleinen.

* VSIDS (variabele staatsonafhankelijke vervalsom): Een populaire heuristiek is VSIDS. Er wordt een score bijgehouden voor elke variabele, die wordt verhoogd wanneer de variabele bij een conflict betrokken is. De scores worden periodiek verslechterd, waarbij de voorkeur wordt gegeven aan variabelen die recentelijk bij conflicten betrokken zijn geweest. Deze heuristiek richt de zoekopdracht op de "actieve" delen van de formule.

* Andere heuristieken: Andere heuristieken houden rekening met de frequentie van variabelen in clausules, het aantal onopgeloste clausules die een variabele bevatten, of gebruiken machine learning-technieken om vertakkingsstrategieën te leren.

5. Heuristieken voor clausulevolgorde:

* Eenheidsvoortplanting begeleiden: De volgorde waarin clausules in aanmerking worden genomen voor eenheidspropagatie kan ook de prestaties beïnvloeden.

* Letterlijke waarden bekeken: De meeste oplossers gebruiken een techniek die 'watched literals' wordt genoemd. Voor elke clausule worden twee letterlijke waarden gekozen als 'bewaakt'. Eenheidsvoortplanting hoeft alleen te worden geactiveerd wanneer een van de bekeken letterlijke waarden onwaar wordt. Hierdoor wordt het aantal clausules dat moet worden onderzocht aanzienlijk verminderd.

6. Strategieën voor opnieuw opstarten:

* Ontsnappen aan lokale minima: CDCL-oplossers kunnen soms vastlopen in een deel van de zoekruimte dat moeilijk te verkennen is. Het periodiek herstarten van de solver kan helpen om aan deze lokale minima te ontsnappen.

* Herstart op basis van glucose: Moderne oplossers gebruiken vaak herstartstrategieën op basis van de kwaliteit van de aangeleerde clausules. De Glucose-herstartstrategie herstart de oplosser bijvoorbeeld vaker wanneer deze veel clausules van lage kwaliteit leert.

7. Voor- en nabewerking:

* Vereenvoudiging van de formule: Voorbewerkingstechnieken worden op de formule toegepast *voordat* het hoofdzoekproces begint. Deze technieken zijn bedoeld om de formule te vereenvoudigen door overbodige clausules te verwijderen, variabelen te vervangen en andere logische transformaties uit te voeren.

* In verwerking: Inprocessingtechnieken worden *tijdens* het zoekproces toegepast. Deze technieken kunnen de formule dynamisch vereenvoudigen op basis van de huidige status van de zoekopdracht.

* Voorbeelden: Voorverwerking en inverwerking omvatten subsumptie (het verwijderen van clausules die logischerwijs worden geïmpliceerd door andere clausules), resolutie (het toevoegen van nieuwe clausules aan de formule op basis van bestaande clausules) en het elimineren van variabelen (het vervangen van een variabele door de definitie ervan).

8. Parallelle SAT-oplossing:

* Verdeel en heers: Parallelle SAT-oplossers maken gebruik van het parallellisme dat inherent is aan het zoekproces. Ze kunnen de zoekruimte in meerdere delen opsplitsen en deze tegelijkertijd verkennen.

* Portfoliobenaderingen: Een andere benadering is om meerdere verschillende SAT-oplossers (met verschillende parameterinstellingen) parallel te laten draaien, en te hopen dat een van hen snel een oplossing zal vinden.

* Clausule delen: Parallelle oplossers kunnen geleerde clausules tussen verschillende processen delen om de algehele zoekefficiëntie te verbeteren.

9. Theorie oplossen (SMT):

* Voorbij de Booleaanse logica: SAT-oplossers worden vaak gebruikt als kerncomponent van Satisfiability Modulo Theories (SMT)-oplossers. SMT-oplossers kunnen redeneren over formules die variabelen en beperkingen uit andere theorieën bevatten, zoals rekenkunde, tekenreeksen of arrays.

* SAT combineren met theoriespecifieke oplossers: SMT-oplossers gebruiken een combinatie van SAT-oplossingstechnieken en theoriespecifieke oplossers om de vervulbaarheid van formules te bepalen.

Samenvattend draaien de belangrijkste principes van SAT-oplossingen om het efficiënt verkennen van de ruimte van mogelijke variabeletoewijzingen, het leren van conflicten om herhaling van fouten te voorkomen, en het vereenvoudigen van de formule om de zoekruimte te verkleinen. Moderne SAT-oplossers zijn zeer geavanceerde tools die problemen met miljoenen variabelen en clausules kunnen oplossen.