always-cautious/ortools-clone
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

more tests on minisat

Browse Source
This commit is contained in:
lperron@google.com
2012-07-13 16:30:18 +00:00
parent b6fa538a13
commit e202cfe4fd
2 changed files with 24 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

24
examples/tests/boolean_test.cc
View File

@@ -105,7 +105,28 @@ void TestBoolEq() {
solver.AddConstraint(reinterpret_cast<Constraint*>(sat));
IntVar* const x = solver.MakeBoolVar("x");
IntVar* const y = solver.MakeBoolVar("y");
CHECK(AddBoolEq(sat, x, solver.MakeDifference(1, y)));
CHECK(AddBoolEq(sat, x, y));
DecisionBuilder* const db =
solver.MakePhase(x, y,
Solver::CHOOSE_FIRST_UNBOUND,
Solver::ASSIGN_MIN_VALUE);
solver.NewSearch(db);
while (solver.NextSolution()) {
LOG(INFO) << " x = " << x->Value() << ", y = " << y->Value();
}
solver.EndSearch();
CHECK_EQ(2, solver.solutions());
LOG(INFO) << solver.DebugString();
}
void TestBoolNot() {
LOG(INFO) << "TestBoolNot";
Solver solver("TestBoolNot");
SatPropagator* const sat = MakeSatPropagator(&solver);
solver.AddConstraint(reinterpret_cast<Constraint*>(sat));
IntVar* const x = solver.MakeBoolVar("x");
IntVar* const y = solver.MakeBoolVar("y");
CHECK(AddBoolNot(sat, x, y));
DecisionBuilder* const db =
solver.MakePhase(x, y,
Solver::CHOOSE_FIRST_UNBOUND,
@@ -240,6 +261,7 @@ int main(int argc, char** argv) {
operations_research::TestConversions();
operations_research::TestBoolLe();
operations_research::TestBoolEq();
operations_research::TestBoolNot();
operations_research::TestBoolAndEq();
operations_research::TestBoolOrEq();
operations_research::TestBoolIsEq();

2
src/constraint_solver/booleans.cc
View File

@@ -82,7 +82,7 @@ class SatPropagator : public Constraint {
}
void VariableBound(int index) {
if (num_bound_literals_.Value() <= minisat_.decisionLevel()) {
if (num_bound_literals_.Value() < minisat_.decisionLevel()) {
minisat_.cancelUntil(num_bound_literals_.Value());
}
VLOG(1) << "VariableBound: " << vars_[index]->DebugString();