Glucose

The Glucose SAT Solver. Glucose is based on a new scoring scheme (well, not so new now, it was introduced in 2009) for the clause learning mechanism of so called ”Modern” SAT sovlers (it is based our IJCAI’09 paper). This page summarizes the techniques embedded in the competition 09 version of glucose. Solver’s name is a contraction of the concept of ”glue clauses”, a particular kind of clauses that glucose detects and preserves during search. Glucose is heavily based on Minisat, so please do cite Minisat also if you want to cite Glucose


References in zbMATH (referenced in 47 articles )

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

1 2 3 next

  1. Baumeister, Dorothea; Järvisalo, Matti; Neugebauer, Daniel; Niskanen, Andreas; Rothe, Jörg: Acceptance in incomplete argumentation frameworks (2021)
  2. Bonet, Maria Luisa; Buss, Sam; Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: Propositional proof systems based on maximum satisfiability (2021)
  3. Ignatiev, Alexey; Marques-Silva, Joao: SAT-based rigorous explanations for decision lists (2021)
  4. Kochemazov, Stepan; Ignatiev, Alexey; Marques-Silva, Joao: Assessing progress in SAT solvers through the Lens of incremental SAT (2021)
  5. Labbé, Sébastien: Substitutive structure of Jeandel-Rao aperiodic tilings (2021)
  6. Manthey, Norbert: The \textscMergeSatsolver (2021)
  7. Yu, Jinqiang; Ignatiev, Alexey; Stuckey, Peter J.; Le Bodic, Pierre: Learning optimal decision sets and lists with SAT (2021)
  8. Amendola, Giovanni; Ricca, Francesco; Truszczynski, Miroslaw: New models for generating hard random Boolean formulas and disjunctive logic programs (2020)
  9. Balko, Martin; Cibulka, Josef; Král, Karel; Kynčl, Jan: Ramsey numbers of ordered graphs (2020)
  10. Dodaro, Carmine; Eiter, Thomas; Ogris, Paul; Schekotihin, Konstantin: Managing caching strategies for stream reasoning with reinforcement learning (2020)
  11. Horáček, Jan; Kreuzer, Martin: On conversions from CNF to ANF (2020)
  12. Lagniez, Jean-Marie; Lonca, Emmanuel; Marquis, Pierre: Definability for model counting (2020)
  13. Li, Chu-Min; Xiao, Fan; Luo, Mao; Manyà, Felip; Lü, Zhipeng; Li, Yu: Clause vivification by unit propagation in CDCL SAT solvers (2020)
  14. Malykhin, Yu. V.; Shchepin, E. V.: Minimal self-similar Peano curve of genus (5 \times5) (2020)
  15. Nadel, Alexander: Polarity and variable selection heuristics for SAT-based anytime MaxSAT (2020)
  16. Pei, Yan Ru; Manukian, Haik; Di Ventra, Massimiliano: Generating weighted MAX-2-SAT instances with frustrated loops: an RBM case study (2020)
  17. Semenov, Alexander; Otpuschennikov, Ilya; Gribanova, Irina; Zaikin, Oleg; Kochemazov, Stepan: Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems (2020)
  18. Abd El-Maksoud, Munira A.; Abdalla, Areeg: A novel SAT solver for the Van der Waerden numbers (2019)
  19. Zha, Aolong; Koshimura, Miyuki; Fujita, Hiroshi: (N)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT (2019)
  20. Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: PySAT: a Python toolkit for prototyping with SAT oracles (2018)

1 2 3 next