From 4ead56c9c9e89f642b0e251af82adae30ba7a46b Mon Sep 17 00:00:00 2001
From: valentin_lechner <valentin_lechner@dismail.de>
Date: Fri, 16 Jun 2023 18:29:57 +0200
Subject: [PATCH] Aufnahme SatHelper implementation

---
 .gitignore     |   1 +
 CMakeLists.txt |   6 ++
 sathelper.cpp  |   1 +
 sathelper.h    | 153 +++++++++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 161 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 CMakeLists.txt
 create mode 100644 sathelper.cpp
 create mode 100644 sathelper.h

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..ff9047e
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/cmake-build-debug/
diff --git a/CMakeLists.txt b/CMakeLists.txt
new file mode 100644
index 0000000..6786c1e
--- /dev/null
+++ b/CMakeLists.txt
@@ -0,0 +1,6 @@
+cmake_minimum_required(VERSION 3.24)
+project(sathelper)
+
+set(CMAKE_CXX_STANDARD 17)
+
+add_library(sathelper sathelper.cpp)
diff --git a/sathelper.cpp b/sathelper.cpp
new file mode 100644
index 0000000..a9b280d
--- /dev/null
+++ b/sathelper.cpp
@@ -0,0 +1 @@
+#include "sathelper.h"
\ No newline at end of file
diff --git a/sathelper.h b/sathelper.h
new file mode 100644
index 0000000..3a53b72
--- /dev/null
+++ b/sathelper.h
@@ -0,0 +1,153 @@
+#ifndef SATHELPER_SATHELPER_H
+#define SATHELPER_SATHELPER_H
+#endif // SATHELPER_SATHELPER_H
+#include <unordered_map>
+
+#include <algorithm>
+#include <fstream>
+#include <iostream>
+#include <sstream>
+#include <vector>
+
+class SatHelper {
+private:
+  int nextIntId = 1;
+  std::unordered_map<std::string, int> varIntMap;
+  std::unordered_map<int, std::string> intVarMap;
+  std::vector<std::vector<int>> clauses;
+  int varToInt(const std::string &name) { return varIntMap[name]; };
+  std::string intToVar(const int var) {
+    if (var == 0)
+      return "0";
+    if (var > 0) {
+      return intVarMap[var];
+    }
+    return "-" + intVarMap[-var];
+  }
+  static std::string getVarName(const std::string &lit) {
+    if (isNegated(lit)) {
+      return lit.substr(1);
+    }
+    return lit;
+  }
+  static bool isNegated(const std::string &lit) { return lit[0] == '-'; }
+  int literalToInt(const std::string &lit) {
+    int code = varToInt(getVarName(lit));
+    if (isNegated(lit)) {
+      return -code;
+    }
+    return code;
+  }
+  std::vector<int> literalsToIntStr(const std::vector<std::string> &clause) {
+    std::vector<int> res(clause.size() + 1, 0);
+    std::for_each(clause.begin(), clause.end(),
+                  [idx = 0, &res, this](const auto &elem) mutable {
+                    res[idx] = literalToInt(elem);
+                    ++idx;
+                  });
+    return res;
+  }
+  static std::string getNegated(const std::string &lit) {
+    if (isNegated(lit)) {
+      return getVarName(lit);
+    }
+    return "-" + lit;
+  }
+
+  static std::string clauseToStr(const std::vector<int> &clause) {
+    std::string res;
+    for (const auto &lit : clause) {
+      res += std::to_string(lit);
+      if (lit == 0) {
+        continue;
+      }
+      res += " ";
+    }
+    return res;
+  }
+
+  std::string formulaToStr() {
+    std::string res = "p cnf " + std::to_string(nextIntId - 1) + " " +
+                      std::to_string((int)clauses.size()) + "\n";
+    std::for_each(clauses.begin(), clauses.end(), [&res](const auto &clause) {
+      res += clauseToStr(clause) + "\n";
+    });
+    return res;
+  }
+  const std::string FORMULA_FNAME = "/tmp/formula.cnf";
+
+public:
+  /*
+   * you need to declare vars first before use to create a mapping from name to
+   * int (dimacs doesn't use names)
+   */
+  void declareVar(const std::string &name) {
+    this->varIntMap[name] = this->nextIntId;
+    this->intVarMap[this->nextIntId] = name;
+    this->nextIntId += 1;
+  }
+  /*
+   * add a cnf clause
+   */
+  void addClause(const std::vector<std::string> &clause) {
+    this->clauses.push_back(literalsToIntStr(clause));
+  }
+  /*
+   * add a clause with at-most-one constraint
+   */
+  void addAtMostOne(const std::vector<std::string> &clause) {
+    std::for_each(clause.begin(), clause.end(),
+                  [idx = 0, &clause, this](const auto &lit) mutable {
+                    for (int j = idx; j < clause.size(); ++j) {
+                      std::vector<std::string> tmp = {getNegated(lit),
+                                                      getNegated(clause[j])};
+                      this->addClause(tmp);
+                    }
+                    ++idx;
+                  });
+  }
+  void printFormula() { std::cout << formulaToStr() << std::endl; }
+  bool solveSat() {
+    const std::string formula = formulaToStr();
+    std::ofstream fout(FORMULA_FNAME);
+    fout << formula << std::endl;
+    FILE *fp = popen(("glucose -model " + FORMULA_FNAME).c_str(), "r");
+    std::ostringstream out;
+    while (!feof(fp) && !ferror(fp)) {
+      char buf[128];
+      int bytesRead = fread(buf, 1, 128, fp);
+      out.write(buf, bytesRead);
+    }
+    // this can probably be written more elegant
+    std::istringstream stream;
+    stream.str(out.str());
+    std::string line;
+    while (getline(stream, line)) {
+      if (line == "s SATISFIABLE") {
+        getline(stream, line);
+        std::string var;
+        std::vector<std::string> actual_vars;
+        std::istringstream var_line(line.substr(2));
+        while (getline(var_line, var, ' ')) {
+          int varCode = atoi(var.c_str());
+          actual_vars.push_back(intToVar(varCode));
+        };
+        std::cout << "SATISFIABLE WITH VARS ";
+        for (int i = 0; i < actual_vars.size(); ++i) {
+          std::cout << actual_vars[i] << " ";
+        }
+        return true;
+      }
+      if (line == "s UNSATISFIABLE") {
+        return false;
+      }
+    }
+    return false;
+  }
+  void reset() {
+    this->nextIntId = 1;
+    this->clauses = {};
+    this->intVarMap = {};
+    this->varIntMap = {};
+  }
+};