Formen på resolutions-refutationer genererade av moderna CDCL-lösare

Modern solvers for the Boolean satisfiability problem (SAT) that are based on conflict-driven clause learning (CDCL) are known to be able to solve some instances significantly more efficiently than older kinds of solvers such as ones using the Davis-Putnam-Logemann-Loveland (DPLL) algorithm. In addition to solving instances that can be satisfied, SAT solvers will implicitly generate proofs of unsatisfiability for formulae that are unsatisfiable. Theoretical models of CDCL based solvers are known to have access to more powerful forms of reasoning compared to their DPLL counterparts and as a result, are able to generate proofs that are significantly shorter for certain kinds of formulae. Additionally, certain characteristics are expected when representing these proofs as graphs, such as them not being strictly tree-like in shape. It is however less well known if these theoretical justifications are indeed the reason CDCL solvers are so successful in practice. This project attempts to answer this question by modifying a modern CDCL solver to output the proof and comparing these proofs to what theoretical results would predict. Firstly, the results indicate that CDCL solvers generate significantly shorter proofs for all kinds of formulae that were investigated as compared to a DPLL solver. Furthermore, it appears that this is in large part due to the proof not being tree-like. Secondly, utilizing restarts was found to make for significantly shorter proofs for most families of formulae but the effect was the opposite for formulas representing the relativized pigeonhole principle. The explanation for this is seemingly not clear. Lastly, it appears that the Tseitin formulae used do not exhibit timespace trade-offs but instead simply require a large amount of space. This is indicated by the run time being significantly greater if clause erasure if more aggressive but the refutation being similar in both length and number of learned clauses. To summarize, it has been found that modern CDCL solvers appear to result in significantly different proofs that largely mirror what one would expect. However, the results are unclear on the role of restarts and how their effect on the proof best can be explained.Moderna lösare för Boolean satisfiability problem (SAT) baserade på konfliktdriven klausulinlärning (CDCL) har visats prestera väl och lösa vissa typer av formler mer effektivt än äldre varianter såsom Davis-Putnam-Logemann-Loveland-algoritmen (DPLL). Förutom att lösa instanser som är lösbara så producerar SAT-lösare implicit bevis på olösbarhet för formler som är olösbara. Teoretiska modeller över CDCL-baserade lösare har visat på att mer kraftfulla former av resonemang är tillgängliga jämfört med DPLL-baserade motsvarigheter; som ett resultat kan CDCL-baserade lösare enligt dessa modeller producera kortare bevis. Vidare väntas dessa bevis ha vissa karaktärsdrag när de representeras som grafer som exempelvis att de inte är strikt trädformade. Dock är det inte känt om dessa teoretiska förklaringar faktiskt korrekt beskriver anledningarna att CDCL-baserade lösare är så framgångsrika i praktiken. Detta projekt ämnar klargöra denna fråga genom att modifiera en CDCL-baserad lösare så att den producerar bevisen explicit och sedan jämföra dessa bevis med vad teoretiska resultat skulle förutspå. För det första så visar resultaten att CDCL-baserade lösare genererar betydligt kortare bevis för alla sorters formler som undersöktes. Studier av småskaliga probleminstanser visar att en del av förklaringen till detta är att beviset inte är strikt trädformat. För det andra visar resultaten att omstarter gör bevisen betydligt kortare för nästan alla formler men att det motsatta är sant för så kallade relativized pigeonhole principle-formler. Förklaringen till detta är inte helt tydlig. För det tredje sågs tendenser till tid-utrymmes-avvägningar för formler som var inspirerade av så kallade Tseitin-formler där dessa avvägningar är bevisade. Det antyder att även dessa inspirerade formler ger dessa avvägningar i praktiska implementationer av CDCL-lösare. För att summera så visar resultaten att moderna CDCL-baserade lösare till stor del uppnår vad teoretiska modeller förutspår i termer av formen på deras bevis. Dock är resultaten mindre tydliga vad gäller omstarter och hur deras påverkan på bevisen bäst förklaras