Heuristik för boolesk tillfredsställelsealgoritm

Det booleska tillfredsställbarhetsproblemet (ofta förkortat SAT) kan formellt anges som: givet ett booleskt uttryck $B$ med $V=\{v_{0},\ldots ,v_{n}\}$ variabler, hitta en tilldelning $V^{*}$ för variablerna så att $B(V^{*})$ är sann. Det ses som det kanoniska NP-kompletta problemet. Även om ingen effektiv algoritm är känd för att lösa detta problem i det allmänna fallet, finns det vissa heuristiker , informellt kallade "tumregler" i programmering, som vanligtvis kan hjälpa till att lösa problemet någorlunda effektivt.

Även om ingen känd algoritm är känd för att lösa SAT i polynomtid, finns det klasser av SAT-problem som har effektiva algoritmer som löser dem. Dessa klasser av problem uppstår från många praktiska problem i AI-planering , kretstestning och mjukvaruverifiering. Forskning om att konstruera effektiva SAT-lösare har baserats på olika principer såsom upplösning , sökning, lokal sökning och slumpmässig vandring, binära beslut och Stalmarcks algoritm. Vissa av dessa algoritmer är deterministiska , medan andra kan vara stokastiska .

Eftersom det finns polynom-tidsalgoritmer för att konvertera alla booleska uttryck till konjunktiv normal form, såsom Tseitins algoritm, förändrar inte SAT-problem i CNF deras beräkningssvårigheter. SAT-problem uttrycks kanoniskt i CNF eftersom CNF har vissa egenskaper som kan hjälpa till att beskära sökutrymmet och påskynda sökprocessen.

Förgreningsheuristik i konfliktdrivna algoritmer

En av hörnstenarna för konfliktdrivna klausuler för att lära sig SAT-lösare är DPLL-algoritmen . Algoritmen fungerar genom att iterativt tilldela fria variabler, och när algoritmen stöter på en dålig tilldelning, går den tillbaka till en tidigare iteration och väljer en annan tilldelning av variabler. Den förlitar sig på en förgreningsheuristik för att välja nästa gratis variabeltilldelning; grenalgoritmen gör effektivt valet av variabeltilldelningen till ett beslutsträd. Olika implementeringar av denna heuristik producerar markant olika beslutsträd och har således betydande effekt på lösarens effektivitet.

Tidig förgreningsheuristik (Bohms heuristik, maximala förekomster på minimistorlekssatser heuristisk och Jeroslow-Wang-heuristik) kan betraktas som giriga algoritmer . Deras grundläggande utgångspunkt är att välja en fri variabeltilldelning som kommer att tillfredsställa de mest redan otillfredsställda satserna i det booleska uttrycket. Men eftersom booleska uttryck blir större, mer komplicerade eller mer strukturerade, lyckas inte dessa heuristiker fånga användbar information om dessa problem som kan förbättra effektiviteten; de fastnar ofta i lokala maxima eller tar inte hänsyn till fördelningen av variabler. Dessutom kräver större problem mer bearbetning, eftersom operationen med att räkna fria variabler i otillfredsställda satser dominerar körtiden.

En annan heuristik som kallas Variable State Independent Decaying Sum (VSIDS) försöker att poängsätta varje variabel. VSIDS börjar med att titta på små delar av det booleska uttrycket och tilldela varje fas av en variabel (en variabel och dess negerade komplement) en poäng som är proportionell mot antalet satser som variabelfasen är i. Allt eftersom VSIDs fortskrider och söker igenom fler delar av den booleska uttryck, periodiskt delas alla poäng med en konstant. Detta diskonterar effekten av förekomsten av variabler i tidigare hittade klausuler till förmån för variabler med en större närvaro i nyare klausuler. VSIDS kommer att välja den variabla fasen med högst poäng för att avgöra var den ska förgrena sig.

VSIDs är ganska effektivt eftersom poängen för variabla faser är oberoende av den aktuella variabeltilldelningen, så att backtracking är mycket lättare. Vidare garanterar VSIDS att varje variabeltilldelning uppfyller det största antalet nyligen sökta segment av det booleska uttrycket.

Stokastiska lösare

MAX-SAT (versionen av SAT där antalet nöjda klausuler maximeras) kan också lösas med hjälp av probabilistiska algoritmer. Om vi ​​får ett booleskt uttryck $B$ , med $V=\{v_{0},\ldots ,v_{n}\}$ variabler och vi ställ in varje variabel slumpmässigt, sedan varje sats $c$ , med $|c|$ -variabler, har en chans att bli tillfredsställda av en viss variabeltilldelning Pr( $c$ är uppfylld) = $1-2^{-|c|}$ . Detta beror på att varje variabel i $c$ har ${\frac {1}{2}}$ sannolikhet att vara nöjd, och vi behöver bara en variabel i $c$ för att vara nöjd . Detta fungerar $\forall ~|c|\geq 1$ , så Pr( $c$ är uppfylld) = $1-2^{-|c|}\geq {\frac {1}{2}}$ .

Nu visar vi att slumpmässig tilldelning av variabelvärden är en ${\frac {1}{2}}$ -approximationsalgoritm, vilket betyder att det är en optimal approximationsalgoritm om inte P = NP. Antag att vi får ett booleskt uttryck $B=\{c_{i}\}_{i=1}^{n}$ och

$\delta _{ij}={\begin{cases}0&{\text{if }}c_{i}{\text{ är nöjd}},\\1&{\text{if }}c_{i }{\text{ är inte tillfredsställd}}.\end{cases}}$

${\begin{aligned}E[{\text{Num-satser uppfyllda}}]&=\summa _{i}E[\delta _{i}]=\summa _{i }1-2^{-|c_{i}|}\\&\geq \sum _{i}{\frac {1}{2}}={\frac {1}{2}}|i|= {\frac {1}{2}}OPT\end{aligned}}$

Denna algoritm kan inte optimeras ytterligare av PCP-satsen om inte P = NP.

Andra Stokastiska SAT-lösare, såsom WalkSAT och GSAT , är en förbättring av ovanstående procedur. De börjar med att slumpmässigt tilldela värden till varje variabel och går sedan igenom det givna booleska uttrycket för att identifiera vilka variabler som ska vändas för att minimera antalet otillfredsställda satser. De kan slumpmässigt välja en variabel att vända eller välja en ny slumpvariabeltilldelning för att undkomma lokala maxima, ungefär som en simulerad glödgningsalgoritm .

2-SAT heuristik

Till skillnad från allmänna SAT-problem kan 2-SAT- problem lösas . Det finns algoritmer som kan beräkna tillfredsställelsen av ett 2-SAT-problem i polynomtid. Detta är ett resultat av begränsningen att varje sats bara har två variabler, så när en algoritm ställer in en variabel ${\displaystyle v_{i}} ,$ tillfredsställelsen av satser, som innehåller $v_{i}$ men inte är nöjda med den variabeltilldelningen, beror på tillfredsställelsen av den andra variabeln i dessa satser, vilket bara lämnar en möjlig tilldelning för dessa variabler.

Backtracking

Antag att vi ges ett booleskt uttryck:

$B_{1}=(v_{3}\lor \neg v_{2})\wedge (\neg v_{ 1}\lor \neg v_{3})$

$B_{2}=(v_{3}\lor \neg v_{2})\wedge (\neg v_{1}\lor \neg v_{3})\wedge (\neg v_{1}\ lor v_{2}).$

Med $B_{1}$ kan algoritmen välja ${\displaystyle v_{1}={\text{true}}} ,$ så för att uppfylla den andra klausulen måste algoritmen ställas in ${\displaystyle v_{3}={\text{false}}} ,$ och för att uppfylla den första satsen kommer algoritmen att sätta $v_{2}={\text{false }}$ .

Om algoritmen försöker uppfylla $B_{2}$ på samma sätt som den försökte lösa $B_{1}$ , kommer den tredje satsen att förbli otillfredsställd. Detta kommer att få algoritmen att backa och ställa in $v_{1}={\text{false}}$ och fortsätta att tilldela variabler.

Grafförminskning

2-SAT-problem kan också reduceras till att köra en djup-först-sökning på en starkt ansluten komponenter i en graf. Varje variabel fas (en variabel och dess negerade komplement) är kopplad till andra variabla faser baserat på implikationer. På samma sätt när algoritmen ovan försökte lösa

$B_{1},v_{1}={\text{true}}\implies v_{3}={\text{false}}\implies v_{2}={\text{false}}\implies v_{1}={\text{true}}.$

Men när algoritmen försökte lösa

${\begin{aligned}B_{2},v_{1}={ \text{true}}&\implies v_{3}={\text{false}}\implies v_{2}={\text{false}}\\&\implies v_{1}={\text{false }}\implies \cdots \implies v_{1}={\text{true}},\end{aligned}}$

vilket är en motsägelse.

När ett 2-SAT-problem har reducerats till en graf, om en djupsökning först hittar en starkt ansluten komponent med båda faserna av en variabel, är 2-SAT-problemet inte tillfredsställbart. På samma sätt, om den första sökningen på djupet inte hittar en starkt ansluten komponent med båda faserna av en variabel, är 2-SAT-problemet tillfredsställbart.

Viktade SAT-problem

Det finns många viktade SAT-problem som optimeringsversioner av det allmänna SAT-problemet. I denna klass av problem får varje sats i ett CNF booleskt uttryck en vikt. Målet är att maximera eller minimera den totala summan av vikterna av de uppfyllda klausulerna givet ett booleskt uttryck. viktad Max-SAT är maximeringsversionen av detta problem, och Max-SAT är en instans av viktat MAX-SAT-problem där vikterna för varje sats är desamma. Det partiella Max-SAT-problemet är problemet där vissa satser nödvändigtvis måste vara uppfyllda (hårda satser) och summan av vikterna för resten av klausulerna (mjuka satserna) ska maximeras eller minimeras, beroende på problemet. Partiell Max-SAT representerar en mellanhand mellan Max-SAT (alla satser är mjuka) och SAT (alla satser är svåra).

Observera att de stokastiska probabilistiska lösarna också kan användas för att hitta optimala approximationer för Max-SAT.

Variabel delning

Huvudartikel: Variabel delning

Variabel uppdelning är ett verktyg för att hitta övre och nedre gränser för ett Max-SAT-problem. Det innebär att dela upp en variabel $a$ i nya variabler för alla utom en gång förekomsten av $a$ i det ursprungliga booleska uttrycket. Till exempel, givet det booleska uttrycket: $B=(a\lor b\lor c) \wedge (\neg a\lor e\lor \neg b)\wedge (a\lor \neg c\lor f)$ blir: $B^{*}=(a\lor b\lor c)\wedge (\neg a_{1}\lor e\lor \neg b)\ kil (a_{2}\lor \neg c\lor f)$ , med $a,a_{1},a_{2},\ldots ,a_{ n}$ är alla distinkta variabler.

Detta mildrar problemet genom att introducera nya variabler i det booleska uttrycket, vilket har effekten att ta bort många av begränsningarna i uttrycket. Eftersom varje tilldelning av variabler i $B$ kan representeras av en tilldelning av variabler i $B^{*}$ , minimering och maximering av vikterna av $B^{* }$ representerar nedre och övre gränser för minimering och maximering av vikterna för $B$ .

Partiell Max-SAT

Partiell Max-SAT kan lösas genom att först överväga alla hårda klausuler och lösa dem som en instans av SAT. Den totala maximala (eller lägsta) vikten av de mjuka klausulerna kan utvärderas med den variabeltilldelning som krävs för att uppfylla de hårda klausulerna och försöker optimera de fria variablerna (de variabler som tillfredsställelsen av de hårda klausulerna inte beror på). Det senare steget är en implementering av Max-SAT givet några fördefinierade variabler. Naturligtvis kan olika variabeltilldelningar som uppfyller de hårda satserna ha olika optimala fria variabeltilldelningar, så det är nödvändigt att kontrollera olika tilldelningar av hårda satser tillfredsställelsevariabel.

Datastrukturer för lagring av klausuler

När SAT-lösare och praktiska SAT-problem (t.ex. kretsverifiering) blir mer avancerade, kan de booleska intresseanmälningarna överstiga miljontals variabler med flera miljoner satser; därför måste effektiva datastrukturer användas för att lagra och utvärdera klausulerna.

Uttryck kan lagras som en lista med satser, där varje sats är en lista med variabler, ungefär som en adjacency-lista . Även om dessa datastrukturer är bekväma för manipulation (lägga till element, ta bort element, etc.), förlitar de sig på många pekare, vilket ökar deras minneskostnader, minskar cache-lokaliteten och ökar cachemissarna , vilket gör dem opraktiska för problem med stora klausuler och stora klausulstorlekar.

När satsstorlekar är stora inkluderar mer effektiva analoga implementeringar att lagra uttryck som en lista med satser, där varje sats representeras som en matris som representerar satserna och variablerna som finns i den satsen, ungefär som en närliggande matris . Elimineringen av pekare och den sammanhängande minnesockupationen av arrayer tjänar till att minska minnesanvändningen och öka cachelokaliteten och cacheträffarna, vilket erbjuder en körtidshastighet jämfört med den tidigare nämnda implementeringen.