Abstract
In this article we describe and evaluate optimized compact data structures for watching
literals. Experiments with our SAT solver PicoSAT show that this low-level optimization
not only saves memory, but also turns out to speed up the SAT solver considerably. We
also discuss how to store proof traces compactly in memory and further unique features of
PicoSAT including an aggressive restart schedule.
| Original language | English |
|---|---|
| Title of host publication | Journal on Satisfiability, Boolean Modeling and Computation (JSAT) |
| Pages | 75-97 |
| Number of pages | 23 |
| Volume | 4 |
| Publication status | Published - 2008 |
Fields of science
- 102011 Formal languages