Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
On the Structure of Resolution Refutations Generated by Modern CDCL Solvers
KTH, School of Electrical Engineering and Computer Science (EECS).
2019 (English)Independent thesis Advanced level (degree of Master (Two Years)), 20 credits / 30 HE creditsStudent thesisAlternative title
Formen på resolutions-refutationer genererade av moderna CDCL-lösare (Swedish)
Abstract [en]

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.

Abstract [sv]

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.

Place, publisher, year, edition, pages
2019. , p. 107
Series
TRITA-EECS-EX ; 2019:96
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:kth:diva-252732OAI: oai:DiVA.org:kth-252732DiVA, id: diva2:1320366
Supervisors
Examiners
Available from: 2019-06-05 Created: 2019-06-04 Last updated: 2019-06-05Bibliographically approved

Open Access in DiVA

fulltext(2963 kB)7 downloads
File information
File name FULLTEXT01.pdfFile size 2963 kBChecksum SHA-512
493233f33924ce97ebd213201f75cab994325924ab87e068aa9f47b4d21181e247408cacddc56efe0f569696860fbd29457f415adb506bae88f4db19bf5cec56
Type fulltextMimetype application/pdf

By organisation
School of Electrical Engineering and Computer Science (EECS)
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 7 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 34 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf