SAT-lösare

Inom datavetenskap och formella metoder är en SAT-lösare ett datorprogram som syftar till att lösa det booleska tillfredsställbarhetsproblemet . Vid inmatning av en formel över booleska variabler, såsom "( x eller y ) och ( x or not y )", matar en SAT-lösare ut om formeln är tillfredsställbar , vilket betyder att det finns möjliga värden på x och y som gör formeln sann , eller otillfredsställande, vilket betyder att det inte finns några sådana värden för x och y . I det här fallet är formeln tillfredsställbar när x är sant, så lösaren bör returnera "satisfiable". Sedan introduktionen av algoritmer för SAT på 1960-talet har moderna SAT-lösare vuxit till komplexa mjukvaruartefakter som involverar ett stort antal heuristiker och programoptimeringar för att fungera effektivt.

Genom ett resultat känt som Cook–Levin-satsen är boolesk tillfredsställelse ett NP-komplett problem i allmänhet. Som ett resultat är endast algoritmer med exponentiell värsta tänkbara komplexitet kända. Trots detta utvecklades effektiva och skalbara algoritmer för SAT under 2000-talet och har bidragit till dramatiska framsteg i vår förmåga att automatiskt lösa probleminstanser som involverar tiotusentals variabler och miljontals begränsningar.

SAT-lösare börjar ofta med att konvertera en formel till konjunktiv normalform . De är ofta baserade på kärnalgoritmer som DPLL-algoritmen , men innehåller ett antal tillägg och funktioner. De flesta SAT-lösare inkluderar time-outs, så de kommer att avslutas inom rimlig tid även om de inte kan hitta en lösning med en utgång som "okänt". Ofta ger SAT-lösare inte bara ett svar, utan kan ge ytterligare information inklusive en exempeltilldelning (värden för x , y , etc.) om formeln är tillfredsställbar eller minimal uppsättning otillfredsställande satser om formeln är otillfredsställande.

Moderna SAT-lösare har haft en betydande inverkan på områden inklusive programvaruverifiering , programanalys , begränsningslösning , artificiell intelligens , elektronisk designautomation och operationsforskning . Kraftfulla lösare är lätt tillgängliga som gratis och öppen källkodsprogramvara och är inbyggda i vissa programmeringsspråk, som att exponera SAT-lösare som begränsningar i programmering av begränsningslogik .

Översikt

DPLL-lösare

En DPLL SAT-lösare använder en systematisk bakåtspårningsprocedur för att utforska det (exponentiellt stora) utrymmet för variabla tilldelningar som letar efter tillfredsställande uppdrag. Den grundläggande sökproceduren föreslogs i två framstående tidningar i början av 1960-talet (se referenser nedan) och kallas nu vanligtvis för Davis–Putnam–Logemann–Loveland-algoritmen ("DPLL" eller "DLL"). Många moderna metoder för praktisk SAT-lösning härleds från DPLL-algoritmen och delar samma struktur. Ofta förbättrar de bara effektiviteten för vissa klasser av SAT-problem, såsom instanser som förekommer i industriella applikationer eller slumpmässigt genererade instanser. Teoretiskt har exponentiella nedre gränser bevisats för DPLL-familjen av algoritmer. ^{[ citat behövs ]}

Algoritmer som inte ingår i DPLL-familjen inkluderar stokastiska lokala sökalgoritmer . Ett exempel är WalkSAT . Stokastiska metoder försöker hitta en tillfredsställande tolkning men kan inte härleda att en SAT-instans är otillfredsställande, i motsats till kompletta algoritmer, såsom DPLL.

Däremot ställer randomiserade algoritmer som PPSZ-algoritmen av Paturi, Pudlak, Saks och Zane variabler i en slumpmässig ordning enligt vissa heuristiker, till exempel upplösning med begränsad bredd . Om heuristiken inte kan hitta rätt inställning tilldelas variabeln slumpmässigt. PPSZ-algoritmen har en körtid ^{[ clarify ]} på $O(1.308^{n})$ för 3-SAT. Detta var den mest kända körtiden för detta problem fram till 2019, då Hansen, Kaplan, Zamir och Zwick publicerade en modifiering av den algoritmen med en körtid på O ( $displaystyle O(1.307^{n})}$ för 3 -SAT. Den senare är för närvarande den snabbaste kända algoritmen för k-SAT vid alla värden på k. I miljön med många tillfredsställande uppdrag har den randomiserade algoritmen av Schöning en bättre gräns.

CDCL-lösare

Moderna SAT-lösare (utvecklade på 2000-talet) finns i två varianter: "konfliktdrivna" och "blick framåt". Båda tillvägagångssätten härstammar från DPLL. Konfliktdrivna lösare, såsom konfliktdriven klausulinlärning (CDCL), utökar den grundläggande DPLL-sökningsalgoritmen med effektiv konfliktanalys, klausulinlärning, icke-kronologisk bakåtspårning (aka backjumping ), såväl som "två-bevakade bokstaver"-enhet utbredning, adaptiv förgrening och slumpmässiga omstarter. Dessa "extra" till den grundläggande systematiska sökningen har empiriskt visat sig vara väsentliga för att hantera de stora SAT-instanser som uppstår inom elektronisk designautomation (EDA). Välkända implementeringar inkluderar Chaff och GRASP . Framtidslösare har särskilt stärkt reduktionerna (som går längre än enhetsklausulutbredning) och heuristiken, och de är generellt sett starkare än konfliktdrivna lösare på hårda instanser (medan konfliktdrivna lösare kan vara mycket bättre på stora instanser som faktiskt har en lätt instans inuti).

Den konfliktdrivna MiniSAT, som var relativt framgångsrik vid 2005 års SAT-tävling, har bara cirka 600 rader kod. En modern Parallell SAT-lösare är ManySAT. Det kan uppnå superlinjära hastigheter på viktiga problemklasser. Ett exempel för framtidslösare är march_dl, som vann ett pris vid 2007 års SAT-tävling. Googles CP-SAT-lösare, en del av OR-Tools , vann guldmedaljer vid Minizinc constraint-programmeringstävlingarna 2018, 2019, 2020 och 2021.

Vissa typer av stora slumpmässigt tillfredsställande instanser av SAT kan lösas genom undersökningsförökning (SP). ^{[ citat behövs ]} Särskilt i hårdvarudesign och verifieringstillämpningar bestäms ibland tillfredsställelse och andra logiska egenskaper hos en given propositionsformel baserat på en representation av formeln som ett binärt beslutsdiagram (BDD).

Olika SAT-lösare kommer att tycka att olika instanser är lätta eller svåra, och vissa utmärker sig på att bevisa otillfredsställelse och andra på att hitta lösningar. Alla dessa beteenden kan ses i SAT-lösningstävlingarna.

Parallell SAT-lösning

Parallella SAT-lösare finns i tre kategorier: portfölj, dela-och-härska och parallella lokala sökalgoritmer . Med parallella portföljer körs flera olika SAT-lösare samtidigt. Var och en av dem löser en kopia av SAT-instansen, medan divide-and-conquer-algoritmer delar problemet mellan processorerna. Det finns olika tillvägagångssätt för att parallellisera lokala sökalgoritmer.

International SAT Solver Competition har ett parallellt spår som återspeglar de senaste framstegen inom parallell SAT-lösning. Under 2016, 2017 och 2018 kördes riktmärkena på ett delat minnessystem med 24 bearbetningskärnor , därför kan lösare avsedda för distribuerat minne eller många kärnprocessorer ha misslyckats.

Portföljer

I allmänhet finns det ingen SAT-lösare som presterar bättre än alla andra lösare på alla SAT-problem. En algoritm kan fungera bra för problem som andra kämpar med, men kommer att göra sämre med andra instanser. Dessutom, givet en SAT-instans, finns det inget tillförlitligt sätt att förutsäga vilken algoritm som kommer att lösa denna instans särskilt snabbt. Dessa begränsningar motiverar den parallella portföljmetoden. En portfölj är en uppsättning olika algoritmer eller olika konfigurationer av samma algoritm. Alla lösare i en parallell portfölj körs på olika processorer för att lösa samma problem. Om en lösare avslutas, rapporterar portföljlösaren att problemet är tillfredsställande eller otillfredsställande enligt denna lösare. Alla andra lösare avslutas. Att diversifiera portföljer genom att inkludera en mängd olika lösare, som var och en presterar bra på olika problem, ökar lösarens robusthet.

Många lösare använder internt en slumptalsgenerator . Att diversifiera sina frön är ett enkelt sätt att diversifiera en portfölj. Andra diversifieringsstrategier involverar att aktivera, inaktivera eller diversifiera vissa heuristiker i den sekventiella lösaren.

En nackdel med parallella portföljer är mängden dubbelarbete. Om satsinlärning används i de sekventiella lösarna kan delning av inlärda satser mellan lösare som körs parallellt minska dubbelarbete och öka prestandan. Men till och med bara att köra en portfölj av de bästa lösarna parallellt blir en konkurrenskraftig parallelllösare. Ett exempel på en sådan lösare är PPfolio. Den designades för att hitta en nedre gräns för den prestanda som en parallell SAT-lösare ska kunna leverera. Trots den stora mängden dubbelarbete på grund av bristen på optimeringar, presterade den bra på en delad minnesmaskin. HordeSat är en parallell portföljlösare för stora kluster av datornoder. Den använder olika konfigurerade instanser av samma sekventiella lösare i sin kärna. Speciellt för hårda SAT-instanser kan HordeSat producera linjära hastigheter och därför minska körtiden avsevärt.

Under de senaste åren har SAT-lösare av parallellportföljer dominerat parallellbanan för International SAT Solver-tävlingar. Anmärkningsvärda exempel på sådana lösare inkluderar Plingeling och smärtfri-mcomsps.

Söndra och erövra

I motsats till parallella portföljer försöker parallell divide-and-conquer dela upp sökutrymmet mellan bearbetningselementen. Dela-och-härska-algoritmer, såsom den sekventiella DPLL, tillämpar redan tekniken att dela upp sökutrymmet, därför är deras förlängning mot en parallell algoritm rakt fram. Men på grund av tekniker som enhetsutbredning, efter en uppdelning, kan de partiella problemen skilja sig avsevärt i komplexitet. Således bearbetar DPLL-algoritmen vanligtvis inte varje del av sökutrymmet på samma tid, vilket ger ett utmanande lastbalanseringsproblem .

Kubfas för formeln

F

. Beslutsheuristiken väljer vilka variabler (cirklar) som ska tilldelas. Efter att cutoff-heuristiken bestämmer sig för att stoppa ytterligare förgrening, löses de partiella problemen (rektanglarna) oberoende med hjälp av CDCL.

På grund av icke-kronologisk bakåtspårning är parallellisering av konfliktdriven klausulinlärning svårare. Ett sätt att övervinna detta är Cube-and-Conquer-paradigmet. Det föreslår lösning i två faser. I "kubfasen" är problemet uppdelat i många tusen, upp till miljoner, sektioner. Detta görs av en framåtblickslösare, som hittar en uppsättning partiella konfigurationer som kallas "kuber". En kub kan också ses som en konjunktion av en delmängd av variabler av den ursprungliga formeln. I samband med formeln bildar var och en av kuberna en ny formel. Dessa formler kan lösas oberoende och samtidigt av konfliktdrivna lösare. Eftersom disjunktionen av dessa formler är ekvivalent med den ursprungliga formeln, rapporteras problemet vara tillfredsställbart, om en av formlerna är tillfredsställande. Framtidslösaren är gynnsam för små men svåra problem, så den används för att gradvis dela upp problemet i flera delproblem. Dessa delproblem är lättare men ändå stora vilket är den idealiska formen för en konfliktdriven lösare. Dessutom överväger framtidslösare hela problemet medan konfliktdrivna lösare fattar beslut baserat på information som är mycket mer lokal. Det finns tre heuristiker involverade i kubfasen. Variablerna i kuberna väljs av beslutsheuristiken. Riktningsheuristiken avgör vilken variabeltilldelning (sant eller falsk) som ska utforskas först. I tillfredsställande problemfall är det fördelaktigt att först välja en tillfredsställande gren. Cutoff-heuristiken avgör när man ska sluta expandera en kub och istället vidarebefordra den till en sekventiell konfliktdriven lösare. Företrädesvis är kuberna lika komplexa att lösa.

Treengeling är ett exempel på en parallelllösare som tillämpar Cube-and-Conquer-paradigmet. Sedan introduktionen 2012 har den haft flera framgångar i International SAT Solver Competition. Cube-and-Conquer användes för att lösa det booleska pythagoras trippelproblem .

Lokal sökning

En strategi mot en parallell lokal sökalgoritm för SAT-lösning är att prova flera variabla vändningar samtidigt på olika bearbetningsenheter. En annan är att tillämpa den tidigare nämnda portföljmetoden, men klausuldelning är inte möjligt eftersom lokala söklösare inte producerar klausuler. Alternativt är det möjligt att dela de konfigurationer som produceras lokalt. Dessa konfigurationer kan användas för att styra produktionen av en ny initial konfiguration när en lokal lösare bestämmer sig för att starta om sin sökning.

Se även