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

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

1 2 next

  1. Amendola, Giovanni; Ricca, Francesco; Truszczynski, Miroslaw: New models for generating hard random Boolean formulas and disjunctive logic programs (2020)
  2. Balko, Martin; Cibulka, Josef; Král, Karel; Kynčl, Jan: Ramsey numbers of ordered graphs (2020)
  3. Horáček, Jan; Kreuzer, Martin: On conversions from CNF to ANF (2020)
  4. Lagniez, Jean-Marie; Lonca, Emmanuel; Marquis, Pierre: Definability for model counting (2020)
  5. Li, Chu-Min; Xiao, Fan; Luo, Mao; Manyà, Felip; Lü, Zhipeng; Li, Yu: Clause vivification by unit propagation in CDCL SAT solvers (2020)
  6. 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)
  7. Abd El-Maksoud, Munira A.; Abdalla, Areeg: A novel SAT solver for the Van der Waerden numbers (2019)
  8. Zha, Aolong; Koshimura, Miyuki; Fujita, Hiroshi: (N)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT (2019)
  9. Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao: PySAT: A Python toolkit for prototyping with SAT oracles (2018)
  10. Alviano, Mario: Model enumeration in propositional circumscription via unsatisfiable core analysis (2017)
  11. Balko, Martin; Valtr, Pavel: A SAT attack on the Erdős-Szekeres conjecture (2017)
  12. Devriendt, Jo; Bogaerts, Bart; Bruynooghe, Maurice: Symmetric explanation learning: effective dynamic symmetry handling for SAT (2017)
  13. Egly, Uwe; Kronegger, Martin; Lonsing, Florian; Pfandler, Andreas: Conformant planning as a case study of incremental QBF solving (2017)
  14. 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)
  15. Lindauer, Marius; Hoos, Holger; Leyton-Brown, Kevin; Schaub, Torsten: Automatic construction of parallel portfolios via algorithm configuration (2017)
  16. 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)
  17. Surynek, Pavel: Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems (2017)
  18. Thimm, Matthias; Villata, Serena: The first international competition on computational models of argumentation: results and analysis (2017)
  19. Audemard, Gilles; Simon, Laurent: Extreme cases in SAT problems (2016)
  20. Balyo, Tomáš; Biere, Armin; Iser, Markus; Sinz, Carsten: SAT race 2015 (2016)

1 2 next