On the Structure of Resolution Refutations Generated by Modern CDCL Solvers
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 addi...
| Main Author: | |
|---|---|
| Format: | Others |
| Language: | English |
| Published: |
KTH, Skolan för elektroteknik och datavetenskap (EECS)
2019
|
| Subjects: | |
| Online Access: | http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-252732 |