Glucose 4.0

CHANGELOG

@@ -0,0 +1,27 @@
+Version 4.0
+ - Add a Multithread version, called syrup (many glucose ;-)
+   See SAT14 paper: Lazy Clause Exchange Policy for parallel SAT solvers.
+
+ - Can work independently in sequential or with many cores
+
+Version 3.0 (2013)
+ - Add incremental features. 
+    See SAT13 paper: Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction
+
+ - Add certified UNSAT proof.
+
+Version 2.3 (2012)
+ - Add new restart strategy 
+    See CP12 paper: Refining Restarts Strategies For SAT and UNSAT
+
+ - Add additionnal features to speed the search
+
+Version 2.0 (2011) 
+ - Add additionnal features (freeze potential good clauses for one turn)
+
+ - Based on Minisat 2.2
+
+Version 1.0 (2009)
+ - Based on Minisat 2.0
+    First release of glucose.
+    See ijcai 2009 paper: Predicting Learnt Clauses Quality in Modern SAT Solver

README.md

@@ -1,13 +1,33 @@
 # Glucose SAT solver
 
-This is the release 3.0 of the glucose SAT solver. 
+This is the release 4.0 of the glucose SAT solver. 
 It is based on [Minisat 2.2](http://minisat.se/MiniSat.html)
 
-For compiling:  
- - ```cd simp```
-- ```make```
+**Glucose is now parallel**
+
+You can call it Glucose Parallel or Glucose-Syrup (a lot of glucose in it).
+An original mechanism for clause sharing (as described in the SAT 2014 paper, based on a 1-Watched literal scheme).
+Can work with a lot of cores and limited memory. There is no determinism in the parallel version.
 
+Very good performances on industrial (non crypto) problems.
 
-For running: ```simp/glucose BENCHNAME```
+**Note**: Don’t change the preprocessing switches on this version (you can turn off the preprocessing but when using it, don’t play with the preprocessing options). We were reported some discrepancies in the results when using the -rcheck argument.
+You can choose to compile the following Glucose alternatives:
 
+    Glucose sequential (with/without Satelite, decided by command line arguments)
+    Glucose sequential, incremental mode
+    Glucose sequential, certified unsat proof logging
+    Glucose parallel with satelite ( not yet a parallel certified unsat / parallel incremental)
+
+Choose your directory (simp or parallel) and type ‘make’.
+
+## Papers 
+
+ - "_Predicting Learnt Clauses Quality in Modern SAT Solver_". Gilles Audemard, Laurent Simon, in Twenty-first International Joint Conference on Artificial Intelligence (IJCAI'09), july 2009.
+ - "_Glucose: a solver that predicts learnt clauses quality_". Gilles Audemard, Laurent Simon, SAT Competition, 2009.
+ - "_Refining restarts strategies for SAT and UNSAT formulae_". Gilles Audemard and Laurent Simon, in Proceedings of the 22nd International Conference on Principles and Practice of Constraint Programming (CP-12), 2012.
+ - "_GLUCOSE 2.1: Aggressive – but Reactive – Clause Database Management, Dynamic Restarts_". In Pragmatics of SAT (Workshop of SAT'12), Gilles Audemard and Laurent Simon, Juin 2012.
+ - "_Improving Glucose for Incremental SAT Solving with Assumption: Application to MUS Extraction_". Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, in Proceedings of SAT 2013, 2013.
+ - "_Lazy Clause Exchange Policy for parallel SAT solvers_". Gilles Audemard, Laurent Simon, in 17th International Conference on Theory and Applications of Satisfiability Testing (SAT'14), 2014.
+ - "_Glucose in the SAT 2014 Competition_". G Audemard, L Simon, SAT Competition, 2014.
 

core/BoundedQueue.h

@@ -1,23 +1,51 @@
-/***********************************************************************************[BoundedQueue.h]
- Glucose -- Copyright (c) 2009, Gilles Audemard, Laurent Simon
-                CRIL - Univ. Artois, France
-                LRI  - Univ. Paris Sud, France
- 
+/***************************************************************************************[BoundedQueue.h]
+ Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon
+                                CRIL - Univ. Artois, France
+                                LRI  - Univ. Paris Sud, France (2009-2013)
+                                Labri - Univ. Bordeaux, France
+
+ Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
+                                CRIL - Univ. Artois, France
+                                Labri - Univ. Bordeaux, France
+
+Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
+Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it 
+is based on. (see below).
+
+Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
+version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
+without restriction, including the rights to use, copy, modify, merge, publish, distribute,
+sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is 
+furnished to do so, subject to the following conditions:
+
+- The above and below copyrights notices and this permission notice shall be included in all
+copies or substantial portions of the Software;
+- The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
+be used in any competitive event (sat competitions/evaluations) without the express permission of 
+the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
+using Glucose Parallel as an embedded SAT engine (single core or not).
+
+
+--------------- Original Minisat Copyrights
+
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
 including without limitation the rights to use, copy, modify, merge, publish, distribute,
 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
 furnished to do so, subject to the following conditions:
- 
+
 The above copyright notice and this permission notice shall be included in all copies or
 substantial portions of the Software.
- 
+
 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
+ **************************************************************************************************/
 
 
 #ifndef BoundedQueue_h
@@ -102,7 +130,17 @@ class bqueue {
 
     void clear(bool dealloc = false)   { elems.clear(dealloc); first = 0; maxsize=0; queuesize=0;sumofqueue=0;}
 
-
+    void copyTo(bqueue &dest) const {
+        dest.last = last;
+        dest.sumofqueue = sumofqueue;
+        dest.maxsize = maxsize;
+        dest.queuesize = queuesize;
+        dest.expComputed = expComputed;
+        dest.exp = exp;
+        dest.value = value;
+        dest.first = first;        
+        elems.copyTo(dest.elems);
+    }
 };
 }
 //=================================================================================================

core/Constants.h

@@ -1,33 +1,59 @@
-/************************************************************************************[Constants.h]
- Glucose -- Copyright (c) 2009, Gilles Audemard, Laurent Simon
-                CRIL - Univ. Artois, France
-                LRI  - Univ. Paris Sud, France
-  
+/***************************************************************************************[Constants.h]
+ Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon
+                                CRIL - Univ. Artois, France
+                                LRI  - Univ. Paris Sud, France (2009-2013)
+                                Labri - Univ. Bordeaux, France
+
+ Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
+                                CRIL - Univ. Artois, France
+                                Labri - Univ. Bordeaux, France
+
+Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
+Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it 
+is based on. (see below).
+
+Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
+version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
+without restriction, including the rights to use, copy, modify, merge, publish, distribute,
+sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is 
+furnished to do so, subject to the following conditions:
+
+- The above and below copyrights notices and this permission notice shall be included in all
+copies or substantial portions of the Software;
+- The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
+be used in any competitive event (sat competitions/evaluations) without the express permission of 
+the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
+using Glucose Parallel as an embedded SAT engine (single core or not).
+
+
+--------------- Original Minisat Copyrights
+
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
 associated documentation files (the "Software"), to deal in the Software without restriction,
 including without limitation the rights to use, copy, modify, merge, publish, distribute,
 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
 furnished to do so, subject to the following conditions:
- 
+
 The above copyright notice and this permission notice shall be included in all copies or
 substantial portions of the Software.
- 
+
 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
-**************************************************************************************************/
+ **************************************************************************************************/
 
 #define DYNAMICNBLEVEL
 #define CONSTANTREMOVECLAUSE
-#define UPDATEVARACTIVITY
 
 // Constants for clauses reductions
 #define RATIOREMOVECLAUSES 2
 
 
-
 // Constants for restarts
 #define LOWER_BOUND_FOR_BLOCKING_RESTART 10000
 

core/Makefile

@@ -1,4 +1,3 @@
-EXEC      = glucose
-DEPDIR    = mtl utils
-MROOT = $(PWD)/..
-include $(MROOT)/mtl/template.mk
+PHONY:
+	@echo "** Careful ** Since 4.0 you have to use the simp or parallel directory only for typing make"
+