Abstrakt. På grund av SAT:s inneboende NP-fullständighet kan många SAT-problem för närvarande inte lösas inom rimlig tid. Vanligtvis måste nya ad hoc-algoritmer utformas för att hantera en ny klass av SAT-problem. Ett annat sätt att lösa ett nytt problem är att använda en generisk lösare och använda parallellism för att minska tiden. I detta dokument föreslår vi ett parallelliseringssystem för en klass av SAT-lösare som bygger på DPLL-förfarandet. Systemet använder sig av en dynamisk mekanism för lastbalansering som bygger på teknik för att stjäla arbete för att hantera oegentligheten i SAT-problemen. Vi parallelliserar Satz, en av de bästa generiska SAT-lösarna, med vårt system för att få en parallell lösare som kallas PSatz. De första experimentella resultaten på slumpmässiga 3-SAT-problem och en uppsättning välkända strukturerade problem visar PSatz effektivitet. PSatz är fritt tillgänglig och körs på alla nätverksarbetsstationer under Unix/Linux.
I REF presenteras ett parallelliseringssystem för en klass av SAT-lösare baserat på DPLL-förfarandet.
A Parallelization Scheme Based on Work Stealing for a Class of SAT Solvers
{'venue': 'Journal of Automated Reasoning', 'journal': 'Journal of Automated Reasoning', 'mag_field_of_study': ['Computer Science']}