PicoSAT Essentials

By Armin Biere. Journal on Satisfiability, Boolean Modeling and Computation, 2008

461 citations recorded by the source corpus.

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.

Subfields: Building and Construction, Geography, Planning and Development, Ocean Engineering

View Paper: https://www.semanticscholar.org/paper/7ea4cdd0003234f9e98ff5a080d9191c398e26c2

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Building and Construction

In Geography, Planning and Development

In Ocean Engineering

Citations in the corpus

DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs (2014, methodology): “DRUP-trim, the predecessor to this tool, can produce a resolution graph of a proof in the TraceCheck [18,13,4] format.”
The Sat4j library, release 2.2 (2010, methodology): “…the settings used in the default SAT solver available in Sat4j 2.2: the rapid restarts strategy is the in/out one proposed by Armin Biere in Picosat[4]; the conﬂict clause minimization of Minisat 1.14 (so called Expensive Simpliﬁcation)[15] is used at the end of the conﬂict analysis; the phase…”
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays (2009, methodology): “SAT Solver PicoSAT [3] is used as SAT solver.”
Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic (2014, background): “Further lines of research examine heuristics for which variable to choose as a decision and what value it should be assigned, and when to restart the SAT search [14, 66, 86, 94].”
Answer Set Solving in Practice (2012, background): “,∼an where 0 ≤ m ≤ n and each ai is an atom for 1 ≤ i ≤ n Example :- edge(3,7), color(3,red), color(7,red).”
Conflict-driven answer set solving: From theory to practice (2012, methodology): “In addition, the nested policy first used in picosat [11] is also offered by clasp.”
Iterative and core-guided MaxSAT solving: A survey and assessment (2013, methodology): “All algorithms have been implemented in C++ inside the MSUnCore system [91] which uses picosat [26] as its underlying non-incremental SAT solver, with the”