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

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

1 2 next

  1. Labbé, Sébastien: Substitutive structure of Jeandel-Rao aperiodic tilings (2021)
  2. Amendola, Giovanni; Ricca, Francesco; Truszczynski, Miroslaw: New models for generating hard random Boolean formulas and disjunctive logic programs (2020)
  3. Balko, Martin; Cibulka, Josef; Král, Karel; Kynčl, Jan: Ramsey numbers of ordered graphs (2020)
  4. Dodaro, Carmine; Eiter, Thomas; Ogris, Paul; Schekotihin, Konstantin: Managing caching strategies for stream reasoning with reinforcement learning (2020)
  5. Horáček, Jan; Kreuzer, Martin: On conversions from CNF to ANF (2020)
  6. Lagniez, Jean-Marie; Lonca, Emmanuel; Marquis, Pierre: Definability for model counting (2020)
  7. Li, Chu-Min; Xiao, Fan; Luo, Mao; Manyà, Felip; Lü, Zhipeng; Li, Yu: Clause vivification by unit propagation in CDCL SAT solvers (2020)
  8. Pei, Yan Ru; Manukian, Haik; Di Ventra, Massimiliano: Generating weighted MAX-2-SAT instances with frustrated loops: an RBM case study (2020)
  9. 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)
  10. Abd El-Maksoud, Munira A.; Abdalla, Areeg: A novel SAT solver for the Van der Waerden numbers (2019)
  11. Zha, Aolong; Koshimura, Miyuki; Fujita, Hiroshi: (N)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT (2019)
  12. Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: PySAT: A Python toolkit for prototyping with SAT oracles (2018)
  13. Alviano, Mario: Model enumeration in propositional circumscription via unsatisfiable core analysis (2017)
  14. Balko, Martin; Valtr, Pavel: A SAT attack on the Erdős-Szekeres conjecture (2017)
  15. Devriendt, Jo; Bogaerts, Bart; Bruynooghe, Maurice: Symmetric explanation learning: effective dynamic symmetry handling for SAT (2017)
  16. Egly, Uwe; Kronegger, Martin; Lonsing, Florian; Pfandler, Andreas: Conformant planning as a case study of incremental QBF solving (2017)
  17. Liang, Jia Hui; Hari Govind, V. K.; Poupart, Pascal; Czarnecki, Krzysztof; Ganesh, Vijay: An empirical study of branching heuristics through the lens of global learning rate (2017)
  18. Lindauer, Marius; Hoos, Holger; Leyton-Brown, Kevin; Schaub, Torsten: Automatic construction of parallel portfolios via algorithm configuration (2017)
  19. Nejati, Saeed; Newsham, Zack; Scott, Joseph; Liang, Jia Hui; Gebotys, Catherine; Poupart, Pascal; Ganesh, Vijay: A propagation rate based splitting heuristic for divide-and-conquer solvers (2017)
  20. Surynek, Pavel: Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems (2017)

1 2 next