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

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

1 2 3 4 5 next

  1. Brandt, Felix; Saile, Christian; Stricker, Christian: Strategyproof social choice when preferences and outcomes may contain ties (2022)
  2. Ansótegui, Carlos; Ojeda, Jesús; Pacheco, Antonio; Pon, Josep; Salvia, Josep M.; Torres, Eduard: OptiLog: a framework for SAT-based systems (2021)
  3. Banković, Milan; Marić, Filip: Faradžev Read-type enumeration of non-isomorphic CC systems (2021)
  4. Kyrillidis, Anastasios; Shrivastava, Anshumali; Vardi, Moshe Y.; Zhang, Zhiwei: Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions (2021)
  5. Le Berre, Daniel; Wallon, Romain: On dedicated CDCL strategies for PB solvers (2021)
  6. Py, Matthieu; Cherif, Mohamed Sami; Habet, Djamal: A proof builder for Max-SAT (2021)
  7. Rawson, Michael; Reger, Giles: Eliminating models during model elimination (2021)
  8. Síč, Juraj; Strejček, Jan: DQBDD: an efficient BDD-based DQBF solver (2021)
  9. Hecher, Markus; Thier, Patrick; Woltran, Stefan: Taming high treewidth with abstraction, nested dynamic programming, and database technology (2020)
  10. 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)
  11. 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)
  12. Scheucher, Manfred: Two disjoint 5-holes in point sets (2020)
  13. Schulz, Stephan; Cruanes, Simon; Vukmirović, Petar: Faster, higher, stronger: E 2.3 (2019)
  14. Marques-Silva, Joao; Malik, Sharad: Propositional SAT solving (2018)
  15. Slaney, John; Woltzenlogel Paleo, Bruno: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (2018)
  16. Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: On tackling the limits of resolution in SAT solving (2017)
  17. Marques-Silva, Joao; Janota, Mikoláš; Mencía, Carlos: Minimal sets on propositional formulae. Problems and reductions (2017)
  18. Schrammel, Peter; Kroening, Daniel; Brain, Martin; Martins, Ruben; Teige, Tino; Bienmüller, Tom: Incremental bounded model checking for embedded software (2017)
  19. Wickerson, John; Batty, Mark; Sorensen, Tyler; Constantinides, George A.: Automatically comparing memory consistency models (2017)
  20. Balyo, Tomáš; Lonsing, Florian: HordeQBF: a modular and massively parallel QBF solver (2016)

1 2 3 4 5 next

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