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

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

1 2 3 4 5 next

  1. Banković, Milan; Marić, Filip: Faradžev Read-type enumeration of non-isomorphic CC systems (2021)
  2. Kyrillidis, Anastasios; Shrivastava, Anshumali; Vardi, Moshe Y.; Zhang, Zhiwei: Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions (2021)
  3. Hecher, Markus; Thier, Patrick; Woltran, Stefan: Taming high treewidth with abstraction, nested dynamic programming, and database technology (2020)
  4. Rocha, Thiago Alves; Martins, Ana Teresa; Ferreira, Francicleber Martins: Synthesis of a DNF formula from a sample of strings using Ehrenfeucht-Fraïssé games (2020)
  5. Rocha, Thiago Alves; Martins, Ana Teresa; Ferreira, Francicleber Martins: Synthesis of quantifier-free DNF sentences from inconsistent samples of strings with EF games and SAT (2020)
  6. Scheucher, Manfred: Two disjoint 5-holes in point sets (2020)
  7. Schulz, Stephan; Cruanes, Simon; Vukmirović, Petar: Faster, higher, stronger: E 2.3 (2019)
  8. Marques-Silva, Joao; Malik, Sharad: Propositional SAT solving (2018)
  9. Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
  10. Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: On tackling the limits of resolution in SAT solving (2017)
  11. Marques-Silva, Joao; Janota, Mikoláš; Mencía, Carlos: Minimal sets on propositional formulae. Problems and reductions (2017)
  12. Schrammel, Peter; Kroening, Daniel; Brain, Martin; Martins, Ruben; Teige, Tino; Bienmüller, Tom: Incremental bounded model checking for embedded software (2017)
  13. Wickerson, John; Batty, Mark; Sorensen, Tyler; Constantinides, George A.: Automatically comparing memory consistency models (2017)
  14. Balyo, Tomáš; Lonsing, Florian: HordeQBF: a modular and massively parallel QBF solver (2016)
  15. Bulteau, Laurent; Froese, Vincent; Hartung, Sepp; Niedermeier, Rolf: Co-clustering under the maximum norm (2016)
  16. Färber, Michael; Brown, Chad: Internal guidance for Satallax (2016)
  17. Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer (2016)
  18. Khasidashvili, Zurab; Korovin, Konstantin: Predicate elimination for preprocessing in first-order theorem proving (2016)
  19. KhudaBukhsh, Ashiqur R.; Xu, Lin; Hoos, Holger H.; Leyton-Brown, Kevin: SATenstein: automatically building local search SAT solvers from components (2016)
  20. Kroening, Daniel; Strichman, Ofer: Decision procedures. An algorithmic point of view (2016)

1 2 3 4 5 next

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