13 #include <zchaff_solver.h>
19 solver->set_variable_number(0);
39 "variable number shall be within bounds");
66 for(clausest::const_iterator it=
clauses.begin();
70 reinterpret_cast<int*>(&((*it)[0])), it->size());
95 msg=
"SAT checker: instance is UNSATISFIABLE";
99 msg=
"SAT checker: instance is SATISFIABLE";
103 msg=
"SAT checker failed: UNDETERMINED";
107 msg=
"SAT checker failed: Time out";
111 msg=
"SAT checker failed: Out of memory";
115 msg=
"SAT checker failed: ABORTED";
119 msg=
"SAT checker failed: unknown result";
129 for(
unsigned i=1; i<
solver->variables().size(); i++)
131 solver->variables()[i].value() == 0 ||
132 solver->variables()[i].value() == 1,
133 "all variables shall have been assigned");
140 cout <<
"DEBUG L" << i <<
":" << get(i) <<
'\n';
147 return P_UNSATISFIABLE;
153 return P_SATISFIABLE;
166 solver->variables()[v].set_value(value);