feat: add GMPC

3rdParty/GPMC/CHANGELOG.md

@@ -0,0 +1,19 @@
+# Change Log
+
+## [1.1.1] - 2022/08/26
+### Added
+- Add a function to contruct a d-DNNF with a variable mapping
+- Deal with natural number weights of literals (-natw option)
+
+### Changed
+- Improve the preprocessor (refactoring)
+- change the public methods of Counter class
+
+## [1.1] - 2022/06/21
+### Added
+- Add a preprocessor for simplying input CNF. 
+- Use FlowCutter for tree decomposition. The result is used for variable selection heuristics. 
+- Deal with Weighted model counting
+
+### Removed
+- Options "-pp" and "-upto"

3rdParty/GPMC/CMakeLists.txt

@@ -0,0 +1,44 @@
+cmake_minimum_required(VERSION 3.0)
+
+project(GMPC VERSION 2.0.0 LANGUAGES CXX)
+
+set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_CURRENT_SOURCE_DIR}/cmake")
+
+find_package(GMP REQUIRED)
+find_package(arjun REQUIRED)
+find_package(ZLIB REQUIRED)
+
+include_directories(${CMAKE_CURRENT_SOURCE_DIR})
+include_directories(${CMAKE_CURRENT_SOURCE_DIR}/include)
+include_directories(${CMAKE_CURRENT_SOURCE_DIR}/../..)
+include_directories(${GMP_INCLUDE_DIRS})
+include_directories(${GMPXX_INCLUDE_DIRS})
+include_directories(${arjun_INCLUDE_DIR})
+include_directories(${ZLIB_INCLUDE_DIR})
+
+add_subdirectory(flow-cutter-pace17)
+
+add_library(gpmc
+	core/ComponentCache.cc
+	core/ComponentManager.cc
+	core/Counter.cc
+	core/Config.cc
+	core/Instance.cc
+	ddnnf/DecisionTree.cc
+	core/Solver.cc 
+	utils/Options.cc
+	utils/System.cc
+	preprocessor/Preprocessor.cc
+	preprocessor/TestSolver.cc
+	preprocessor/lib_sharpsat_td/subsumer.cpp
+	preprocessor/TreeDecomposition.cc
+	preprocessor/IFlowCutter.cc
+    core/gpmc.cpp
+    core/Solver.h
+)
+
+set_target_properties(gpmc PROPERTIES PUBLIC_HEADER include/gpmc.hpp)
+
+target_link_libraries(gpmc GMP::GMP GMP::GMPXX arjun ZLIB::ZLIB flowcutter)
+
+install(TARGETS gpmc)

3rdParty/GPMC/LICENSE.md

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2020 Kenji Hashimoto
+
+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.

3rdParty/GPMC/README.md

@@ -0,0 +1,66 @@
+# GPMC
+
+GPMC is an exact model counter for CNF formulas. The current version of GPMC supports model counting, weighted model counting, projected model counting, and weighted projected model counting.
+
+The source codes of this software are based on those of MiniSat-based Sat solver [Glucose1 3.0](https://www.labri.fr/perso/lsimon/Glucose1/) and [SharpSAT](https://github.com/marcthurley/sharpSAT) 12.08.1.
+And also, inspired by [sharpSAT-TD](https://github.com/Laakeri/sharpsat-td), the current version incorporates 
+a preprocessor for simplifying input formulas, and uses tree decomposition in decision heuristics. 
+In the implementation, we use a part of source files of the preprocessor in sharpSAT-TD, and use [FlowCutter](https://github.com/kit-algo/flow-cutter-pace17) for tree decomposition.
+
+## Installation
+See `INSTALL.md`.
+
+## Usage
+```
+$ ./gpmc [options] [file]
+```
+Options:
+
+-  -mode=<0..3>
+    - 0 : Model Counting
+    - 1 : Weighted Model Counting
+    - 2 : Projected Model Counting
+    - 3 : Weighted Projected Model Counting 
+
+-  -ddnnf  / -no-ddnnf  
+	construct a d-DNNF with a variable mapping (default: off).  
+	The d-DNNF is for the CNF simplified by the preprocessor.  
+	The information about the correspondence between the input and simplified CNF is maintained.
+
+-  -nnfout=\<string\>  
+	write a constructed d-DNNF to the specified file when -ddnnf is set (default: no file output). 
+    The variable correpondance 
+
+-  -natw / -no-natw  
+    use mpz_class as the internal data type for weights when weighted model counting (default: off, use mpfr::mpreal).  
+    Note that we must give natual number weights for each literals in an input file (like "c p weight 1 2 0").
+
+-  -prec=\<1..intmax>  
+    set the precision of floating-point numbers (default: 15).
+
+-  -cs=\<1..intmax>  
+    set maximum component cache size (MB) (default: 4000)  
+    NOTE: This bound is only for component cache. GPMC may use much more memory.
+
+## Input file format
+Input boolean formulas should be in DIMACS CNF format, together with additional information, weights and projection variables.
+GPMC supports the [MCC2021 format](https://mccompetition.org/assets/files/2021/competition2021.pdf). 
+
+Example:
+
+```
+p cnf 3 4
+c p show 2 3 0
+c p weight 2 0.6 0
+c p weight -2 0.4 0
+-1 2 0
+-2 3 0
+2 -3 0
+1 -2 3 0
+```
+The set of projection variables is { 2, 3 }.
+The weight of the positive literal of var 2 is 0.6, and that of the negative one is 0.4.
+
+## Author
+[Kenji Hashimoto](https://www.trs.cm.is.nagoya-u.ac.jp/~k-hasimt/index-e.html),
+Nagoya University, Japan.

3rdParty/GPMC/cmake/FindGMP.cmake

@@ -0,0 +1,78 @@
+include(FindPackageHandleStandardArgs)
+
+# Keep track of the original library suffixes to reset them later.
+set(_gmp_ORIG_CMAKE_FIND_LIBRARY_SUFFIXES ${CMAKE_FIND_LIBRARY_SUFFIXES})
+
+# Look for .a or .lib libraries in case of a static library.
+if(GMP_USE_STATIC_LIBS)
+    set(CMAKE_FIND_LIBRARY_SUFFIXES .a .lib)
+endif()
+
+# Find libraries and headers.
+find_library(GMP_LIBRARY NAMES gmp)
+find_path(GMP_INCLUDE_DIR NAMES gmp.h)
+
+find_library(GMPXX_LIBRARY NAMES gmpxx)
+find_path(GMPXX_INCLUDE_DIR NAMES gmpxx.h)
+
+# Windows (dynamic): Also find import libraries.
+if(WIN32 AND NOT GMP_USE_STATIC_LIBS)
+    set(CMAKE_FIND_LIBRARY_SUFFIXES .dll.a .lib)
+    find_library(GMP_IMPORT_LIBRARY NAMES gmp)
+    find_library(GMPXX_IMPORT_LIBRARY NAMES gmpxx)
+endif()
+
+# Reset library suffixes.
+set(CMAKE_FIND_LIBRARY_SUFFIXES ${_gmp_ORIG_CMAKE_FIND_LIBRARY_SUFFIXES})
+
+# Register the found package.
+if(WIN32 AND NOT GMP_USE_STATIC_LIBS)
+    # Windows (dynamic): also require import libraries.
+    find_package_handle_standard_args(GMP REQUIRED_VARS GMP_LIBRARY GMP_IMPORT_LIBRARY GMP_INCLUDE_DIR GMPXX_LIBRARY GMPXX_IMPORT_LIBRARY GMPXX_INCLUDE_DIR)
+else()
+    find_package_handle_standard_args(GMP REQUIRED_VARS GMP_LIBRARY GMP_INCLUDE_DIR GMPXX_LIBRARY GMPXX_INCLUDE_DIR)
+endif()
+
+if(GMP_FOUND)
+    mark_as_advanced(GMP_LIBRARY)
+    mark_as_advanced(GMP_IMPORT_LIBRARY)
+    mark_as_advanced(GMP_INCLUDE_DIR)
+    mark_as_advanced(GMPXX_LIBRARY)
+    mark_as_advanced(GMPXX_IMPORT_LIBRARY)
+    mark_as_advanced(GMPXX_INCLUDE_DIR)
+
+    # Create targets in case not already done.
+    if(NOT TARGET GMP::GMP)
+        if(GMP_USE_STATIC_LIBS)
+            add_library(GMP::GMP STATIC IMPORTED)
+        else()
+            add_library(GMP::GMP SHARED IMPORTED)
+        endif()
+
+        # Set library and include paths.
+        set_target_properties(GMP::GMP PROPERTIES IMPORTED_LOCATION ${GMP_LIBRARY})
+        target_include_directories(GMP::GMP INTERFACE ${GMP_INCLUDE_DIR})
+
+        # Windows (dynamic): Also set import library.
+        if(WIN32 AND NOT GMP_USE_STATIC_LIBS)
+            set_target_properties(GMP::GMP PROPERTIES IMPORTED_IMPLIB ${GMP_IMPORT_LIBRARY})
+        endif()
+    endif()
+
+    if(NOT TARGET GMP::GMPXX)
+        if(GMP_USE_STATIC_LIBS)
+            add_library(GMP::GMPXX STATIC IMPORTED)
+        else()
+            add_library(GMP::GMPXX SHARED IMPORTED)
+        endif()
+
+        # Set library and include paths.
+        set_target_properties(GMP::GMPXX PROPERTIES IMPORTED_LOCATION ${GMPXX_LIBRARY})
+        target_include_directories(GMP::GMPXX INTERFACE ${GMPXX_INCLUDE_DIR})
+
+        # Windows (dynamic): Also set import library.
+        if(WIN32 AND NOT GMP_USE_STATIC_LIBS)
+            set_target_properties(GMP::GMPXX PROPERTIES IMPORTED_IMPLIB ${GMPXX_IMPORT_LIBRARY})
+        endif()
+    endif()
+endif()

3rdParty/GPMC/core/BoundedQueue.h

@@ -0,0 +1,110 @@
+/***********************************************************************************[BoundedQueue.h]
+ Glucose1 -- Copyright (c) 2009, Gilles Audemard, Laurent Simon
+                CRIL - Univ. Artois, France
+                LRI  - Univ. Paris Sud, France
+ 
+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
+#define BoundedQueue_h
+
+#include "mtl/Vec.h"
+
+//=================================================================================================
+
+namespace Glucose1 {
+
+template <class T>
+class bqueue {
+    vec<T>  elems;
+    int     first;
+	int		last;
+	unsigned long long sumofqueue;
+	int     maxsize;
+	int     queuesize; // Number of current elements (must be < maxsize !)
+	bool expComputed;
+	double exp,value;
+public:
+ bqueue(void) : first(0), last(0), sumofqueue(0), maxsize(0), queuesize(0),expComputed(false) { } 
+
+	void initSize(int size) {growTo(size);exp = 2.0/(size+1);} // Init size of bounded size queue
+
+	void push(T x) {
+	  expComputed = false;
+		if (queuesize==maxsize) {
+			assert(last==first); // The queue is full, next value to enter will replace oldest one
+			sumofqueue -= elems[last];
+			if ((++last) == maxsize) last = 0;
+		} else 
+			queuesize++;
+		sumofqueue += x;
+		elems[first] = x;
+		if ((++first) == maxsize) {first = 0;last = 0;}
+	}
+
+	T peek() { assert(queuesize>0); return elems[last]; }
+	void pop() {sumofqueue-=elems[last]; queuesize--; if ((++last) == maxsize) last = 0;}
+
+	unsigned long long getsum() const {return sumofqueue;}
+	unsigned int getavg() const {return (unsigned int)(sumofqueue/((unsigned long long)queuesize));}
+	int maxSize() const {return maxsize;}
+	double getavgDouble() const {
+	  double tmp = 0;
+	  for(int i=0;i<elems.size();i++) {
+	    tmp+=elems[i];
+	  }
+	  return tmp/elems.size();
+	}
+	int isvalid() const {return (queuesize==maxsize);}
+
+	void growTo(int size) {
+		elems.growTo(size); 
+		first=0; maxsize=size; queuesize = 0;last = 0;
+		for(int i=0;i<size;i++) elems[i]=0; 
+	}
+
+	double getAvgExp() {
+	  if(expComputed) return value;
+	  double a=exp;
+	  value = elems[first];
+	  for(int i  = first;i<maxsize;i++) {
+	    value+=a*((double)elems[i]);
+	    a=a*exp;
+	  }
+	  for(int i  = 0;i<last;i++) {
+	    value+=a*((double)elems[i]);
+	    a=a*exp;
+	  }
+	  value = value*(1-exp)/(1-a);
+	  expComputed = true;
+	  return value;
+
+
+	}
+	void fastclear() {first = 0; last = 0; queuesize=0; sumofqueue=0;} // to be called after restarts... Discard the queue
+
+    int  size(void)    { return queuesize; }
+
+    void clear(bool dealloc = false)   { elems.clear(dealloc); first = 0; maxsize=0; queuesize=0;sumofqueue=0;}
+
+
+};
+}
+//=================================================================================================
+
+#endif