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} = True

You 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

• Codeforces Round #383 (Div. 2) E

• mugenen
• kmyk
• koba-e964

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