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 72 articles , 1 standard article )

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

1 2 3 4 next

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

1 2 3 4 next

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