togasat based on minisat is a header-only CDCL SAT Solver for programming contests.
- C++11
At first, include the header (or do copy & paste):
#include "togasat.hpp"Make a solver object.
togasat::Solver solver;If you want to add a (x1 v x2 v not x3) clause
std::vector<int> clause;
clause.push_back(1); // x1
clause.push_back(2); // x2
clause.push_back(-3); // not x3
solver.addClause(clause); // add (x1 v x2 v not x3)YOU MUST NOT ADD CLAUSES THAT CONTAIN 0, IT WILL CAUSE A SAT SOLVER ABORTION
After adding all clauses, call .solve() method.
togasat::lbool status = solver.solve();The return value:
- status is 0,
SATISFIABLE - status is 1,
UNSATSFIABLE - status is 2,
UNKNOWN
Also, you can get the assignments, e.g.
solver.assigns[0] = 0; // X_1 = True
solver.assigns[1] = 1; // X_2 = False
solver.assigns[i] = 0; // X_{i + 1} = TrueYou should take care that 0 denotes true and 1 denotes false.
$ ./togasat <cnf problem>
int main(int argc, char *argv[]) {
togasat::Solver solver;
std::string problem_name = argv[1];
solver.parseDimacsProblem(problem_name); // parse problem
togasat::lbool status = solver.solve(); // solve sat problem
solver.printAnswer(); // print answer
}If Sat Solver proves a given problem is SATISFIABLE(SAT), it prints SAT and a model for the problem.
SAT
-1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 13 -14 15 16 0
The model is separated by a space and ended with zero(0).
- A positive integer represents
True. - A negative integer represents
False.
For example,-1 represents X1=False,13 represents X13=True.
It only prints UNSAT.
UNSAT
- DPLL
- Clause learning
- Two literal watching
- Back jump
- Phase saving
- Luby restart
- VSIDS
Welcome any pull requests, fix of typo, refactoring, correction of documents and so on. If you can solve a competitive programming problem by togasat, please let me know and you make a pull request. It's very helpful for me.
Your star makes me motivated