: Journal on Satisfiability, Boolean Modeling and Computation (JSAT), Vol. 4, Seite(n) 75-97, 2008
Sprache des Titels:
Journal on Satisfiability, Boolean Modeling and Computation (JSAT)
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.