Merge pull request #72 from whitemech/feature/minisat

Include Minisat and model enumeration algorithm

.github/workflows/build_cmake.yml

@@ -28,17 +28,6 @@ jobs:
           sudo apt-get install -f flex bison
           sudo apt-get install -f libgraphviz-dev
           sudo python -m pip install gcovr
-      - name: Install Cryptominisat
-        run: |
-          wget https://github.com/msoos/cryptominisat/archive/5.7.1.tar.gz
-          tar -xzvf 5.7.1.tar.gz
-          cd cryptominisat-5.7.1
-          mkdir build
-          cd build
-          cmake ..
-          make
-          sudo make install
-          sudo ldconfig
       - name: Install CUDD
         run: |
           sudo apt-get install -f automake libtool

.gitmodules

@@ -19,3 +19,6 @@
 [submodule "third_party/cppitertools"]
 	path = third_party/cppitertools
 	url = https://github.com/ryanhaining/cppitertools.git
+[submodule "third_party/minisat"]
+	path = third_party/minisat
+	url = https://github.com/whitemech/minisat.git

CMakeLists.txt

@@ -74,7 +74,6 @@ set( CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib )
 set (THREADS_PREFER_PTHREAD_FLAG ON)
 find_package (Threads REQUIRED)
 find_package(cudd REQUIRED)
-find_package(cryptominisat5 REQUIRED)
 find_package(Graphviz REQUIRED)
 find_package(BISON 3.0 REQUIRED)
 find_package(FLEX 2.6 REQUIRED)

CMakeModules/Findortools.cmake

@@ -0,0 +1,97 @@
+if(WIN32)
+    if(NOT TARGET ortools::ortools)
+        find_library(ORTOOLS_LIBRARIES NAME ortools PATH_SUFFIXES lib )
+        find_path(ORTOOLS_INCLUDE_DIRS NAME zlib.h PATH_SUFFIXES include)
+        set(ORTOOLS_DEFINITIONS /DNOMINMAX -DUSE_CBC -DUSE_CLP -DUSE_BOP -DUSE_GLOP)
+
+        add_library(ortools::ortools STATIC IMPORTED GLOBAL)
+        set_target_properties(ortools::ortools PROPERTIES IMPORTED_LOCATION ${ORTOOLS_LIBRARIES} )
+        target_include_directories(ortools::ortools INTERFACE ${ORTOOLS_INCLUDE_DIRS})
+        target_link_libraries(ortools::ortools INTERFACE ${ORTOOLS_LIBRARIES})
+        target_compile_options(ortools::ortools INTERFACE ${ORTOOLS_DEFINITIONS})
+
+        include(FindPackageHandleStandardArgs)
+        # handle the QUIETLY and REQUIRED arguments and set ortools to TRUE
+        # if all listed variables are TRUE
+        find_package_handle_standard_args(ortools_FOUND  REQUIRED_VARS
+                ORTOOLS_LIBRARIES ORTOOLS_INCLUDE_DIRS)
+
+    endif()
+elseif(UNIX)
+    if(NOT TARGET ortools::ortools)
+        # Include directories
+        find_path(ORTOOLS_INCLUDE_DIRS NAME ortools PATH_SUFFIXES include/)
+        message(STATUS "ortools found here : ${ORTOOLS_INCLUDE_DIRS}")
+
+        ## Libraries
+        set(LIB_TO_FIND
+                CbcSolver #CBC_LNK
+                Cbc
+                OsiCbc
+                Cgl
+                ClpSolver
+                Clp
+                OsiClp
+                Osi
+                CoinUtils
+                absl_bad_any_cast_impl #ABSL_LNK
+                absl_bad_optional_access
+                absl_bad_variant_access
+                absl_base
+                absl_city
+                absl_civil_time
+                absl_debugging_internal
+                absl_demangle_internal
+                absl_dynamic_annotations
+                absl_examine_stack
+                absl_failure_signal_handler
+                absl_graphcycles_internal
+                absl_hash
+                absl_hashtablez_sampler
+                absl_int128
+                absl_leak_check
+                absl_malloc_internal
+#                absl_optional
+                absl_raw_hash_set
+                absl_spinlock_wait
+                absl_stacktrace
+                absl_str_format_internal
+                absl_strings
+                absl_strings_internal
+                absl_symbolize
+                absl_synchronization
+                absl_throw_delegate
+                absl_time
+                absl_time_zone
+                protobuf #protobuf
+                glog #glog
+                gflags #gflags
+                ortools #ortools
+                )
+
+        foreach(X ${LIB_TO_FIND})
+            find_library(LIB_${X} NAME ${X} PATH_SUFFIXES lib/)
+            message(STATUS "${X} lib found here : ${LIB_${X}}")
+            set(ORTOOLS_LIBRARIES ${ORTOOLS_LIBRARIES} ${LIB_${X}})
+        endforeach()
+
+
+        # Definitions
+        set(ORTOOLS_DEFINITIONS -DUSE_CBC -DUSE_CLP -DUSE_BOP -DUSE_GLOP)
+
+
+        add_library(ortools INTERFACE)
+        add_library(ortools::ortools ALIAS ortools)
+        target_include_directories(ortools INTERFACE ${ORTOOLS_INCLUDE_DIRS})
+        target_link_libraries(ortools INTERFACE ${ORTOOLS_LIBRARIES})
+        target_compile_options(ortools INTERFACE ${ORTOOLS_DEFINITIONS})
+
+        include(FindPackageHandleStandardArgs)
+        # handle the QUIETLY and REQUIRED arguments and set ortools to TRUE
+        # if all listed variables are TRUE
+        find_package_handle_standard_args(ortools_FOUND
+                REQUIRED_VARS ORTOOLS_LIBRARIES ORTOOLS_INCLUDE_DIRS)
+    endif()
+else()
+    message(FATAL_ERROR "No other platform supported yet")
+endif()

README.md

@@ -58,17 +58,16 @@ sudo make install
   3. Using a version of aclocal other than 1.14:
      modify the version 1.14 in configure accordingly.
 
-# CryptoMiniSat
+## ZLib
 
-We use Cryptominisat as SAT solver library.
+The software depends on MiniSAT Solver, which in turn depends
+on [ZLib](https://www.zlib.net/).
 
-For Ubuntu systems:
-```
-sudo apt-get install libcryptominisat5-dev
-```
+To install it, e.g. on Ubuntu:
 
-For other systems, please look at
-the [documentation](https://github.com/msoos/cryptominisat#compiling-in-linux).
+```bash
+sudo apt-get install zlib1g-dev
+```
 
 ## Graphviz
 

lib/CMakeLists.txt

@@ -46,7 +46,10 @@ add_library (${LIB_NAME}
         ${BISON_lydia_parser_OUTPUTS}
         ${FLEX_lydia_lexer_OUTPUTS})
 
-target_link_libraries(${LIB_NAME} ${CUDD_LIBRARIES} ${GRAPHVIZ_LIBRARIES} ${CRYPTOMINISAT5_LIBRARIES})
+target_link_libraries(${LIB_NAME}
+        ${CUDD_LIBRARIES}
+        ${GRAPHVIZ_LIBRARIES}
+        ${MINISAT_LIBRARIES})
 
 #export vars
 set (LIBRARY_INCLUDE_PATH  ${LIBRARY_INCLUDE_PATH} PARENT_SCOPE)

lib/benchmark/src/pl.cpp

@@ -17,43 +17,93 @@
 
 #include <benchmark/benchmark.h>
 #include <lydia/pl/logic.hpp>
-#include <lydia/pl/models_sat.hpp>
+#include <lydia/pl/models/naive.hpp>
+#include <lydia/pl/models/sat.hpp>
 #include <lydia/utils/benchmark.hpp>
+#include <minisat/simp/SimpSolver.h>
 #include <random>
 
 namespace whitemech::lydia::Benchmark {
 
-static void BM_pl_models_cryptominisat_true(benchmark::State &state) {
-  auto solver = CMSat::SATSolver();
-  solver.set_num_threads(4);
+static void BM_pl_models_minisat_1(benchmark::State &state) {
   for (auto _ : state) {
-    auto result = solver.solve();
-    escape(&result);
-    (void)result;
+    Minisat::SimpSolver solver;
+    solver.verbosity = -1;
+
+    // Create variables
+    auto A = solver.newVar();
+    auto B = solver.newVar();
+    auto C = solver.newVar();
+
+    // Create the clauses
+    solver.addClause(Minisat::mkLit(A), Minisat::mkLit(B), Minisat::mkLit(C));
+    solver.addClause(~Minisat::mkLit(A), Minisat::mkLit(B), Minisat::mkLit(C));
+    solver.addClause(Minisat::mkLit(A), ~Minisat::mkLit(B), Minisat::mkLit(C));
+    solver.addClause(Minisat::mkLit(A), Minisat::mkLit(B), ~Minisat::mkLit(C));
+
+    // Check for solution and retrieve model if found
+    auto sat = solver.solve();
+
+    escape((void *)&sat);
+    (void)sat;
   }
 }
-BENCHMARK(BM_pl_models_cryptominisat_true);
+BENCHMARK(BM_pl_models_minisat_1);
 
-static void BM_pl_models_cryptominisat_false(benchmark::State &state) {
-  auto solver = CMSat::SATSolver();
-  solver.set_num_threads(4);
-  solver.add_clause(std::vector<CMSat::Lit>());
+static void BM_pl_models_naive_all_models_tautology(benchmark::State &state) {
+  auto t = boolean_prop(true);
   for (auto _ : state) {
-    auto result = solver.solve();
-    escape(&result);
-    (void)result;
+    auto m = all_models<NaiveModelEnumerationStategy>(*t);
+    escape(&m);
+    (void)m;
+  }
+}
+BENCHMARK(BM_pl_models_naive_all_models_tautology);
+
+static void BM_pl_models_sat_all_models_tautology(benchmark::State &state) {
+  auto t = boolean_prop(true);
+  for (auto _ : state) {
+    auto m = all_models<SATModelEnumerationStategy>(*t);
+    escape(&m);
+    (void)m;
+  }
+}
+BENCHMARK(BM_pl_models_sat_all_models_tautology);
+
+static void BM_pl_models_naive_all_models_or(benchmark::State &state) {
+  auto t = boolean_prop(true);
+  for (auto _ : state) {
+    auto N = state.range(0);
+    auto operands = std::vector<prop_ptr>();
+    operands.reserve(N);
+    for (int i = 0; i < N; i++) {
+      operands.push_back(prop_atom(UniquePropositionalSymbol()));
+    }
+    auto f = logical_or(set_prop_formulas(operands.begin(), operands.end()));
+    auto m = all_models<NaiveModelEnumerationStategy>(*f);
+    assert(m.size() == 2 << N);
+    escape(&m);
+    (void)m;
   }
 }
-BENCHMARK(BM_pl_models_cryptominisat_false);
+BENCHMARK(BM_pl_models_naive_all_models_or)->Arg(5)->Arg(10)->Arg(15);
 
-static void BM_pl_models_sat_all_models_t(benchmark::State &state) {
+static void BM_pl_models_sat_all_models_or(benchmark::State &state) {
   auto t = boolean_prop(true);
   for (auto _ : state) {
-    auto m = all_models_sat(*t);
+    auto N = state.range(0);
+    auto operands = std::vector<prop_ptr>();
+    operands.reserve(N);
+    for (int i = 0; i < N; i++) {
+      operands.push_back(prop_atom(UniquePropositionalSymbol()));
+    }
+    auto f = logical_or(set_prop_formulas(operands.begin(), operands.end()));
+    auto m = all_models<SATModelEnumerationStategy>(*t);
+    assert(m.size() == 2 << N);
     escape(&m);
     (void)m;
   }
 }
-BENCHMARK(BM_pl_models_sat_all_models_t);
+BENCHMARK(BM_pl_models_sat_all_models_or)->Arg(5)->Arg(10)->Arg(20)->Arg(50);
 
 } // namespace whitemech::lydia::Benchmark

lib/benchmark/src/to_dfa.cpp

@@ -105,9 +105,9 @@ static void BM_translate_sequence_of_stars_of_atoms(benchmark::State &state) {
 // clang-format off
 BENCHMARK(BM_translate_sequence_of_stars_of_atoms)
   ->Arg(5)->Arg(10)->Arg(15)
-//  ->Arg(20)->Arg(25)->Arg(30)
-//  ->Arg(40)->Arg(80)->Arg(100)
-//  ->Arg(200)->Arg(500)->Arg(1000)
+  ->Arg(20)->Arg(25)->Arg(30)
+  ->Arg(40)->Arg(80)->Arg(100)
+  ->Arg(200)->Arg(500)->Arg(1000)
   ->Unit(benchmark::kMillisecond)
   ->Repetitions(5)
   ->DisplayAggregatesOnly(true);
@@ -134,9 +134,9 @@ static void BM_translate_union(benchmark::State &state) {
 // clang-format off
 BENCHMARK(BM_translate_union)
 ->Arg(5)->Arg(10)->Arg(15)
-//->Arg(20)->Arg(25)->Arg(30)
-//->Arg(40)->Arg(80)->Arg(100)
-//->Arg(200)->Arg(500)->Arg(1000)
+->Arg(20)->Arg(25)->Arg(30)
+->Arg(40)->Arg(80)->Arg(100)
+->Arg(200)->Arg(500)->Arg(1000)
 ->Unit(benchmark::kMillisecond)
 ->Repetitions(5)
 ->DisplayAggregatesOnly(true);

lib/include/lydia/basic.hpp

@@ -122,10 +122,6 @@ class Basic : public std::enable_shared_from_this<Basic> {
   int compare_(const Basic &o) const;
   virtual void accept(Visitor &v) const = 0;
   std::string str() const;
-
-  template <typename Derived> std::shared_ptr<Derived> shared_from_base() {
-    return std::static_pointer_cast<Derived>(shared_from_this());
-  }
 };
 
 // TODO decide what to do with this:

lib/include/lydia/pl/cnf.hpp

@@ -28,22 +28,6 @@ class CNFTransformer : public Visitor {
   std::shared_ptr<const PropositionalFormula> result;
 
 public:
-  // callbacks for LDLf
-  void visit(const Symbol &) override{};
-  void visit(const LDLfBooleanAtom &) override{};
-  void visit(const LDLfAnd &) override{};
-  void visit(const LDLfOr &) override{};
-  void visit(const LDLfNot &) override{};
-  void visit(const LDLfDiamond &x) override{};
-  void visit(const LDLfBox &x) override{};
-
-  // callbacks for regular expressions
-  void visit(const PropositionalRegExp &) override{};
-  void visit(const TestRegExp &) override{};
-  void visit(const UnionRegExp &) override{};
-  void visit(const SequenceRegExp &) override{};
-  void visit(const StarRegExp &) override{};
-
   // callbacks for propositional logic
   void visit(const PropositionalTrue &) override;
   void visit(const PropositionalFalse &) override;
@@ -62,5 +46,8 @@ class CNFTransformer : public Visitor {
 set_prop_formulas to_container(prop_ptr p);
 prop_ptr to_cnf(const PropositionalFormula &);
 
+std::vector<std::vector<PropositionalAtom>>
+to_clauses(const PropositionalFormula &cnf_f);
+
 } // namespace lydia
 } // namespace whitemech