naive SAT solver using DPLL algorithm

SATurtle.cc

#include <fstream>
#include <iostream>
#include <sstream>
#include <string>
#include <vector>

namespace SATurtle {
struct CNF {
  CNF(const std::string &fn);
  int vc = 0;                       // #var
  int lc = 0;                       // #clause
  std::vector<std::vector<int>> cs; // clauses
};

CNF::CNF(const std::string &fn) {
  std::ifstream f(fn);
  if (!f.is_open()) {
    std::cerr << fn << " not exists" << std::endl;
    exit(0);
  }
  int c = 0, v;
  std::string line, dummy;
  while (std::getline(f, line)) {
    if (line[0] == 'c')
      continue;
    else if (line[0] == 'p') {
      std::stringstream s(line);
      if (!(s >> dummy >> dummy >> vc >> lc)) {
        std::cerr << "bad cnf line: " << line << std::endl;
        exit(0);
      }
    } else {
      std::stringstream s(line);
      auto &l = cs.emplace_back();
      l.reserve(vc);
      while ((s >> v) && v != 0)
        l.push_back(v);
      if (l.empty()) {
        cs.pop_back();
        break;
      }
      if (++c == lc)
        break;
    }
  }
}

struct Solver {
  const CNF &cnf;
  std::vector<bool> skip;
  std::vector<int> skip_hist;
  std::vector<int> st_hist;
  std::vector<uint8_t> st; // -1, 0, 1

  Solver(const CNF &cnf) : cnf(cnf), skip(cnf.lc, false), st(cnf.vc + 1, 0) {}

  std::vector<int> solve() { return dpll() ? st_hist : std::vector<int>{0}; }

  bool dpll() {
    if (done())
      return true;
    if (contra())
      return false;
    int lit = choose();
    size_t sts = st_hist.size(), sks = skip_hist.size();
    while (unit_propagate())
      ;
    size_t sts2 = st_hist.size(), sks2 = skip_hist.size();
    set(lit);
    if (dpll())
      return true;
    back(sts2, sks2);
    set(-lit);
    if (dpll())
      return true;
    back(sts, sks);
    return false;
  }

  void back(size_t st_hist_bef, size_t skip_hist_bef) {
    while (skip_hist.size() > skip_hist_bef) {
      skip[skip_hist.back()] = false;
      skip_hist.pop_back();
    }
    while (st_hist.size() > st_hist_bef) {
      st[std::abs(st_hist.back())] = 0;
      st_hist.pop_back();
    }
  }

  void set(int lit) {
    if (st[std::abs(lit)])
      return;
    st[std::abs(lit)] = lit > 0 ? 1 : -1;
    st_hist.push_back(lit);
    simplify(lit);
  }

  int choose() {
    for (int i = 0; i < cnf.lc; ++i) {
      if (skip[i])
        continue;
      for (int lit : cnf.cs[i])
        if (st[std::abs(lit)] == 0)
          return lit;
    }
    __builtin_unreachable();
  }

  bool unit_propagate() {
    bool found = false;
    for (int i = 0; i < cnf.lc; ++i) {
      if (skip[i])
        continue;
      int cnt = 0, lit;
      for (int lit2 : cnf.cs[i])
        if (st[std::abs(lit2)] == 0)
          ++cnt, lit = lit2;
      if (cnt == 1)
        set(lit), found = true;
    }
    return found;
  }

  void simplify(int lit) {
    for (int i = 0; i < cnf.lc; ++i) {
      if (skip[i])
        continue;
      if (std::find(cnf.cs[i].begin(), cnf.cs[i].end(), lit) !=
          cnf.cs[i].end()) {
        skip_hist.push_back(i);
        skip[i] = true;
      }
    }
  }

  bool done() {
    return std::all_of(skip.begin(), skip.end(), [](bool v) { return v; });
  }

  bool contra() {
    for (int i = 0; i < cnf.lc; ++i) {
      if (skip[i])
        continue;
      if (std::all_of(cnf.cs[i].begin(), cnf.cs[i].end(),
                      [&](int l) { return st[std::abs(l)] != 0; }))
        return true;
    }
    return false;
  }
};

} // namespace SATurtle

int main(int argc, char **argv) {
  if (argc < 2) {
    std::cerr << "no input file" << std::endl;
    exit(0);
  }
  SATurtle::CNF cnf(argv[1]);
  SATurtle::Solver solver(cnf);
  for (int lit : solver.solve())
      std::cout << lit << " ";
  std::cout << std::endl;
}