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 16 articles )

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

  1. Lagniez, Jean-Marie; Marquis, Pierre: On preprocessing techniques and their impact on propositional model counting (2017)
  2. Toda, Takahisa: Dualization of Boolean functions using ternary decision diagrams (2017)
  3. Wang, Jinyan; Yin, Minghao; Wu, Jingli: Two approximate algorithms for model counting (2017)
  4. Zulkoski, Edward; Bright, Curtis; Heinle, Albert; Kotsireas, Ilias; Czarnecki, Krzysztof; Ganesh, Vijay: Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (2017)
  5. Cuong, C.K.; Heule, M.J.H.: Computing maximum unavoidable subgraphs using SAT solvers (2016)
  6. Mengel, Stefan: Parameterized compilation lower bounds for restricted CNF-formulas (2016)
  7. Tsuiki, Hideki; Tsukamoto, Yasuyuki: Sudoku colorings of a 16-cell pre-fractal (2016)
  8. Aziz, Rehan Abdul; Chu, Geoffrey; Muise, Christian; Stuckey, Peter: $\#\existsSAT$: projected model counting (2015)
  9. Burchard, Jan; Schubert, Tobias; Becker, Bernd: Laissez-faire caching for parallel #SAT solving (2015)
  10. Douglass, Adam; King, Andrew D.; Raymond, Jack: Constructing SAT filters with a quantum annealer (2015)
  11. Wang, Jinyan; Yin, Minghao; Wu, Jingli: Approximate model counting via extension rule (2015)
  12. Zulkoski, Edward; Ganesh, Vijay; Czarnecki, Krzysztof: MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers (2015)
  13. Castaño, José M.; Castaño, Rodrigo: A finite state intersection approach to propositional satisfiability (2012)
  14. Baarir, Souheib; Braunstein, Cécile; Encrenaz, Emmanuelle; Ilié, Jean-Michel; Mounier, Isabelle; Poitrenaud, Denis; Younes, Sana: Feasibility analysis for robustness quantification by symbolic model checking (2011)
  15. Castaño, José M.; Castaño, Rodrigo: Variable and clause ordering in an FSA approach to propositional satisfiability (2011)
  16. Thurley, Marc: sharpSAT -- counting models with advanced component caching and implicit BCP (2006) ioport