CDCL SAT Solver for programming contest.
Togasat is CDCL SAT Solver by modifying minisat.
##Install
g++ -std=c++11 -o Solver -O3 Solver.cpp
##How to If you want to add a (x1 v x2 v not x3) clause,
togast::Solver solver;
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)
solver.assigns[0] = 0;//X1 = True
solver.assigns[1] = 1;//X2 = False
solver.assigns[i] = 0;//X_{i + 1} = True
####How to solve cnf
./Solver <cnf problem>
int main(int argc, char *argv[]) {
togasat::Solver solver;
std::string problem_name = argv[1];
solver.parse_dimacs_problem(problem_name);//parse problem
togasat::lbool status = solver.solve();//solve sat problem
solver.print_answer();//print answer
}
status is 0,SATISFIABLE
status is 1,UNSATSFIABLE
status is 2,UNKNOWN
#####SATISFIABLE
If Sat Solver prove a given problem is SATISFIABLE(SAT),print SAT and model for problem.
SAT -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 13 -14 15 16 0
The model is seperated by 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
.
#####UNSATISFIABLE
only print UNSAT.
UNSAT
##Tutorial for 8-queen problem Coming soon!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
##Algorithm
- DPLL
- Clause learning
- Two literal watching
- Back jump
- Phase saving
- Luby restart
- VSIDS