sharpSAT – counting models with advanced component caching and implicit BCP. We introduce sharpSAT, a new #SAT solver that is based on the well known DPLL algorithm and techniques from SAT and #SAT solvers. Most importantly, we introduce an entirely new approach of coding components, which reduces the cache size by at least one order of magnitude, and a new cache management scheme. Furthermore, we apply a well known look ahead based on BCP in a manner that is well suited for #SAT solving. We show that these techniques are highly beneficial, especially on large structured instances, such that our solver performs significantly better than other #SAT solvers.

References in zbMATH (referenced in 27 articles )

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

1 2 next

  1. Teuber, Samuel; Weigl, Alexander: Quantifying software reliability via model-counting (2021)
  2. Boege, Tobias; Kahle, Thomas: Construction methods for gaussoids. (2020)
  3. Hecher, Markus; Thier, Patrick; Woltran, Stefan: Taming high treewidth with abstraction, nested dynamic programming, and database technology (2020)
  4. Lagniez, Jean-Marie; Lonca, Emmanuel; Marquis, Pierre: Definability for model counting (2020)
  5. Achlioptas, Dimitris; Theodoropoulos, Panos: Model counting with error-correcting codes (2019)
  6. Boege, Tobias; D’Alì, Alessio; Kahle, Thomas; Sturmfels, Bernd: The geometry of gaussoids (2019)
  7. Heule, Marijn J. H.: Optimal symmetry breaking for graph problems (2019)
  8. Meel, Kuldeep S.; Shrotri, Aditya A.; Vardi, Moshe Y.: Not all FPRASs are equal: demystifying FPRASs for DNF-counting (2019)
  9. Fichte, Johannes K.; Hecher, Markus; Woltran, Stefan; Zisser, Markus: Weighted model counting on the GPU by exploiting small treewidth (2018)
  10. Avni, Guy; Goel, Shubham; Henzinger, Thomas A.; Rodriguez-Navas, Guillermo: Computing scores of forwarding schemes in switched networks with probabilistic faults (2017)
  11. Lagniez, Jean-Marie; Marquis, Pierre: On preprocessing techniques and their impact on propositional model counting (2017)
  12. Previti, Alessandro; Mencía, Carlos; Järvisalo, Matti; Marques-Silva, Joao: Improving MCS enumeration via caching (2017)
  13. Toda, Takahisa: Dualization of Boolean functions using ternary decision diagrams (2017)
  14. Wang, Jinyan; Yin, Minghao; Wu, Jingli: Two approximate algorithms for model counting (2017)
  15. Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
  16. Cuong, C. K.; Heule, M. J. H.: Computing maximum unavoidable subgraphs using SAT solvers (2016)
  17. Mengel, Stefan: Parameterized compilation lower bounds for restricted CNF-formulas (2016)
  18. Tsuiki, Hideki; Tsukamoto, Yasuyuki: Sudoku colorings of a 16-cell pre-fractal (2016)
  19. Aziz, Rehan Abdul; Chu, Geoffrey; Muise, Christian; Stuckey, Peter: (#\exists\mathrmSAT): projected model counting (2015)
  20. Burchard, Jan; Schubert, Tobias; Becker, Bernd: Laissez-faire caching for parallel #SAT solving (2015)

1 2 next