PicoSAT

PicoSAT essentials. 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.


References in zbMATH (referenced in 75 articles , 1 standard article )

Showing results 1 to 20 of 75.
Sorted by year (citations)

1 2 3 4 next

  1. Marques-Silva, Joao; Malik, Sharad: Propositional SAT solving (2018)
  2. Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
  3. Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: On tackling the limits of resolution in SAT solving (2017)
  4. Marques-Silva, Joao; Janota, Mikoláš; Mencía, Carlos: Minimal sets on propositional formulae. problems and reductions (2017)
  5. Schrammel, Peter; Kroening, Daniel; Brain, Martin; Martins, Ruben; Teige, Tino; Bienmüller, Tom: Incremental bounded model checking for embedded software (2017)
  6. Wickerson, John; Batty, Mark; Sorensen, Tyler; Constantinides, George A.: Automatically comparing memory consistency models (2017)
  7. Balyo, Tomáš; Lonsing, Florian: Hordeqbf: A modular and massively parallel QBF solver (2016)
  8. Färber, Michael; Brown, Chad: Internal guidance for Satallax (2016)
  9. Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer (2016)
  10. Khasidashvili, Zurab; Korovin, Konstantin: Predicate elimination for preprocessing in first-order theorem proving (2016)
  11. KhudaBukhsh, Ashiqur R.; Xu, Lin; Hoos, Holger H.; Leyton-Brown, Kevin: SATenstein: automatically building local search SAT solvers from components (2016)
  12. Kroening, Daniel; Strichman, Ofer: Decision procedures. An algorithmic point of view (2016)
  13. Lonsing, Florian; Egly, Uwe; Seidl, Martina: Q-resolution with generalized axioms (2016)
  14. Rabe, Markus N.; Seshia, Sanjit A.: Incremental determinization (2016)
  15. Schlaipfer, Matthias; Weissenbacher, Georg: Labelled interpolation systems for hyper-resolution, clausal, and local proofs (2016)
  16. Tentrup, Leander: Non-prenex QBF solving using abstraction (2016)
  17. Toda, Takahisa; Soh, Takehide: Implementing efficient All solutions SAT solvers (2016)
  18. Woźna-Szcześniak, Bożena; Zbrzezny, Andrzej: Checking EMTLK properties of timed interpreted systems via bounded model checking (2016)
  19. Biere, Armin; Fröhlich, Andreas: Evaluating CDCL variable scoring schemes (2015)
  20. Heule, Marijn J. H.; Hunt, Warren A. jun.; Wetzler, Nathan: Expressing symmetry breaking in DRAT proofs (2015)

1 2 3 4 next


Further publications can be found at: http://fmv.jku.at/papers/index.html