stp · nindanaoto · Oct 22, 2024
diff --git a/.dockerignore b/.dockerignore
@@ -25,3 +25,4 @@ todo*
 utils
 windows
 Dockerfile
+!scripts/deps/setup-kissat.sh
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -45,6 +45,7 @@ jobs:
       run: |
         ./scripts/deps/setup-minisat.sh
         ./scripts/deps/setup-cms.sh
+        ./scripts/deps/setup-kissat.sh
         ./scripts/deps/setup-gtest.sh
         ./scripts/deps/setup-outputcheck.sh
 

diff --git a/.gitignore b/.gitignore
@@ -9,3 +9,4 @@ docs/_build
 .DS_Store
 .direnv
 build
+scripts/deps/kissat
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -522,6 +522,18 @@ if (FORCE_CMS AND NOT USE_CRYPTOMINISAT)
     message(FATAL_ERROR "CryptoMiniSat 5.x was not found but it was requested. Exiting.")
 endif()
 
+# -----------------------------------------------------------------------------
+# Find Kissat
+# -----------------------------------------------------------------------------
+option(USE_KISSAT "Try to use Kissat" OFF)
+add_feature_info(Kissat USE_KISSAT "Enables Kissat solver")
+
+if (USE_KISSAT)
+    add_definitions(-DUSE_KISSAT)
+    include_directories(${PROJECT_SOURCE_DIR}/scripts/deps/)
+    link_directories(${PROJECT_SOURCE_DIR}/scripts/deps/kissat/build)
+endif()
+
 # -----------------------------------------------------------------------------
 # Find ZLIB (needed for MiniSat)
 # yes, we need to include the zlib header location or STP will not build

diff --git a/Dockerfile b/Dockerfile
@@ -16,6 +16,7 @@ RUN apt-get update \
         flex \
         g++ \
         gcc \
+        git \
         libboost-program-options-dev \
         libgmp-dev \
         libm4ri-dev \
@@ -48,8 +49,10 @@ RUN wget -O minisat.tgz https://github.com/stp/minisat/archive/releases/2.2.1.ta
  && cmake --install .
 
 # Build STP
-WORKDIR /stp/build
 COPY . /stp
+WORKDIR /stp
+RUN ./scripts/deps/setup-kissat.sh
+WORKDIR /stp/build
 RUN cmake .. \
         -DCMAKE_BUILD_TYPE=Release \
         -DENABLE_ASSERTIONS=OFF \

diff --git a/include/stp/STPManager/UserDefinedFlags.h b/include/stp/STPManager/UserDefinedFlags.h
@@ -154,7 +154,8 @@ struct UserDefinedFlags
     MINISAT_SOLVER = 0,
     SIMPLIFYING_MINISAT_SOLVER,
     CRYPTOMINISAT5_SOLVER,
-    RISS_SOLVER
+    RISS_SOLVER,
+    KISSAT_SOLVER
   };
 
   enum SATSolvers solver_to_use;

diff --git a/include/stp/Sat/Kissat.h b/include/stp/Sat/Kissat.h
@@ -0,0 +1,78 @@
+/********************************************************************
+ * AUTHORS: Kotaro Matsuoka
+ *
+ * BEGIN DATE: Oct, 2024
+ *
+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.
+********************************************************************/
+
+/*
+ * Wraps around Kissat.
+ */
+#ifndef KISSAT_H_
+#define KISSAT_H_
+
+#include "stp/Sat/SATSolver.h"
+extern "C" {
+#include "kissat/src/kissat.h"
+}
+#include <unordered_set>
+
+namespace stp
+{
+#if defined(__GNUC__) || defined(__clang__)
+  class __attribute__((visibility("default"))) Kissat : public SATSolver
+#else
+  class Kissat : public SATSolver
+#endif
+
+{
+  kissat * s;
+
+public:
+  Kissat();
+
+  ~Kissat();
+
+  virtual void setMaxConflicts(int64_t max_confl); // set max solver conflicts
+
+  bool addClause(const vec_literals& ps); // Add a clause to the solver.
+
+  bool okay() const; // FALSE means solver is in a conflicting state
+
+  bool solve(bool& timeout_expired); // Search without assumptions.
+
+  virtual uint8_t modelValue(uint32_t x) const;
+
+  virtual uint32_t newVar();
+
+  void setVerbosity(int v);
+
+  unsigned long nVars() const;
+
+  void printStats() const;
+
+  // nb Kissat has different literal values to the other minisats.
+  virtual lbool true_literal() { return ((uint8_t)1); }
+  virtual lbool false_literal() { return ((uint8_t)-1); }
+  virtual lbool undef_literal() { return ((uint8_t)0); }
+};
+}
+
+#endif
diff --git a/include/stp/c_interface.h b/include/stp/c_interface.h
@@ -177,6 +177,10 @@ enum ifaceflag_t
   //!
   RISS,
 
+  //! Use the SAT solver Kissat.
+  //!
+  KISSAT,
+
   //! \brief Deprecated: use `MS` instead!
   //!
   //! This used to be the array version of the minisat SAT solver.
@@ -1225,6 +1229,17 @@ DLL_PUBLIC bool vc_useRiss(VC vc);
 //!
 DLL_PUBLIC bool vc_isUsingRiss(VC vc);
 
+//! \brief Checks if STP was compiled with support for Kissat
+//!
+DLL_PUBLIC bool vc_supportsKissat(VC vc);
+
+//! \brief Sets underlying SAT solver to Kissat
+//!
+DLL_PUBLIC bool vc_useKissat(VC vc);
+
+//! \brief Checks if underlying SAT solver is Kissat
+//!
+DLL_PUBLIC bool vc_isUsingKissat(VC vc);
 
 #ifdef __cplusplus
 }

diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt
@@ -151,6 +151,11 @@ if (USE_RISS)
         ${stp_link_libs} -lriss-coprocessor)
 endif()
 
+if (USE_KISSAT)
+    set(stp_link_libs
+        ${stp_link_libs} -lkissat)
+endif()
+
 target_link_libraries(stp
     LINK_PUBLIC ${stp_link_libs}
 )

diff --git a/lib/Interface/c_interface.cpp b/lib/Interface/c_interface.cpp
@@ -141,6 +141,9 @@ void vc_setInterfaceFlags(VC vc, enum ifaceflag_t f, int param_value)
       //Array-based Minisat has been replaced with normal MiniSat
       b->UserFlags.solver_to_use = stp::UserDefinedFlags::MINISAT_SOLVER;
       break;
+    case KISSAT:
+      b->UserFlags.solver_to_use = stp::UserDefinedFlags::KISSAT_SOLVER;
+      break;
     default:
       stp::FatalError("C_interface: vc_setInterfaceFlags: Unrecognized flag\n");
       break;
@@ -2305,3 +2308,38 @@ vc
 #endif
 }
 
+bool vc_supportsKissat(VC /*vc*/ )
+{
+#ifdef USE_KISSAT
+  return true;
+#else
+  return false;
+#endif
+}
+
+bool vc_useKissat(VC
+#ifdef USE_KISSAT
+vc
+#endif
+)
+{
+#ifdef USE_KISSAT
+  _vc_useSolver(vc, stp::UserDefinedFlags::KISSAT_SOLVER);
+  return true;
+#else
+  return false;
+#endif
+}
+
+bool vc_isUsingKissat(VC
+#ifdef USE_KISSAT
+vc
+#endif
+)
+{
+#ifdef USE_KISSAT
+  return _vc_isUsingSolver(vc, stp::UserDefinedFlags::KISSAT_SOLVER);
+#else
+  return false;
+#endif
+}
diff --git a/lib/STPManager/STP.cpp b/lib/STPManager/STP.cpp
@@ -37,6 +37,10 @@ THE SOFTWARE.
 #include "stp/Sat/Riss.h"
 #endif
 
+#ifdef USE_KISSAT
+#include "stp/Sat/Kissat.h"
+#endif
+
 #include "stp/Sat/MinisatCore.h"
 #include "stp/Sat/SimplifyingMinisat.h"
 
@@ -113,6 +117,15 @@ SATSolver* STP::get_new_sat_solver()
       std::cerr << "Riss support was not enabled at configure time."
                 << std::endl;
       exit(-1);
+#endif
+      break;
+    case UserDefinedFlags::KISSAT_SOLVER:
+#ifdef USE_KISSAT
+      newS = new Kissat();
+#else
+      std::cerr << "Kissat support was not enabled at configure time."
+                << std::endl;
+      exit(-1);
 #endif
       break;
     case UserDefinedFlags::MINISAT_SOLVER:

diff --git a/lib/Sat/CMakeLists.txt b/lib/Sat/CMakeLists.txt
@@ -32,5 +32,9 @@ if (USE_RISS)
     set(sat_lib_to_add ${sat_lib_to_add} RissCore.cpp)
 endif()
 
+if (USE_KISSAT)
+    set(sat_lib_to_add ${sat_lib_to_add} Kissat.cpp)
+endif()
+
 add_library(sat OBJECT ${sat_lib_to_add})
 
diff --git a/lib/Sat/Kissat.cpp b/lib/Sat/Kissat.cpp
@@ -0,0 +1,118 @@
+/********************************************************************
+ * AUTHORS: Kotaro Matsuoka
+ *
+ * BEGIN DATE: Oct, 2024
+ *
+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.
+********************************************************************/
+
+#include "stp/Sat/Kissat.h"
+#include <unordered_set>
+#include <algorithm>
+
+namespace stp
+{
+
+Kissat::Kissat()
+{
+  s = kissat_init();
+  kissat_set_option(s, "quiet", 1);
+}
+
+Kissat::~Kissat()
+{
+  kissat_release(s);
+}
+
+void Kissat::setMaxConflicts(int64_t _max_confl)
+{
+  if(_max_confl > 0)
+    kissat_set_conflict_limit(s,_max_confl);
+}
+
+// void Kissat::setMaxTime(int64_t _max_time)
+// {
+//   max_time = _max_time;
+// }
+
+bool Kissat::addClause(
+    const vec_literals& ps) // Add a clause to the solver.
+{
+
+  for (int i = 0; i < ps.size(); i++)
+    // kissat_add(s,ps[i].x);
+    kissat_add(s,ps[i].x&1?-(ps[i].x>>1):(ps[i].x>>1));
+  kissat_add(s,0);
+  return true;
+}
+
+bool Kissat::okay()
+    const // FALSE means solver is in a conflicting state
+{
+  return kissat_okay(s);
+}
+
+bool Kissat::solve(bool& timeout_expired) // Search without assumptions.
+{
+
+  int32_t res = kissat_solve(s);
+  if (res == 10)
+  {
+    return true;
+  }
+  else if (res == 20)
+  {
+    return false;
+  }
+  else
+  {
+    timeout_expired = true;
+    return false;
+  }
+}
+
+uint8_t Kissat::modelValue(uint32_t x) const
+{
+  int32_t val = kissat_value(s,x);
+  if (val > 0) return 1;
+  else if (val < 0) return -1;
+  else return 0;
+}
+
+uint32_t Kissat::newVar()
+{
+  return kissat_new_var(s);
+}
+
+void Kissat::setVerbosity(int v)
+{
+  kissat_set_option(s, "verbose", v);
+}
+
+unsigned long Kissat::nVars() const
+{
+  return kissat_nvars(s);
+}
+
+void Kissat::printStats() const
+{
+  kissat_print_statistics(s);
+}
+
+} //end namespace stp
-Original file line number
+Diff line change
@@ Expand Up / @@ -25,3 +25,4 @@ todo* @@
     utils
     windows
     Dockerfile
+    !scripts/deps/setup-kissat.sh