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

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

1 2 next

  1. Balko, Martin; Valtr, Pavel: A SAT attack on the Erd\Hos-Szekeres conjecture (2017)
  2. Egly, Uwe; Kronegger, Martin; Lonsing, Florian; Pfandler, Andreas: Conformant planning as a case study of incremental QBF solving (2017)
  3. Lindauer, Marius; Hoos, Holger; Leyton-Brown, Kevin; Schaub, Torsten: Automatic construction of parallel portfolios via algorithm configuration (2017)
  4. Thimm, Matthias; Villata, Serena: The first international competition on computational models of argumentation: results and analysis (2017)
  5. Audemard, Gilles; Simon, Laurent: Extreme cases in SAT problems (2016)
  6. Balyo, Tomáš; Biere, Armin; Iser, Markus; Sinz, Carsten: SAT race 2015 (2016)
  7. Itzhakov, Avraham; Codish, Michael: Breaking symmetries in graph search with canonizing sets (2016)
  8. Liang, Jia Hui; Ganesh, Vijay; Poupart, Pascal; Czarnecki, Krzysztof: Learning rate based branching heuristic for SAT solvers (2016)
  9. Niskanen, Andreas; Wallner, Johannes P.; Järvisalo, Matti: Pakota: a system for enforcement in abstract argumentation (2016)
  10. Balko, Martin; Valtr, Pavel: A SAT attack on the Erd\Hos-Szekeres conjecture (2015)
  11. Biere, Armin; Fröhlich, Andreas: Evaluating CDCL variable scoring schemes (2015)
  12. Ignatiev, Alexey; Previti, Alessandro; Marques-Silva, Joao: SAT-based formula simplification (2015)
  13. Konev, Boris; Lisitsa, Alexei: Computer-aided proof of Erd\Hosdiscrepancy properties (2015)
  14. Lonsing, Florian; Egly, Uwe: Incrementally computing minimal unsatisfiable cores of QBFs via a clause group solver API (2015)
  15. Mencía, Carlos; Previti, Alessandro; Marques-Silva, Joao: SAT-based Horn least upper bounds (2015)
  16. Oh, Chanseok: Between SAT and UNSAT: the fundamental difference in CDCL SAT (2015)
  17. Hurley, Barry; Kotthoff, Lars; Malitsky, Yuri; O’Sullivan, Barry: Proteus: a hierarchical portfolio of solvers and transformations (2014)
  18. Martins, Ruben; Manquinho, Vasco; Lynce, In^es: Open-WBO: a modular MaxSAT solver (2014)
  19. Audemard, Gilles; Lagniez, Jean-Marie; Simon, Laurent: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction (2013)
  20. Jiang, Chuan; Zhang, Ting: Partial backtracking in CDCL solvers (2013)

1 2 next