Rahulolu käsiraamat

Lauseloogikat on läbi sajandite peetud filosoofia ja matemaatika arutluskäigu üheks nurgakiviks. Aja jooksul kaasnes selle formaliseerimisega Boole'i ​​algebrasse äratundmine, et laia valikut kombinatoorseid probleeme saab väljendada lausepõhise rahuldatavuse (SAT) probleemidena. Selle kahetise rolli tõttu arenes SAT küpseks ja mitmetahuliseks teadusdistsipliiniks ning arvutite algusaegadest peale otsiti võimalusi SAT probleemide automatiseeritud lahendamiseks. See raamat, „Rahuldavuse käsiraamat“, on 2009. aastal sama nime all esmakordselt avaldatud raamatu teine, ajakohastatud ja parandatud väljaanne. Käsiraamatu eesmärk on jäädvustada SAT täielikku ulatust ja sügavust ning koondada olulisi edusamme ja edusamme automatiseeritud lahendamisel. Käsitletavad teemad hõlmavad SAT ja selle rakenduste praktilist ja teoreetilist uurimistööd ning hõlmavad otsingualgoritme, heuristikat, algoritmide analüüsi, raskeid eksemplare, randomiseeritud valemeid, probleemide kodeerimist, tööstuslikke rakendusi, lahendajaid, lihtsustajaid, tööriistu, juhtumiuuringuid ja empiirilisi tulemusi. SAT-i tõlgendatakse laias tähenduses, seega lisaks propositsioonilisele rahuldatavusele on olemas peatükid, mis käsitlevad kvantifitseeritud Boole'i ​​valemeid (QBF), piirangutega programmeerimise tehnikaid (CSP) sõnataseme probleemide ja nende propositsioonilise kodeerimise jaoks ning rahuldatavuse mooduliteooriaid (SMT). Iga peatükki täiendab ulatuslik bibliograafia. Käsiraamatu teine ​​väljaanne pakub huvi teadlastele, magistrantidele, bakalaureuseõppe lõpukursuslastele ja praktikutele, kes kasutavad SAT-i või panustavad sellesse, ning pakub nende tööks nii inspiratsiooni kui ka rikkalikku ressurssi. Edmund Clarke, 2007. aasta ACM Turingi auhinna saaja: „SAT-i lahendamine on 21. sajandi arvutiteaduse võtmetehnoloogia.“ Donald Knuth, 1974. aasta ACM Turingi auhinna saaja: „SAT on ilmselgelt suurepärane rakendus, sest see on võtmeks nii paljude teiste probleemide lahendamisel.“ Stephen Cook, 1982. aasta ACM Turingi auhinna saaja: „SAT-probleem on vaieldamatult arvutiteaduse kõige fundamentaalsema küsimuse keskmes: mis teeb probleemi keeruliseks?“