Skip to content

Instantly share code, notes, and snippets.

@scturtle scturtle/SATurtle.cc
Last active Aug 9, 2018

Embed
What would you like to do?
naive SAT solver using DPLL algorithm
#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;
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.