From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 22 May 2020 13:41:50 +0000 (-0700)
Subject: Add support for SAT solver Kissat. (#4514)
X-Git-Tag: cvc5-1.0.0~3300
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c531152e6a707b66b885e508ea61e2a67e195ccc;p=cvc5.git

Add support for SAT solver Kissat. (#4514)
---

diff --git a/CMakeLists.txt b/CMakeLists.txt
index c535890e1..d34d6ebfe 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -67,6 +67,9 @@ endif()
 if(GMP_DIR)
   list(APPEND CMAKE_PREFIX_PATH "${GMP_DIR}")
 endif()
+if(KISSAT_DIR)
+  list(APPEND CMAKE_PREFIX_PATH "${KISSAT_DIR}")
+endif()
 if(LFSC_DIR)
   list(APPEND CMAKE_PREFIX_PATH "${LFSC_DIR}")
 endif()
@@ -143,8 +146,9 @@ option(ENABLE_PROFILING        "Enable support for gprof profiling")
 cvc4_option(USE_ABC           "Use ABC for AIG bit-blasting")
 cvc4_option(USE_CADICAL       "Use CaDiCaL SAT solver")
 cvc4_option(USE_CLN           "Use CLN instead of GMP")
-cvc4_option(USE_GLPK          "Use GLPK simplex solver")
 cvc4_option(USE_CRYPTOMINISAT "Use CryptoMiniSat SAT solver")
+cvc4_option(USE_GLPK          "Use GLPK simplex solver")
+cvc4_option(USE_KISSAT        "Use Kissat SAT solver")
 cvc4_option(USE_READLINE      "Use readline for better interactive support")
 # >> 2-valued: ON OFF
 #    > for options where we don't need to detect if set by user (default: OFF)
@@ -167,6 +171,7 @@ set(CXXTEST_DIR       "" CACHE STRING "Set CxxTest install directory")
 set(DRAT2ER_DIR       "" CACHE STRING "Set drat2er install directory")
 set(GLPK_DIR          "" CACHE STRING "Set GLPK install directory")
 set(GMP_DIR           "" CACHE STRING "Set GMP install directory")
+set(KISSAT_DIR        "" CACHE STRING "Set Kissat install directory")
 set(LFSC_DIR          "" CACHE STRING "Set LFSC install directory")
 set(SYMFPU_DIR        "" CACHE STRING "Set SymFPU install directory")
 
@@ -483,6 +488,11 @@ if(USE_GLPK)
   add_definitions(-DCVC4_USE_GLPK)
 endif()
 
+if(USE_KISSAT)
+  find_package(Kissat REQUIRED)
+  add_definitions(-DCVC4_USE_KISSAT)
+endif()
+
 if(USE_LFSC)
   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --with-lfsc)
   find_package(LFSC REQUIRED)
@@ -587,9 +597,9 @@ string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}")
 message("CVC4 ${CVC4_RELEASE_STRING}")
 message("")
 if(ENABLE_COMP_INC_TRACK)
-  message("Build profile        : ${CVC4_BUILD_PROFILE_STRING} (incremental)")
+  message("Build profile             : ${CVC4_BUILD_PROFILE_STRING} (incremental)")
 else()
-  message("Build profile        : ${CVC4_BUILD_PROFILE_STRING}")
+  message("Build profile             : ${CVC4_BUILD_PROFILE_STRING}")
 endif()
 message("")
 print_config("GPL                       :" ENABLE_GPL)
@@ -627,55 +637,59 @@ print_config("CaDiCaL                   :" USE_CADICAL)
 print_config("CryptoMiniSat             :" USE_CRYPTOMINISAT)
 print_config("drat2er                   :" USE_DRAT2ER)
 print_config("GLPK                      :" USE_GLPK)
+print_config("Kissat                    :" USE_KISSAT)
 print_config("LFSC                      :" USE_LFSC)
 
 if(CVC4_USE_CLN_IMP)
-  message("MP library                   : cln")
+  message("MP library                : cln")
 else()
-  message("MP library                   : gmp")
+  message("MP library                : gmp")
 endif()
 print_config("Readline                  :" ${USE_READLINE})
 print_config("SymFPU                    :" ${USE_SYMFPU})
 message("")
 if(ABC_DIR)
-  message("ABC dir                      : ${ABC_DIR}")
+  message("ABC dir                   : ${ABC_DIR}")
 endif()
 if(ANTLR_DIR)
-  message("ANTLR dir                    : ${ANTLR_DIR}")
+  message("ANTLR dir                 : ${ANTLR_DIR}")
 endif()
 if(CADICAL_DIR)
-  message("CADICAL dir                  : ${CADICAL_DIR}")
+  message("CADICAL dir               : ${CADICAL_DIR}")
 endif()
 if(CRYPTOMINISAT_DIR)
-  message("CRYPTOMINISAT dir            : ${CRYPTOMINISAT_DIR}")
+  message("CRYPTOMINISAT dir         : ${CRYPTOMINISAT_DIR}")
 endif()
 if(DRAT2ER_DIR)
-  message("DRAT2ER dir                  : ${DRAT2ER_DIR}")
+  message("DRAT2ER dir               : ${DRAT2ER_DIR}")
 endif()
 if(GLPK_DIR)
-  message("GLPK dir                     : ${GLPK_DIR}")
+  message("GLPK dir                  : ${GLPK_DIR}")
 endif()
 if(GMP_DIR)
-  message("GMP dir                      : ${GMP_DIR}")
+  message("GMP dir                   : ${GMP_DIR}")
+endif()
+if(KISSAT_DIR)
+  message("KISSAT dir                : ${KISSAT_DIR}")
 endif()
 if(LFSC_DIR)
-  message("LFSC dir                     : ${LFSC_DIR}")
+  message("LFSC dir                  : ${LFSC_DIR}")
 endif()
 if(SYMFPU_DIR)
-  message("SYMFPU dir                   : ${SYMFPU_DIR}")
+  message("SYMFPU dir                : ${SYMFPU_DIR}")
 endif()
 message("")
-message("CPPLAGS (-D...)                : ${CVC4_DEFINITIONS}")
-message("CXXFLAGS                       : ${CMAKE_CXX_FLAGS}")
-message("CFLAGS                         : ${CMAKE_C_FLAGS}")
-message("Linker flags                   : ${CMAKE_EXE_LINKER_FLAGS}")
+message("CPPLAGS (-D...)           : ${CVC4_DEFINITIONS}")
+message("CXXFLAGS                  : ${CMAKE_CXX_FLAGS}")
+message("CFLAGS                    : ${CMAKE_C_FLAGS}")
+message("Linker flags              : ${CMAKE_EXE_LINKER_FLAGS}")
 message("")
-message("Install prefix                 : ${CMAKE_INSTALL_PREFIX}")
+message("Install prefix            : ${CMAKE_INSTALL_PREFIX}")
 message("")
 
 if(GPL_LIBS)
   message(
-  "CVC4 license                         : GPLv3 (due to optional libraries; see below)"
+  "CVC4 license             : GPLv3 (due to optional libraries; see below)"
   "\n"
   "\n"
   "Please note that CVC4 will be built against the following GPLed libraries:"
@@ -692,7 +706,7 @@ if(GPL_LIBS)
   )
 else()
   message(
-  "CVC4 license                         : modified BSD"
+  "CVC4 license              : modified BSD"
   "\n"
   "\n"
   "Note that this configuration is NOT built against any GPL'ed libraries, so"
diff --git a/cmake/FindKissat.cmake b/cmake/FindKissat.cmake
new file mode 100644
index 000000000..cc5311ad4
--- /dev/null
+++ b/cmake/FindKissat.cmake
@@ -0,0 +1,17 @@
+# Find Kissat
+# Kissat_FOUND - found Kissat lib
+# Kissat_INCLUDE_DIR - the Kissat include directory
+# Kissat_LIBRARIES - Libraries needed to use Kissat
+
+find_path(Kissat_INCLUDE_DIR NAMES kissat/kissat.h)
+find_library(Kissat_LIBRARIES NAMES kissat)
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(Kissat
+  DEFAULT_MSG Kissat_INCLUDE_DIR Kissat_LIBRARIES)
+
+mark_as_advanced(Kissat_INCLUDE_DIR Kissat_LIBRARIES)
+if(Kissat_LIBRARIES)
+  message(STATUS "Found Kissat library: ${Kissat_LIBRARIES}")
+endif()
+
diff --git a/configure.sh b/configure.sh
index 070e2c230..21a444082 100755
--- a/configure.sh
+++ b/configure.sh
@@ -63,6 +63,7 @@ The following flags enable optional packages (disable with --no-<option name>).
   --cadical                use the CaDiCaL SAT solver
   --cryptominisat          use the CryptoMiniSat SAT solver
   --drat2er                use drat2er (required for eager BV proofs)
+  --kissat                 use the Kissat SAT solver
   --lfsc                   use the LFSC proof checker
   --symfpu                 use SymFPU for floating point solver
   --readline               support the readline library
@@ -76,6 +77,7 @@ Optional Path to Optional Packages:
   --cxxtest-dir=PATH       path to CxxTest installation
   --glpk-dir=PATH          path to top level of GLPK installation
   --gmp-dir=PATH           path to top level of GMP installation
+  --kissat-dir=PATH        path to top level of Kissat source tree
   --lfsc-dir=PATH          path to top level of LFSC source tree
   --symfpu-dir=PATH        path to top level of SymFPU source tree
 
@@ -110,8 +112,6 @@ buildtype=default
 
 abc=default
 asan=default
-ubsan=default
-tsan=default
 assertions=default
 best=default
 cadical=default
@@ -119,30 +119,33 @@ cln=default
 comp_inc=default
 coverage=default
 cryptominisat=default
-debug_symbols=default
 debug_context_mm=default
+debug_symbols=default
 drat2er=default
 dumping=default
-gpl=default
-win64=default
-ninja=default
 glpk=default
+gpl=default
+kissat=default
 lfsc=default
 muzzle=default
+ninja=default
 optimized=default
+profiling=default
 proofs=default
+python2=default
+python3=default
+python_bindings=default
+readline=default
 shared=default
 static_binary=default
 statistics=default
 symfpu=default
 tracing=default
+tsan=default
+ubsan=default
 unit_testing=default
-python2=default
-python3=default
-python_bindings=default
 valgrind=default
-profiling=default
-readline=default
+win64=default
 
 language_bindings_java=default
 language_bindings_python=default
@@ -155,6 +158,7 @@ drat2er_dir=default
 cxxtest_dir=default
 glpk_dir=default
 gmp_dir=default
+kissat_dir=default
 lfsc_dir=default
 symfpu_dir=default
 
@@ -228,6 +232,9 @@ do
     --gpl) gpl=ON;;
     --no-gpl) gpl=OFF;;
 
+    --kissat) kissat=ON;;
+    --no-kissat) kissat=OFF;;
+
     --win64) win64=ON;;
     --no-win64) win64=OFF;;
 
@@ -325,6 +332,9 @@ do
     --gmp-dir) die "missing argument to $1 (try -h)" ;;
     --gmp-dir=*) gmp_dir=${1##*=} ;;
 
+    --kissat-dir) die "missing argument to $1 (try -h)" ;;
+    --kissat-dir=*) kissat_dir=${1##*=} ;;
+
     --lfsc-dir) die "missing argument to $1 (try -h)" ;;
     --lfsc-dir=*) lfsc_dir=${1##*=} ;;
 
@@ -418,6 +428,8 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DUSE_DRAT2ER=$drat2er"
 [ $glpk != default ] \
   && cmake_opts="$cmake_opts -DUSE_GLPK=$glpk"
+[ $kissat != default ] \
+  && cmake_opts="$cmake_opts -DUSE_KISSAT=$kissat"
 [ $lfsc != default ] \
   && cmake_opts="$cmake_opts -DUSE_LFSC=$lfsc"
 [ $symfpu != default ] \
@@ -444,6 +456,8 @@ cmake_opts=""
   && cmake_opts="$cmake_opts -DGLPK_DIR=$glpk_dir"
 [ "$gmp_dir" != default ] \
   && cmake_opts="$cmake_opts -DGMP_DIR=$gmp_dir"
+[ "$kissat_dir" != default ] \
+  && cmake_opts="$cmake_opts -DKISSAT=$kissat_dir"
 [ "$lfsc_dir" != default ] \
   && cmake_opts="$cmake_opts -DLFSC_DIR=$lfsc_dir"
 [ "$symfpu_dir" != default ] \
diff --git a/contrib/get-kissat b/contrib/get-kissat
new file mode 100755
index 000000000..7b513caef
--- /dev/null
+++ b/contrib/get-kissat
@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+
+set -e -o pipefail
+
+source "$(dirname "$0")/get-script-header.sh"
+
+KISSAT_DIR="${DEPS_DIR}/kissat"
+version="sc2020-039805f2"
+
+check_dep_dir "${KISSAT_DIR}"
+
+# Download and build Kissat
+setup_dep \
+  "http://fmv.jku.at/kissat/kissat-$version.tar.xz" "$KISSAT_DIR"
+cd "${KISSAT_DIR}"
+
+./configure -fPIC --quiet
+make -j${NPROC}
+install_lib build/libkissat.a
+install_includes src/kissat.h kissat
+
+echo
+echo "Using Kissat version $version"
+echo
+echo ===================== Now configure CVC4 with =====================
+echo ./configure.sh --kissat
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 66a1fee16..ff11897e9 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -190,6 +190,8 @@ libcvc4_add_sources(
   prop/cnf_stream.h
   prop/cryptominisat.cpp
   prop/cryptominisat.h
+  prop/kissat.cpp
+  prop/kissat.h
   prop/minisat/core/Dimacs.h
   prop/minisat/core/Solver.cc
   prop/minisat/core/Solver.h
@@ -841,6 +843,10 @@ if(USE_CRYPTOMINISAT)
   target_link_libraries(cvc4 ${CryptoMiniSat_LIBRARIES})
   target_include_directories(cvc4 PRIVATE ${CryptoMiniSat_INCLUDE_DIR})
 endif()
+if(USE_KISSAT)
+  target_link_libraries(cvc4 ${Kissat_LIBRARIES})
+  target_include_directories(cvc4 PRIVATE ${Kissat_INCLUDE_DIR})
+endif()
 if(USE_DRAT2ER)
   target_link_libraries(cvc4 ${Drat2Er_LIBRARIES})
   target_include_directories(cvc4 PRIVATE ${Drat2Er_INCLUDE_DIR})
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index a1fd01c96..5df579b86 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -138,6 +138,7 @@ std::string Configuration::copyright() {
   if (Configuration::isBuiltWithAbc() || Configuration::isBuiltWithLfsc()
       || Configuration::isBuiltWithCadical()
       || Configuration::isBuiltWithCryptominisat()
+      || Configuration::isBuiltWithKissat()
       || Configuration::isBuiltWithSymFPU())
   {
     ss << "This version of CVC4 is linked against the following non-(L)GPL'ed\n"
@@ -164,6 +165,12 @@ std::string Configuration::copyright() {
          << "  See https://github.com/msoos/cryptominisat for copyright "
          << "information.\n\n";
     }
+    if (Configuration::isBuiltWithKissat())
+    {
+      ss << "  Kissat - Simplified Satisfiability Solver\n"
+         << "  See https://fmv.jku.at/kissat for copyright "
+         << "information.\n\n";
+    }
     if (Configuration::isBuiltWithSymFPU())
     {
       ss << "  SymFPU - The Symbolic Floating Point Unit\n"
@@ -250,6 +257,8 @@ bool Configuration::isBuiltWithCryptominisat() {
   return IS_CRYPTOMINISAT_BUILD;
 }
 
+bool Configuration::isBuiltWithKissat() { return IS_KISSAT_BUILD; }
+
 bool Configuration::isBuiltWithDrat2Er() { return IS_DRAT2ER_BUILD; }
 
 bool Configuration::isBuiltWithReadline() {
diff --git a/src/base/configuration.h b/src/base/configuration.h
index 72ccb2301..7de4a337b 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -99,6 +99,8 @@ public:
 
   static bool isBuiltWithCryptominisat();
 
+  static bool isBuiltWithKissat();
+
   static bool isBuiltWithDrat2Er();
 
   static bool isBuiltWithReadline();
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 77db0b51c..e77752420 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -126,6 +126,12 @@ namespace CVC4 {
 #  define IS_DRAT2ER_BUILD false
 #endif /* CVC4_USE_DRAT2ER */
 
+#if CVC4_USE_KISSAT
+#define IS_KISSAT_BUILD true
+#else /* CVC4_USE_KISSAT */
+#define IS_KISSAT_BUILD false
+#endif /* CVC4_USE_KISSAT */
+
 #if CVC4_USE_LFSC
 #define IS_LFSC_BUILD true
 #else /* CVC4_USE_LFSC */
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 05dc6b716..5c8cd8f58 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -56,6 +56,8 @@ header = "options/bv_options.h"
   name = "cryptominisat"
 [[option.mode.CADICAL]]
   name = "cadical"
+[[option.mode.KISSAT]]
+  name = "kissat"
 
 [[option]]
   name       = "bitblastMode"
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 9253ea1c8..af811e085 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -51,6 +51,10 @@ void throwLazyBBUnsupported(options::SatSolverMode m)
   {
     sat_solver = "CaDiCaL";
   }
+  else if (m == options::SatSolverMode::KISSAT)
+  {
+    sat_solver = "Kissat";
+  }
   else
   {
     Assert(m == options::SatSolverMode::CRYPTOMINISAT);
@@ -166,7 +170,17 @@ void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
     throw OptionException(ss.str());
   }
 
-  if (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL)
+  if (m == SatSolverMode::KISSAT && !Configuration::isBuiltWithKissat())
+  {
+    std::stringstream ss;
+    ss << "option `" << option
+       << "' requires a Kissat build of CVC4; this binary was not built with "
+          "Kissat support";
+    throw OptionException(ss.str());
+  }
+
+  if (m == SatSolverMode::CRYPTOMINISAT || m == SatSolverMode::CADICAL
+      || m == SatSolverMode::KISSAT)
   {
     if (options::bitblastMode() == options::BitblastMode::LAZY
         && options::bitblastMode.wasSetByUser())
@@ -443,6 +457,7 @@ void OptionsHandler::showConfiguration(std::string option) {
   print_config_cond("cryptominisat", Configuration::isBuiltWithCryptominisat());
   print_config_cond("drat2er", Configuration::isBuiltWithDrat2Er());
   print_config_cond("gmp", Configuration::isBuiltWithGmp());
+  print_config_cond("kissat", Configuration::isBuiltWithKissat());
   print_config_cond("lfsc", Configuration::isBuiltWithLfsc());
   print_config_cond("readline", Configuration::isBuiltWithReadline());
   print_config_cond("symfpu", Configuration::isBuiltWithSymFPU());
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 396b2c8ea..283558709 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -140,10 +140,11 @@ public:
 template<class T>
 void OptionsHandler::checkSatSolverEnabled(std::string option, T m)
 {
-#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL)
+#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL) \
+    && !defined(CVC4_USE_KISSAT)
   std::stringstream ss;
   ss << "option `" << option
-     << "' requires CVC4 to be built with CryptoMiniSat or CaDiCaL";
+     << "' requires CVC4 to be built with CryptoMiniSat or CaDiCaL or Kissat";
   throw OptionException(ss.str());
 #endif
 }
diff --git a/src/prop/kissat.cpp b/src/prop/kissat.cpp
new file mode 100644
index 000000000..0440fcd4e
--- /dev/null
+++ b/src/prop/kissat.cpp
@@ -0,0 +1,179 @@
+/*********************                                                        */
+/*! \file kissat.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Wrapper for Kissat SAT Solver.
+ **
+ ** Wrapper for the Kissat SAT solver (for theory of bit-vectors).
+ **/
+
+#include "prop/kissat.h"
+
+#ifdef CVC4_USE_KISSAT
+
+#include "base/check.h"
+#include "proof/sat_proof.h"
+
+namespace CVC4 {
+namespace prop {
+
+using KissatLit = int32_t;
+using KissatVar = int32_t;
+
+// helper functions
+namespace {
+
+SatValue toSatValue(int32_t result)
+{
+  if (result == 10) return SAT_VALUE_TRUE;
+  if (result == 20) return SAT_VALUE_FALSE;
+  Assert(result == 0);
+  return SAT_VALUE_UNKNOWN;
+}
+
+/**
+ * Helper to convert the value of a literal as returned by Kissat to the
+ * corresponding true/false SAT_VALUE.
+ * Note: Kissat returns lit/-lit for true/false. Older versions returned 1/-1.
+ */
+SatValue toSatValueLit(int value)
+{
+  if (value > 0) return SAT_VALUE_TRUE;
+  Assert(value < 0);
+  return SAT_VALUE_FALSE;
+}
+
+/** Helper to convert SatLiteral to KissatLit. */
+KissatLit toKissatLit(const SatLiteral lit)
+{
+  return lit.isNegated() ? -lit.getSatVariable() : lit.getSatVariable();
+}
+
+/** Helper to convert a SatVariable to a KissatVar. */
+KissatVar toKissatVar(SatVariable var) { return var; }
+
+}  // namespace
+
+KissatSolver::KissatSolver(StatisticsRegistry* registry,
+                           const std::string& name)
+    : d_solver(kissat_init()),
+      // Note: Kissat variables start with index 1 rather than 0 since negated
+      //       literals are represented as the negation of the index.
+      d_nextVarIdx(1),
+      d_statistics(registry, name)
+{
+}
+
+void KissatSolver::init()
+{
+  d_true = newVar();
+  d_false = newVar();
+  kissat_add(d_solver, toKissatVar(d_true));
+  kissat_add(d_solver, 0);
+  kissat_add(d_solver, -toKissatVar(d_false));
+  kissat_add(d_solver, 0);
+}
+
+KissatSolver::~KissatSolver() { kissat_release(d_solver); }
+
+ClauseId KissatSolver::addClause(SatClause& clause, bool removable)
+{
+  for (const SatLiteral& lit : clause)
+  {
+    kissat_add(d_solver, toKissatLit(lit));
+  }
+  kissat_add(d_solver, 0);
+  ++d_statistics.d_numClauses;
+  return ClauseIdError;
+}
+
+ClauseId KissatSolver::addXorClause(SatClause& clause, bool rhs, bool removable)
+{
+  Unreachable() << "Kissat does not support adding XOR clauses.";
+}
+
+SatVariable KissatSolver::newVar(bool isTheoryAtom,
+                                 bool preRegister,
+                                 bool canErase)
+{
+  ++d_statistics.d_numVariables;
+  return d_nextVarIdx++;
+}
+
+SatVariable KissatSolver::trueVar() { return d_true; }
+
+SatVariable KissatSolver::falseVar() { return d_false; }
+
+SatValue KissatSolver::solve()
+{
+  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTime);
+  SatValue res = toSatValue(kissat_solve(d_solver));
+  d_okay = (res == SAT_VALUE_TRUE);
+  ++d_statistics.d_numSatCalls;
+  return res;
+}
+
+SatValue KissatSolver::solve(long unsigned int&)
+{
+  Unimplemented() << "Setting limits for Kissat not supported yet";
+};
+
+SatValue KissatSolver::solve(const std::vector<SatLiteral>& assumptions)
+{
+  Unimplemented() << "Incremental solving with Kissat not supported yet";
+}
+
+void KissatSolver::interrupt() { kissat_terminate(d_solver); }
+
+SatValue KissatSolver::value(SatLiteral l)
+{
+  Assert(d_okay);
+  return toSatValueLit(kissat_value(d_solver, toKissatLit(l)));
+}
+
+SatValue KissatSolver::modelValue(SatLiteral l)
+{
+  Assert(d_okay);
+  return value(l);
+}
+
+unsigned KissatSolver::getAssertionLevel() const
+{
+  Unreachable() << "Kissat does not support assertion levels.";
+}
+
+bool KissatSolver::ok() const { return d_okay; }
+
+KissatSolver::Statistics::Statistics(StatisticsRegistry* registry,
+                                     const std::string& prefix)
+    : d_registry(registry),
+      d_numSatCalls("theory::bv::" + prefix + "::Kissat::calls_to_solve", 0),
+      d_numVariables("theory::bv::" + prefix + "::Kissat::variables", 0),
+      d_numClauses("theory::bv::" + prefix + "::Kissat::clauses", 0),
+      d_solveTime("theory::bv::" + prefix + "::Kissat::solve_time")
+{
+  d_registry->registerStat(&d_numSatCalls);
+  d_registry->registerStat(&d_numVariables);
+  d_registry->registerStat(&d_numClauses);
+  d_registry->registerStat(&d_solveTime);
+}
+
+KissatSolver::Statistics::~Statistics()
+{
+  d_registry->unregisterStat(&d_numSatCalls);
+  d_registry->unregisterStat(&d_numVariables);
+  d_registry->unregisterStat(&d_numClauses);
+  d_registry->unregisterStat(&d_solveTime);
+}
+
+}  // namespace prop
+}  // namespace CVC4
+
+#endif  // CVC4_USE_KISSAT
diff --git a/src/prop/kissat.h b/src/prop/kissat.h
new file mode 100644
index 000000000..35b33daeb
--- /dev/null
+++ b/src/prop/kissat.h
@@ -0,0 +1,102 @@
+/*********************                                                        */
+/*! \file kissat.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Wrapper for Kissat SAT Solver.
+ **
+ ** Wrapper for the Kissat SAT solver (for theory of bit-vectors).
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__PROP__KISSAT_H
+#define CVC4__PROP__KISSAT_H
+
+#ifdef CVC4_USE_KISSAT
+
+#include "prop/sat_solver.h"
+
+extern "C" {
+#include <kissat/kissat.h>
+}
+
+namespace CVC4 {
+namespace prop {
+
+class KissatSolver : public SatSolver
+{
+  friend class SatSolverFactory;
+
+ public:
+  ~KissatSolver() override;
+
+  ClauseId addClause(SatClause& clause, bool removable) override;
+
+  ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override;
+
+  SatVariable newVar(bool isTheoryAtom = false,
+                     bool preRegister = false,
+                     bool canErase = true) override;
+
+  SatVariable trueVar() override;
+  SatVariable falseVar() override;
+
+  SatValue solve() override;
+  SatValue solve(long unsigned int&) override;
+  SatValue solve(const std::vector<SatLiteral>& assumptions) override;
+
+  void interrupt() override;
+
+  SatValue value(SatLiteral l) override;
+
+  SatValue modelValue(SatLiteral l) override;
+
+  unsigned getAssertionLevel() const override;
+
+  bool ok() const override;
+
+ private:
+  struct Statistics
+  {
+    StatisticsRegistry* d_registry;
+    IntStat d_numSatCalls;
+    IntStat d_numVariables;
+    IntStat d_numClauses;
+    TimerStat d_solveTime;
+    Statistics(StatisticsRegistry* registry, const std::string& prefix);
+    ~Statistics();
+  };
+
+  /**
+   * Private to disallow creation outside of SatSolverFactory.
+   * Function init() must be called after creation.
+   */
+  KissatSolver(StatisticsRegistry* registry, const std::string& name = "");
+  /**
+   * Initialize SAT solver instance.
+   * Note: Split out to not call virtual functions in constructor.
+   */
+  void init();
+
+  kissat* d_solver;
+
+  unsigned d_nextVarIdx;
+  bool d_okay;
+  SatVariable d_true;
+  SatVariable d_false;
+
+  Statistics d_statistics;
+};
+
+}  // namespace prop
+}  // namespace CVC4
+
+#endif  // CVC4_USE_KISSAT
+#endif  // CVC4__PROP__KISSAT_H
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 460ab3ece..8f18a6055 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -19,6 +19,7 @@
 #include "prop/bvminisat/bvminisat.h"
 #include "prop/cadical.h"
 #include "prop/cryptominisat.h"
+#include "prop/kissat.h"
 #include "prop/minisat/minisat.h"
 
 namespace CVC4 {
@@ -58,5 +59,17 @@ SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry,
 #endif
 }
 
+SatSolver* SatSolverFactory::createKissat(StatisticsRegistry* registry,
+                                          const std::string& name)
+{
+#ifdef CVC4_USE_KISSAT
+  KissatSolver* res = new KissatSolver(registry, name);
+  res->init();
+  return res;
+#else
+  Unreachable() << "CVC4 was not compiled with Kissat support.";
+#endif
+}
+
 }  // namespace prop
 }  // namespace CVC4
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index 5f8649768..04b5d73a6 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -45,6 +45,8 @@ class SatSolverFactory
   static SatSolver* createCadical(StatisticsRegistry* registry,
                                   const std::string& name = "");
 
+  static SatSolver* createKissat(StatisticsRegistry* registry,
+                                 const std::string& name = "");
 }; /* class SatSolverFactory */
 
 }  // namespace prop
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index ea9867b0f..295090699 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -164,6 +164,10 @@ AigBitblaster::AigBitblaster()
       solver = prop::SatSolverFactory::createCryptoMinisat(
           smtStatisticsRegistry(), "AigBitblaster");
       break;
+    case options::SatSolverMode::KISSAT:
+      solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(),
+                                                    "AigBitblaster");
+      break;
     default: CVC4_FATAL() << "Unknown SAT solver type";
   }
   d_satSolver.reset(solver);
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index bddde4cb7..0ba69c8b8 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -60,6 +60,10 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
       solver = prop::SatSolverFactory::createCryptoMinisat(
           smtStatisticsRegistry(), "EagerBitblaster");
       break;
+    case options::SatSolverMode::KISSAT:
+      solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(),
+                                                    "EagerBitblaster");
+      break;
     default: Unreachable() << "Unknown SAT solver type";
   }
   d_satSolver.reset(solver);