Some modern DPLL-based propositional SAT solvers now have fast in-memory algorithms for generating unsatisfiability proofs and cores without writing traces to disk. However, in long SAT runs these algorithms still run out of memory. For several of these algorithms, here we discuss advantages and disadvantages, based on carefully designed experiments with our implementation of each one of them, as well as with (our implementation of) Zhang and Malik's one writing traces on disk. Then we describe a new in-memory algorithm which saves space by doing more bookkeeping to discard unnecessary information, and show that it can handle significantly more instances than the previously existing algorithms, at a negligible expense in time. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Asín, R., Nieuwenhuis, R., Oliveras, A., & Rodríguez-Carbonell, E. (2008). Efficient generation of unsatisfiability proofs and cores in SAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5330 LNAI, pp. 16–30). https://doi.org/10.1007/978-3-540-89439-1_2
Mendeley helps you to discover research relevant for your work.