Glucose swMATH ID: 7833 Software Authors: Gilles Audemard; Laurent Simon Description: 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 Homepage: http://www.labri.fr/perso/lsimon/glucose/ Related Software: MiniSat; Chaff; Lingeling; Plingeling; Treengeling; CryptoMiniSat; PySAT; COMiniSatPS; Open-WBO; GitHub; clasp; PrecoSAT; MapleCOMSPS; CaDiCaL; Syrup; Sat4j; BerkMin; StarExec; Gurobi; MapleCOMSPS_LRB Cited in: 54 Documents all top 5 Cited by 120 Authors 6 Ignatyev, Alexey A. 6 Marques-Silva, João P. 3 Balko, Martin 3 Codish, Michael 3 Surynek, Pavel 2 Audemard, Gilles 2 Biere, Armin 2 Czarnecki, Krzysztof 2 Egly, Uwe 2 Ganesh, Vijay 2 Itzhakov, Avraham 2 Järvisalo, Matti 2 Kochemazov, Stepan 2 Lagniez, Jean-Marie 2 Liang, Jiahui 2 Lonsing, Florian 2 Malykhin, Yuriĭ Vyacheslavovich 2 Morgado, António 2 Niskanen, Andreas 2 Poupart, Pascal 2 Previti, Alessandro 2 Shchepin, Evgenij V. 2 Simon, Laurent S. R. 2 Valtr, Pavel 1 Abd El-Maksoud, Munira A. 1 Abdalla, Areeg 1 Alviano, Mario 1 Amendola, Giovanni 1 Andreychuk, Anton 1 Atzmon, Dor 1 Balyo, Tomáš 1 Baumeister, Dorothea 1 Bogaerts, Bart 1 Bøgsted Poulsen, Danny 1 Bonet, Maria Luisa 1 Brimkov, Boris 1 Bruynooghe, Maurice 1 Buss, Samuel R. 1 Cai, Shaowei 1 Cibulka, Josef 1 Dergachev, E. A. 1 Devriendt, Jo 1 Di Ventra, Massimiliano 1 Dodaro, Carmine 1 Eiter, Thomas 1 Fröhlich, Andreas M. 1 Fujita, Hiroshi 1 Gebser, Martin 1 Giesl, Jürgen 1 Gribanova, Irina 1 Hari Govind, V. K. 1 Hicks, Illya V. 1 Hoos, Holger H. 1 Horáček, Jan 1 Iser, Markus 1 Janhunen, Tomi 1 Jiang, Chuan 1 Koenig, Sven 1 Konev, Boris 1 Koshimura, Miyuki 1 Král, Karel 1 Kreuzer, Martin 1 Kronegger, Martin 1 Kučera, Petr 1 Kulczynski, Mitja 1 Kumar, T. K. Satish 1 Kyncl, Jan 1 Le Bodic, Pierre 1 Leyton-Brown, Kevin 1 Li, Chumin 1 Li, Jiaoyang 1 Li, Yu 1 Lindauer, Marius 1 Lisitsa, Alexei P. 1 Lonca, Emmanuel 1 Lotz, Kevin 1 Lü, Zhipeng 1 Luo, Mao 1 Lynce, Inês 1 Manquinho, Vasco M. 1 Manthey, Norbert 1 Manukian, Haik 1 Manyà, Felip 1 Marquis, Pierre 1 Martins, Ruben 1 Mencía, Carlos 1 Mikesell, Derek 1 Nadel, Alexander 1 Neopryatnaya, A. M. 1 Neugebauer, Daniel 1 Nowotka, Dirk 1 Ogris, Paul 1 Oh, Chanseok 1 Otpuschennikov, Ilya V. 1 Pei, Yan Ru 1 Pfandler, Andreas 1 Ricca, Francesco 1 Rintanen, Jussi 1 Rothe, Jörg-Matthias 1 Schaub, Torsten H. ...and 20 more Authors all top 5 Cited in 17 Serials 11 Artificial Intelligence 3 Constraints 2 Discrete & Computational Geometry 2 Annals of Mathematics and Artificial Intelligence 2 Theory and Practice of Logic Programming 1 Discrete Mathematics 1 European Journal of Combinatorics 1 Journal of Symbolic Computation 1 Journal of Automated Reasoning 1 Journal of the Egyptian Mathematical Society 1 The Electronic Journal of Combinatorics 1 The Journal of Artificial Intelligence Research (JAIR) 1 INFORMS Journal on Computing 1 Doklady Mathematics 1 Journal of Machine Learning Research (JMLR) 1 Journal of Satisfiability, Boolean Modeling and Computation 1 Logical Methods in Computer Science all top 5 Cited in 11 Fields 46 Computer science (68-XX) 5 Mathematical logic and foundations (03-XX) 5 Combinatorics (05-XX) 3 Operations research, mathematical programming (90-XX) 2 Number theory (11-XX) 2 Convex and discrete geometry (52-XX) 2 Information and communication theory, circuits (94-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Commutative algebra (13-XX) 1 Measure and integration (28-XX) 1 Dynamical systems and ergodic theory (37-XX) Citations by Year