00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 #include "test.h"
00021 #include <algorithm>
00022 #include <clasp/minimize_constraint.h>
00023 #include <clasp/solver.h>
00024 #include <clasp/solve_algorithms.h>
00025 namespace Clasp { namespace Test {
00026 class DefaultMinimizeTest : public CppUnit::TestFixture {
00027 CPPUNIT_TEST_SUITE(DefaultMinimizeTest);
00028 CPPUNIT_TEST(testEmpty);
00029 CPPUNIT_TEST(testOneLevelLits);
00030 CPPUNIT_TEST(testMultiLevelLits);
00031 CPPUNIT_TEST(testMultiLevelWeightsAreReused);
00032 CPPUNIT_TEST(testMergeComplementaryLits);
00033 CPPUNIT_TEST(testMergeComplementaryLits2);
00034 CPPUNIT_TEST(testNegativeLowerInit);
00035 CPPUNIT_TEST(testNegativeLower);
00036
00037 CPPUNIT_TEST(testOrder);
00038 CPPUNIT_TEST(testSkipLevel);
00039 CPPUNIT_TEST(testReassertAfterBacktrack);
00040 CPPUNIT_TEST(testConflict);
00041 CPPUNIT_TEST(testOptimize);
00042 CPPUNIT_TEST(testEnumerate);
00043 CPPUNIT_TEST(testComputeImplicationLevel);
00044 CPPUNIT_TEST(testSetModelMayBacktrackMultiLevels);
00045 CPPUNIT_TEST(testPriorityBug);
00046 CPPUNIT_TEST(testStrengthenImplication);
00047 CPPUNIT_TEST(testRootLevelMadness);
00048 CPPUNIT_TEST(testIntegrateOptimum);
00049 CPPUNIT_TEST(testIntegrateOptimumConflict);
00050 CPPUNIT_TEST(testIntegrateBug);
00051
00052 CPPUNIT_TEST(testReasonBug);
00053 CPPUNIT_TEST(testSmartBacktrack);
00054 CPPUNIT_TEST(testBacktrackToTrue);
00055 CPPUNIT_TEST(testMultiAssignment);
00056 CPPUNIT_TEST(testBugBacktrackFromFalse);
00057 CPPUNIT_TEST(testBugBacktrackToTrue);
00058 CPPUNIT_TEST(testBugInitOptHierarch);
00059 CPPUNIT_TEST(testBugAdjustSum);
00060 CPPUNIT_TEST(testWeightNullBug);
00061 CPPUNIT_TEST(testAdjust);
00062 CPPUNIT_TEST(testAdjustFact);
00063 CPPUNIT_TEST(testAssumption);
00064
00065 CPPUNIT_TEST(testHierarchicalSetModel);
00066 CPPUNIT_TEST(testHierarchical);
00067 CPPUNIT_TEST(testInconsistent);
00068 CPPUNIT_TEST_SUITE_END();
00069 public:
00070 DefaultMinimizeTest() {
00071 a = posLit(ctx.addVar(Var_t::atom_var));
00072 b = posLit(ctx.addVar(Var_t::atom_var));
00073 c = posLit(ctx.addVar(Var_t::atom_var));
00074 d = posLit(ctx.addVar(Var_t::atom_var));
00075 e = posLit(ctx.addVar(Var_t::atom_var));
00076 f = posLit(ctx.addVar(Var_t::atom_var));
00077 x = posLit(ctx.addVar(Var_t::atom_var));
00078 y = posLit(ctx.addVar(Var_t::atom_var));
00079 ctx.startAddConstraints();
00080 }
00081 void setUp() { newMin = 0; data = 0; }
00082 void tearDown() {
00083 if (newMin) { newMin->destroy(ctx.master(), true); }
00084 if (data) { data->release(); }
00085 }
00086 void testEmpty() {
00087 MinimizeBuilder b;
00088 newMin = buildAndAttach(b);
00089 CPPUNIT_ASSERT(countMinLits() == 0);
00090 }
00091
00092 void testOneLevelLits() {
00093 WeightLitVec min;
00094 ctx.addUnary(c);
00095 ctx.addUnary(~e);
00096 min.push_back( WeightLiteral(a, 1) );
00097 min.push_back( WeightLiteral(b, 2) );
00098 min.push_back( WeightLiteral(c, 1) );
00099 min.push_back( WeightLiteral(a, 2) );
00100 min.push_back( WeightLiteral(d, 1) );
00101 min.push_back( WeightLiteral(e, 2) );
00102 newMin = buildAndAttach(MinimizeBuilder().addRule(min));
00103 CPPUNIT_ASSERT(newMin->numRules() == 1);
00104 CPPUNIT_ASSERT(countMinLits() == 3);
00105 CPPUNIT_ASSERT(newMin->shared()->adjust(0) == 1);
00106 const SharedMinimizeData* data = newMin->shared();
00107 CPPUNIT_ASSERT(data->lits[0].first == a && data->lits[0].second == 3);
00108 for (const WeightLiteral* it = data->lits; !isSentinel(it->first); ++it) {
00109 CPPUNIT_ASSERT_MESSAGE("Minimize lits not sorted!", it->second >= (it+1)->second);
00110 CPPUNIT_ASSERT(ctx.master()->hasWatch(it->first, newMin));
00111 CPPUNIT_ASSERT(ctx.varInfo(it->first.var()).frozen());
00112 }
00113 newMin->destroy(ctx.master(), true);
00114 newMin = 0;
00115 CPPUNIT_ASSERT(!ctx.master()->hasWatch(a, newMin));
00116 }
00117
00118 void testMultiLevelLits() {
00119 MinimizeBuilder builder;
00120 WeightLitVec min;
00121 ctx.addUnary(c);
00122 ctx.addUnary(~e);
00123 min.push_back( WeightLiteral(a, 1) );
00124 min.push_back( WeightLiteral(b, 1) );
00125 min.push_back( WeightLiteral(c, 1) );
00126 min.push_back( WeightLiteral(b, 2) );
00127 min.push_back( WeightLiteral(d, 1) );
00128 min.push_back( WeightLiteral(b, 1) );
00129
00130 builder.addRule(min);
00131 min.clear();
00132 min.push_back( WeightLiteral(e, 2) );
00133 min.push_back( WeightLiteral(f, 1) );
00134 min.push_back( WeightLiteral(x, 2) );
00135 min.push_back( WeightLiteral(y, 3) );
00136 min.push_back( WeightLiteral(b, 1) );
00137 builder.addRule(min);
00138 min.clear();
00139 min.push_back( WeightLiteral(b, 2) );
00140 min.push_back( WeightLiteral(a, 1) );
00141 min.push_back( WeightLiteral(a, 2) );
00142 min.push_back( WeightLiteral(c, 2) );
00143 min.push_back( WeightLiteral(d, 1) );
00144 builder.addRule(min);
00145
00146 newMin = buildAndAttach(builder);
00147 CPPUNIT_ASSERT(newMin->numRules() == 3);
00148 CPPUNIT_ASSERT(countMinLits() == 6);
00149 const SharedMinimizeData* data = newMin->shared();
00150 CPPUNIT_ASSERT(data->adjust(0) == 1 && data->adjust(1) == 0 && data->adjust(2) == 2);
00151 CPPUNIT_ASSERT(data->lits[0].first == b);
00152 CPPUNIT_ASSERT(data->weights.size() == 11);
00153 for (const WeightLiteral* it = data->lits; !isSentinel(it->first); ++it) {
00154 CPPUNIT_ASSERT(ctx.master()->hasWatch(it->first, newMin));
00155 }
00156 }
00157
00158 void testMultiLevelWeightsAreReused() {
00159 MinimizeBuilder builder;
00160 WeightLitVec min;
00161 min.push_back( WeightLiteral(a, 1) );
00162 min.push_back( WeightLiteral(b, 1) );
00163 min.push_back( WeightLiteral(b, 2) );
00164 min.push_back( WeightLiteral(c, 1) );
00165 min.push_back( WeightLiteral(d, 3) );
00166 builder.addRule(min);
00167
00168 min.clear();
00169 min.push_back( WeightLiteral(b, 1) );
00170 min.push_back( WeightLiteral(d, 1) );
00171 builder.addRule(min);
00172
00173 newMin = buildAndAttach(builder);
00174
00175
00176
00177
00178
00179 CPPUNIT_ASSERT(newMin->shared()->weights.size() == 4);
00180 }
00181
00182 void testMergeComplementaryLits() {
00183 MinimizeBuilder builder;
00184 WeightLitVec min;
00185 min.push_back( WeightLiteral(a, 1) );
00186 min.push_back( WeightLiteral(b, 1) );
00187 min.push_back( WeightLiteral(c, 2) );
00188 min.push_back( WeightLiteral(d, 1) );
00189 min.push_back( WeightLiteral(~d, 2) );
00190 builder.addRule(min);
00191 min.clear();
00192 min.push_back( WeightLiteral(~c, 1) );
00193 min.push_back( WeightLiteral(e, 1) );
00194 builder.addRule(min);
00195 newMin = buildAndAttach(builder);
00196 CPPUNIT_ASSERT(countMinLits() == 5);
00197 CPPUNIT_ASSERT(newMin->shared()->adjust(0) == 1 && newMin->shared()->adjust(1) == 1);
00198
00199 ctx.master()->assume(c) && ctx.master()->propagate();
00200 CPPUNIT_ASSERT(newMin->sum(1, true) == 0);
00201
00202 }
00203
00204 void testMergeComplementaryLits2() {
00205 MinimizeBuilder builder;
00206 WeightLitVec min;
00207 min.push_back( WeightLiteral(a, 1) );
00208 min.push_back( WeightLiteral(~a, 1) );
00209 builder.addRule(min);
00210 min.clear();
00211 min.push_back( WeightLiteral(a, 1) );
00212 builder.addRule(min);
00213 newMin = buildAndAttach(builder);
00214 CPPUNIT_ASSERT(countMinLits() == 1);
00215 CPPUNIT_ASSERT(newMin->shared()->adjust(0) == 1 && newMin->shared()->adjust(1) == 0);
00216 }
00217 void testNegativeLowerInit() {
00218 WeightLitVec aMin, bMin;
00219 aMin.push_back( WeightLiteral(a, 1) );
00220 aMin.push_back( WeightLiteral(b, 1) );
00221 bMin.push_back( WeightLiteral(~a, 1) );
00222 bMin.push_back( WeightLiteral(~b, 1) );
00223 data = MinimizeBuilder()
00224 .addRule(aMin)
00225 .addRule(bMin)
00226 .build(ctx);
00227 CPPUNIT_ASSERT(data->lower(0) == 0);
00228 CPPUNIT_ASSERT(data->lower(1) == -2);
00229 }
00230 void testNegativeLower() {
00231 ctx.addBinary(a, b);
00232 WeightLitVec aMin, bMin;
00233 aMin.push_back( WeightLiteral(a, 1) );
00234 aMin.push_back( WeightLiteral(b, 1) );
00235 bMin.push_back( WeightLiteral(~a, 1) );
00236 data = MinimizeBuilder()
00237 .addRule(aMin)
00238 .addRule(bMin)
00239 .build(ctx);
00240 newMin = createMin(ctx, *ctx.master(), data, SolverStrategies::opt_hier);
00241 newMin->integrateBound(*ctx.master());
00242
00243 Solver& s = *ctx.master();
00244 s.assume(b) && s.propagate();
00245 s.assume(~a) && s.propagate();
00246 newMin->handleModel(s);
00247 s.undoUntil(0);
00248 CPPUNIT_ASSERT(!newMin->integrate(s) || !s.propagate());
00249 LitVec ignore;
00250 CPPUNIT_ASSERT(newMin->handleUnsat(s, true, ignore));
00251 CPPUNIT_ASSERT(newMin->integrate(s) && s.propagate());
00252
00253 CPPUNIT_ASSERT(s.isFalse(b));
00254 CPPUNIT_ASSERT(s.assume(a) && s.propagate());
00255 newMin->handleModel(s);
00256 }
00257
00258 void testOrder() {
00259 WeightLitVec aMin, bMin;
00260 aMin.push_back( WeightLiteral(a, 1) );
00261 bMin.push_back( WeightLiteral(b, 1) );
00262 newMin = buildAndAttach(MinimizeBuilder()
00263 .addRule(aMin)
00264 .addRule(bMin));
00265
00266 Solver& solver = *ctx.master();
00267 solver.assume(b);
00268 CPPUNIT_ASSERT_EQUAL(true, solver.propagate());
00269 solver.assume(~a);
00270 CPPUNIT_ASSERT_EQUAL(true, solver.propagate());
00271 CPPUNIT_ASSERT(newMin->sum(0, true) == 0 && newMin->sum(1, true) == 1);
00272 newMin->commitUpperBound(solver);
00273 CPPUNIT_ASSERT(newMin->integrateBound(solver));
00274 CPPUNIT_ASSERT(solver.isFalse(a));
00275 CPPUNIT_ASSERT(solver.isFalse(b));
00276 CPPUNIT_ASSERT(solver.decisionLevel() == 0);
00277 }
00278
00279 void testSkipLevel() {
00280 WeightLitVec aMin, bMin;
00281 aMin.push_back( WeightLiteral(c, 2) );
00282 aMin.push_back( WeightLiteral(d, 1) );
00283 aMin.push_back( WeightLiteral(e, 2) );
00284
00285 bMin.push_back( WeightLiteral(a, 1) );
00286 bMin.push_back( WeightLiteral(b, 1) );
00287
00288 newMin = buildAndAttach(MinimizeBuilder()
00289 .addRule(aMin)
00290 .addRule(bMin));
00291 Solver& solver = *ctx.master();
00292 CPPUNIT_ASSERT_EQUAL(true, solver.assume(a) && solver.propagate());
00293 CPPUNIT_ASSERT_EQUAL(true, solver.assume(b) && solver.propagate());
00294 CPPUNIT_ASSERT_EQUAL(true, solver.assume(~d) && solver.propagate());
00295 CPPUNIT_ASSERT_EQUAL(true, solver.assume(c) && solver.propagate());
00296 solver.force(~e, 0); solver.propagate();
00297 newMin->commitUpperBound(solver);
00298 solver.backtrack();
00299 solver.force(e, 0);
00300 CPPUNIT_ASSERT_EQUAL(true, newMin->integrateBound(solver));
00301 CPPUNIT_ASSERT(solver.decisionLevel() == 2 && solver.backtrackLevel() == 2);
00302 CPPUNIT_ASSERT(solver.isFalse(c) && solver.isFalse(e));
00303 solver.backtrack();
00304 }
00305
00306 void testReassertAfterBacktrack() {
00307 WeightLitVec aMin;
00308 aMin.push_back( WeightLiteral(x, 1) );
00309 aMin.push_back( WeightLiteral(y, 1) );
00310 newMin = buildAndAttach(MinimizeBuilder().addRule(aMin));
00311
00312 ctx.setProject(a.var(), true);
00313 Solver& solver = *ctx.master();
00314 CPPUNIT_ASSERT_EQUAL(true, solver.assume(a) && solver.propagate());
00315 CPPUNIT_ASSERT_EQUAL(true, solver.assume(~x) && solver.propagate());
00316 CPPUNIT_ASSERT_EQUAL(true, solver.assume(y) && solver.propagate());
00317 newMin->commitUpperBound(solver);
00318 solver.undoUntil(1);
00319 solver.setBacktrackLevel(1);
00320 CPPUNIT_ASSERT_EQUAL(true, newMin->integrateBound(solver));
00321 CPPUNIT_ASSERT(solver.decisionLevel() == 1 && solver.isTrue(~x));
00322 solver.backtrack();
00323 CPPUNIT_ASSERT(solver.decisionLevel() == 0 && solver.isTrue(~x));
00324 }
00325
00326 void testConflict() {
00327 WeightLitVec aMin, bMin;
00328 aMin.push_back( WeightLiteral(c, 2) );
00329 aMin.push_back( WeightLiteral(d, 1) );
00330 aMin.push_back( WeightLiteral(e, 2) );
00331
00332 bMin.push_back( WeightLiteral(a, 1) );
00333 bMin.push_back( WeightLiteral(b, 1) );
00334
00335 newMin = buildAndAttach(MinimizeBuilder()
00336 .addRule(aMin)
00337 .addRule(bMin));
00338 Solver& solver = *ctx.master();
00339
00340 CPPUNIT_ASSERT_EQUAL(true, solver.assume(a) && solver.propagate());
00341 CPPUNIT_ASSERT_EQUAL(true, solver.assume(b) && solver.propagate());
00342 CPPUNIT_ASSERT_EQUAL(true, solver.assume(~d) && solver.propagate());
00343 CPPUNIT_ASSERT_EQUAL(true, solver.assume(c) && solver.propagate());
00344 solver.force(~e, 0); solver.propagate();
00345 newMin->commitUpperBound(solver);
00346 solver.undoUntil(0);
00347 CPPUNIT_ASSERT_EQUAL(true, newMin->integrateBound(solver));
00348 CPPUNIT_ASSERT_EQUAL(true, solver.assume(a) && solver.propagate());
00349 solver.force(c, 0);
00350 solver.force(d, 0);
00351 CPPUNIT_ASSERT_EQUAL(false, solver.propagate());
00352 const LitVec& cfl = solver.conflict();
00353 CPPUNIT_ASSERT(cfl.size() == 3);
00354 CPPUNIT_ASSERT(std::find(cfl.begin(), cfl.end(), a) != cfl.end());
00355 CPPUNIT_ASSERT(std::find(cfl.begin(), cfl.end(), c) != cfl.end());
00356 CPPUNIT_ASSERT(std::find(cfl.begin(), cfl.end(), d) != cfl.end());
00357 }
00358
00359 void testOptimize() {
00360 WeightLitVec aMin, bMin;
00361 aMin.push_back( WeightLiteral(a, 1) );
00362 aMin.push_back( WeightLiteral(b, 1) );
00363 bMin.push_back( WeightLiteral(c, 1) );
00364 bMin.push_back( WeightLiteral(d, 1) );
00365 newMin = buildAndAttach(MinimizeBuilder()
00366 .addRule(aMin)
00367 .addRule(bMin));
00368 Solver& solver = *ctx.master();
00369 CPPUNIT_ASSERT_EQUAL(true, solver.assume(a) && solver.propagate());
00370 CPPUNIT_ASSERT_EQUAL(true, solver.assume(c) && solver.propagate());
00371 newMin->commitUpperBound(solver);
00372 solver.undoUntil(0);
00373 CPPUNIT_ASSERT_EQUAL(true, newMin->integrateBound(solver));
00374 CPPUNIT_ASSERT_EQUAL(true, solver.assume(d) && solver.propagate());
00375 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~a));
00376 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~b));
00377 CPPUNIT_ASSERT_EQUAL(value_free, solver.value(c.var()));
00378 }
00379
00380 void testEnumerate() {
00381 WeightLitVec aMin, bMin;
00382 aMin.push_back( WeightLiteral(a, 1) );
00383 aMin.push_back( WeightLiteral(b, 1) );
00384 bMin.push_back( WeightLiteral(c, 1) );
00385 bMin.push_back( WeightLiteral(d, 1) );
00386 wsum_t bound[2] = {1,1};
00387 newMin = buildAndAttach(MinimizeBuilder()
00388 .addRule(aMin)
00389 .addRule(bMin)
00390 , MinimizeMode_t::enumerate, bound, 2);
00391
00392 Solver& solver = *ctx.master();
00393 CPPUNIT_ASSERT_EQUAL(true, solver.propagate());
00394
00395 CPPUNIT_ASSERT_EQUAL(true, solver.assume(~a) && solver.propagate());
00396 CPPUNIT_ASSERT_EQUAL(true, solver.assume(c) && solver.propagate());
00397
00398 newMin->commitUpperBound(solver);
00399 solver.undoUntil(0);
00400 newMin->relaxBound();
00401 newMin->integrateBound(solver);
00402 CPPUNIT_ASSERT(solver.queueSize() == 0);
00403
00404 CPPUNIT_ASSERT_EQUAL(true, solver.assume(d) && solver.propagate());
00405 CPPUNIT_ASSERT_EQUAL(true, solver.assume(b) && solver.propagate());
00406 CPPUNIT_ASSERT(solver.isTrue(~c));
00407 CPPUNIT_ASSERT(solver.isTrue(~a));
00408 }
00409
00410 void testComputeImplicationLevel() {
00411 WeightLitVec aMin;
00412 aMin.push_back( WeightLiteral(a, 1) );
00413 aMin.push_back( WeightLiteral(b, 1) );
00414 aMin.push_back( WeightLiteral(c, 1) );
00415 aMin.push_back( WeightLiteral(d, 2) );
00416 newMin = buildAndAttach(MinimizeBuilder()
00417 .addRule(aMin));
00418 Solver& solver = *ctx.master();
00419 solver.assume(a) && solver.propagate();
00420 solver.force(b,0)&& solver.propagate();
00421 solver.assume(c) && solver.propagate();
00422 solver.force(~d,0) && solver.propagate();
00423 newMin->commitUpperBound(solver);
00424 solver.undoUntil(1u);
00425 CPPUNIT_ASSERT(newMin->integrateBound(solver));
00426 CPPUNIT_ASSERT(solver.isFalse(d));
00427 LitVec r1, r2;
00428 solver.reason(~d, r1);
00429 solver.undoUntil(0);
00430 solver.assume(a) && solver.propagate();
00431 solver.reason(~d, r2);
00432 CPPUNIT_ASSERT(r2.size() <= r1.size() && r2.size() == 1);
00433 CPPUNIT_ASSERT(r1[0] == r2[0]);
00434 CPPUNIT_ASSERT(r1.size() == 1 || b == r1[1]);
00435 CPPUNIT_ASSERT_MESSAGE("TODO: REASON CORRECT BUT NOT MINIMAL!", r1.size() == r2.size());
00436 }
00437
00438 void testSetModelMayBacktrackMultiLevels() {
00439 WeightLitVec aMin;
00440 aMin.push_back( WeightLiteral(a, 1) );
00441 newMin = buildAndAttach(MinimizeBuilder().addRule(aMin));
00442 Solver& solver = *ctx.master();
00443 CPPUNIT_ASSERT_EQUAL(true, solver.assume(a) && solver.propagate());
00444 CPPUNIT_ASSERT_EQUAL(true, solver.assume(b) && solver.propagate());
00445 CPPUNIT_ASSERT_EQUAL(true, solver.assume(c) && solver.propagate());
00446 newMin->commitUpperBound(solver);
00447 newMin->integrateBound(solver);
00448 CPPUNIT_ASSERT(solver.decisionLevel() == 0);
00449 }
00450
00451 void testPriorityBug() {
00452 WeightLitVec aMin, bMin;
00453 aMin.push_back( WeightLiteral(a, 1) );
00454 aMin.push_back( WeightLiteral(b, 1) );
00455 aMin.push_back( WeightLiteral(c, 1) );
00456 bMin.push_back( WeightLiteral(d, 1) );
00457 bMin.push_back( WeightLiteral(e, 1) );
00458 bMin.push_back( WeightLiteral(f, 1) );
00459 newMin = buildAndAttach(MinimizeBuilder()
00460 .addRule(aMin)
00461 .addRule(bMin));
00462
00463 ctx.setProject(a.var(), true);
00464 ctx.setProject(e.var(), true);
00465 Solver& solver = *ctx.master();
00466 CPPUNIT_ASSERT_EQUAL(true, solver.assume(a) && solver.propagate());
00467 CPPUNIT_ASSERT_EQUAL(true, solver.assume(e) && solver.propagate());
00468 CPPUNIT_ASSERT_EQUAL(true, solver.assume(f) && solver.propagate());
00469 newMin->commitUpperBound(solver);
00470 solver.backtrack();
00471 CPPUNIT_ASSERT_EQUAL(true, newMin->integrateBound(solver));
00472 CPPUNIT_ASSERT(solver.decisionLevel() == 2);
00473 solver.backtrack();
00474 CPPUNIT_ASSERT_EQUAL(true, solver.propagate());
00475 CPPUNIT_ASSERT_EQUAL(true, solver.assume(d) && solver.propagate());
00476 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~b));
00477 LitVec r;
00478 solver.reason(~b, r);
00479 CPPUNIT_ASSERT(LitVec::size_type(1) == r.size());
00480 CPPUNIT_ASSERT(a == r[0]);
00481 }
00482
00483 void testStrengthenImplication() {
00484 WeightLitVec aMin;
00485 aMin.push_back( WeightLiteral(a, 1) );
00486 aMin.push_back( WeightLiteral(b, 2) );
00487 aMin.push_back( WeightLiteral(c, 1) );
00488 wsum_t bound = 2;
00489 newMin = buildAndAttach(MinimizeBuilder().addRule(aMin), MinimizeMode_t::optimize, &bound, 1);
00490 Solver& solver = *ctx.master();
00491 solver.assume(a) && solver.propagate();
00492 solver.setBacktrackLevel(1);
00493 ctx.setProject(a.var(), true);
00494 CPPUNIT_ASSERT(solver.isTrue(~b));
00495 LitVec r;
00496 solver.reason(~b, r);
00497 CPPUNIT_ASSERT(r.size() == 1 && r[0] == a);
00498 solver.assume(x) && solver.propagate();
00499 solver.assume(y) && solver.propagate();
00500 solver.assume(c) && solver.propagate();
00501 solver.assume(e) && solver.propagate();
00502 newMin->commitUpperBound(solver);
00503 solver.undoUntil(3);
00504 CPPUNIT_ASSERT(newMin->integrateBound(solver));
00505 CPPUNIT_ASSERT(solver.decisionLevel() == 1 && solver.isTrue(~b));
00506 r.clear();
00507 solver.reason(~b, r);
00508 CPPUNIT_ASSERT(r.empty() || (r.size() == 1 && r[0] == posLit(0)));
00509 }
00510
00511 void testRootLevelMadness() {
00512 WeightLitVec aMin, bMin;
00513 aMin.push_back( WeightLiteral(a, 1) );
00514 aMin.push_back( WeightLiteral(b, 2) );
00515 aMin.push_back( WeightLiteral(c, 1) );
00516 bMin.push_back( WeightLiteral(d, 1) );
00517 bMin.push_back( WeightLiteral(e, 2) );
00518 bMin.push_back( WeightLiteral(f, 1) );
00519 newMin = buildAndAttach(MinimizeBuilder()
00520 .addRule(aMin)
00521 .addRule(bMin));
00522 Solver& solver = *ctx.master();
00523 solver.assume(a) && solver.propagate();
00524 solver.assume(c) && solver.propagate();
00525 solver.pushRootLevel(2);
00526 SumVec opt(newMin->numRules());
00527 opt[0] = 2;
00528 opt[1] = 3;
00529 setOptimum(solver, opt, false);
00530 LitVec r;
00531 CPPUNIT_ASSERT(solver.isFalse(b));
00532 solver.reason(~b, r);
00533 CPPUNIT_ASSERT(r.size() == 1 && r[0] == a);
00534 solver.clearAssumptions();
00535 solver.assume(d) && solver.propagate();
00536 solver.assume(e) && solver.propagate();
00537 solver.assume(f) && solver.propagate();
00538 solver.pushRootLevel(3);
00539 opt[0] = 2;
00540 opt[1] = 2;
00541 setOptimum(solver, opt, false);
00542 CPPUNIT_ASSERT(solver.isFalse(b));
00543 r.clear();
00544 solver.reason(~b, r);
00545 CPPUNIT_ASSERT(r.size() == 2 && r[0] == d && r[1] == e);
00546 }
00547
00548 void testIntegrateOptimum() {
00549 WeightLitVec aMin;
00550 aMin.push_back( WeightLiteral(a, 1) );
00551 aMin.push_back( WeightLiteral(b, 1) );
00552 aMin.push_back( WeightLiteral(c, 1) );
00553 aMin.push_back( WeightLiteral(d, 1) );
00554 Solver& solver = *ctx.master();
00555 data = MinimizeBuilder().addRule(aMin).build(ctx);
00556 newMin = createMin(ctx, solver, data);
00557 newMin->integrateBound(solver);
00558 solver.assume(a) && solver.propagate();
00559 solver.assume(e) && solver.propagate();
00560 solver.assume(b) && solver.propagate();
00561 solver.assume(f) && solver.propagate();
00562 solver.assume(c) && solver.propagate();
00563
00564 SumVec opt(data->numRules());
00565 opt[0] = 2;
00566 CPPUNIT_ASSERT(setOptimum(solver, opt, true));
00567 CPPUNIT_ASSERT(solver.decisionLevel() == 1 && solver.queueSize() == 3);
00568 newMin->destroy(&solver, true);
00569 newMin = 0;
00570 }
00571
00572 void testIntegrateOptimumConflict() {
00573 WeightLitVec aMin;
00574 aMin.push_back( WeightLiteral(a, 1) );
00575 aMin.push_back( WeightLiteral(b, 1) );
00576 aMin.push_back( WeightLiteral(c, 1) );
00577 aMin.push_back( WeightLiteral(d, 1) );
00578 Solver& solver = *ctx.master();
00579 data = MinimizeBuilder().addRule(aMin).build(ctx);
00580 SumVec opt(data->numRules());
00581 newMin = createMin(ctx, solver, data);
00582 newMin->integrateBound(solver);
00583 solver.assume(a) && solver.propagate();
00584 solver.assume(e) && solver.propagate();
00585 solver.assume(b) && solver.propagate();
00586 solver.assume(f) && solver.propagate();
00587 solver.assume(c) && solver.propagate();
00588 ctx.setProject(a.var(), true);
00589 ctx.setProject(b.var(), true);
00590 solver.setBacktrackLevel(3);
00591 opt[0] = 2;
00592 CPPUNIT_ASSERT(setOptimum(solver, opt, true));
00593 CPPUNIT_ASSERT(solver.decisionLevel() == 1 && solver.queueSize() == 3);
00594 solver.propagate();
00595 opt[0] = 0;
00596 CPPUNIT_ASSERT(!setOptimum(solver, opt, true));
00597 CPPUNIT_ASSERT(solver.hasConflict());
00598 CPPUNIT_ASSERT(solver.clearAssumptions());
00599 CPPUNIT_ASSERT(newMin->integrateBound(solver) == false && solver.hasConflict());
00600 CPPUNIT_ASSERT(!solver.resolveConflict());
00601 newMin->destroy(&solver, true);
00602 newMin = 0;
00603 }
00604 void testIntegrateBug() {
00605 WeightLitVec min;
00606 min.push_back( WeightLiteral(a, 1) );
00607 min.push_back( WeightLiteral(b, 1) );
00608 min.push_back( WeightLiteral(c, 1) );
00609 data = MinimizeBuilder().addRule(min).build(ctx);
00610 wsum_t bound = 2;
00611 Solver& s = *ctx.master();
00612 newMin = createMin(ctx, s, data, SolverStrategies::opt_dec);
00613 data->setMode(MinimizeMode_t::optimize, &bound, 1);
00614 s.pushRoot(s.tagLiteral());
00615 s.pushRoot(a);
00616 s.pushRoot(b);
00617 s.pushRoot(c);
00618 CPPUNIT_ASSERT(!newMin->integrateBound(s));
00619 }
00620 void testReasonBug() {
00621 WeightLitVec aMin, bMin;
00622 aMin.push_back( WeightLiteral(a, 1) );
00623 aMin.push_back( WeightLiteral(b, 1) );
00624 bMin.push_back( WeightLiteral(d, 2) );
00625 bMin.push_back( WeightLiteral(e, 1) );
00626 bMin.push_back( WeightLiteral(f, 3) );
00627
00628 newMin = buildAndAttach(MinimizeBuilder()
00629 .addRule(aMin)
00630 .addRule(bMin));
00631 Solver& solver = *ctx.master();
00632 CPPUNIT_ASSERT_EQUAL(true, solver.assume(a) && solver.propagate());
00633 CPPUNIT_ASSERT_EQUAL(true, solver.assume(b) && solver.propagate());
00634 CPPUNIT_ASSERT_EQUAL(true, solver.assume(d) && solver.propagate());
00635 newMin->commitUpperBound(solver);
00636 solver.backtrack();
00637 CPPUNIT_ASSERT_EQUAL(true, newMin->integrateBound(solver));
00638 CPPUNIT_ASSERT_EQUAL(true, solver.assume(e) && solver.propagate());
00639 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~f));
00640 CPPUNIT_ASSERT_EQUAL(true, solver.assume(c) && solver.propagate());
00641 solver.backtrack();
00642 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~f));
00643 LitVec r;
00644 solver.reason(~f, r);
00645 CPPUNIT_ASSERT(std::find(r.begin(), r.end(), e) == r.end());
00646 }
00647
00648 void testSmartBacktrack() {
00649 WeightLitVec aMin;
00650 aMin.push_back( WeightLiteral(a, 1) );
00651 aMin.push_back( WeightLiteral(b, 1) );
00652 aMin.push_back( WeightLiteral(c, 1) );
00653 newMin = buildAndAttach(MinimizeBuilder().addRule(aMin));
00654 Solver& solver = *ctx.master();
00655 CPPUNIT_ASSERT_EQUAL(true, solver.assume(a) && solver.propagate());
00656 CPPUNIT_ASSERT_EQUAL(true, solver.assume(b) && solver.propagate());
00657 CPPUNIT_ASSERT_EQUAL(true, solver.assume(~c) && solver.propagate());
00658
00659 newMin->commitUpperBound(solver);
00660 CPPUNIT_ASSERT_EQUAL(true, newMin->integrateBound(solver));
00661
00662 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~b));
00663 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~c));
00664 }
00665
00666 void testBacktrackToTrue() {
00667 WeightLitVec min1, min2;
00668 min1.push_back( WeightLiteral(a, 1) );
00669 min2.push_back( WeightLiteral(b, 1) );
00670 newMin = buildAndAttach(MinimizeBuilder()
00671 .addRule(min1)
00672 .addRule(min2));
00673 Solver& solver = *ctx.master();
00674 CPPUNIT_ASSERT_EQUAL(true, solver.assume(~a) && solver.propagate());
00675 CPPUNIT_ASSERT_EQUAL(true, solver.force(b, 0) && solver.propagate());
00676
00677 newMin->commitUpperBound(solver);
00678 solver.backtrack();
00679 CPPUNIT_ASSERT_EQUAL(false, newMin->integrateBound(solver));
00680 }
00681
00682 void testMultiAssignment() {
00683 WeightLitVec min1, min2;
00684 min1.push_back( WeightLiteral(a, 1) );
00685 min1.push_back( WeightLiteral(b, 1) );
00686 min1.push_back( WeightLiteral(c, 1) );
00687 min1.push_back( WeightLiteral(d, 1) );
00688 min1.push_back( WeightLiteral(e, 1) );
00689
00690 min2.push_back( WeightLiteral(f, 1) );
00691
00692 newMin = buildAndAttach(MinimizeBuilder()
00693 .addRule(min1)
00694 .addRule(min2));
00695 Solver& solver = *ctx.master();
00696 SumVec opt(newMin->numRules());
00697 opt[0] = 3;
00698 opt[1] = 0;
00699 CPPUNIT_ASSERT_EQUAL(true, setOptimum(solver, opt, false));
00700
00701 solver.assume(f);
00702 solver.force(a, 0);
00703 solver.force(b, 0);
00704 solver.force(c, 0);
00705
00706 CPPUNIT_ASSERT_EQUAL(false, solver.propagate());
00707 }
00708
00709 void testBugBacktrackFromFalse() {
00710 WeightLitVec min1, min2;
00711 min1.push_back( WeightLiteral(a, 1) );
00712 min1.push_back( WeightLiteral(b, 1) );
00713 min1.push_back( WeightLiteral(c, 1) );
00714 min2.push_back( WeightLiteral(d, 1) );
00715 min2.push_back( WeightLiteral(e, 1) );
00716 min2.push_back( WeightLiteral(f, 1) );
00717
00718 newMin = buildAndAttach(MinimizeBuilder()
00719 .addRule(min1)
00720 .addRule(min2));
00721 ctx.setProject(x.var(), true);
00722 Solver& solver = *ctx.master();
00723 CPPUNIT_ASSERT_EQUAL(true, solver.assume(a) && solver.propagate());
00724 CPPUNIT_ASSERT_EQUAL(true, solver.assume(b) && solver.propagate());
00725 CPPUNIT_ASSERT_EQUAL(true, solver.assume(x) && solver.propagate());
00726 CPPUNIT_ASSERT_EQUAL(true, solver.force(~c,0) && solver.propagate());
00727 CPPUNIT_ASSERT_EQUAL(true, solver.assume(y) && solver.propagate());
00728 CPPUNIT_ASSERT_EQUAL(true, solver.force(d,0) && solver.propagate());
00729 CPPUNIT_ASSERT_EQUAL(true, solver.force(e,0) && solver.propagate());
00730 CPPUNIT_ASSERT_EQUAL(true, solver.force(~f,0) && solver.propagate());
00731
00732 newMin->commitUpperBound(solver);
00733 solver.undoUntil(3);
00734 solver.setBacktrackLevel(3);
00735 CPPUNIT_ASSERT(newMin->integrateBound(solver));
00736 CPPUNIT_ASSERT_EQUAL(true, solver.force(f,0) && solver.propagate());
00737 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~d));
00738 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~e));
00739
00740 newMin->commitUpperBound(solver);
00741 solver.undoUntil(2);
00742 solver.backtrack();
00743 CPPUNIT_ASSERT(newMin->integrateBound(solver));
00744 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~x));
00745 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~f));
00746 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~d));
00747 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~e));
00748 CPPUNIT_ASSERT_EQUAL(true, solver.isTrue(~c));
00749 }
00750
00751 void testBugBacktrackToTrue() {
00752 WeightLitVec min1, min2;
00753 min1.push_back( WeightLiteral(a, 1) );
00754 min1.push_back( WeightLiteral(b, 1) );
00755 min1.push_back( WeightLiteral(~b, 2) );
00756 min2.push_back( WeightLiteral(a, 1) );
00757 min2.push_back( WeightLiteral(b, 1) );
00758 min2.push_back( WeightLiteral(c, 1) );
00759
00760 newMin = buildAndAttach(MinimizeBuilder()
00761 .addRule(min1)
00762 .addRule(min2));
00763 Solver& solver = *ctx.master();
00764
00765 CPPUNIT_ASSERT_EQUAL(true, solver.assume(a) && solver.propagate());
00766 CPPUNIT_ASSERT_EQUAL(true, solver.assume(b) && solver.propagate());
00767 CPPUNIT_ASSERT_EQUAL(true, solver.assume(c) && solver.propagate());
00768
00769 newMin->commitUpperBound(solver);
00770 CPPUNIT_ASSERT(newMin->integrateBound(solver) && 1 == solver.decisionLevel());
00771 CPPUNIT_ASSERT(solver.propagate());
00772
00773 newMin->commitUpperBound(solver);
00774 solver.undoUntil(0);
00775 CPPUNIT_ASSERT(newMin->integrateBound(solver));
00776 CPPUNIT_ASSERT(solver.isTrue(~a));
00777 CPPUNIT_ASSERT(solver.value(b.var()) == value_free);
00778 }
00779
00780 void testBugInitOptHierarch() {
00781 WeightLitVec aMin, bMin;
00782 aMin.push_back( WeightLiteral(a, 1) );
00783 aMin.push_back( WeightLiteral(b, 1) );
00784 bMin.push_back( WeightLiteral(c, 1) );
00785 bMin.push_back( WeightLiteral(d, 1) );
00786 data = MinimizeBuilder()
00787 .addRule(aMin)
00788 .addRule(bMin)
00789 .build(ctx);
00790 wsum_t bound[2] = {wsum_t(1),wsum_t(1)};
00791 data->setMode(MinimizeMode_t::optimize, bound, 2);
00792 newMin = createMin(ctx, *ctx.master(), data, SolverStrategies::opt_hier);
00793 newMin->integrateBound(*ctx.master());
00794 CPPUNIT_ASSERT(ctx.master()->value(a.var()) == value_free);
00795 ctx.master()->assume(a) && ctx.master()->propagate();
00796 CPPUNIT_ASSERT(ctx.master()->isFalse(b));
00797 CPPUNIT_ASSERT(ctx.master()->value(c.var()) == value_free);
00798 ctx.master()->assume(c) && ctx.master()->propagate();
00799 CPPUNIT_ASSERT(ctx.master()->isFalse(d));
00800 }
00801
00802 void testBugAdjustSum() {
00803 WeightLitVec aMin, bMin;
00804 aMin.push_back( WeightLiteral(a, 1) );
00805 aMin.push_back( WeightLiteral(b, 1) );
00806 bMin.push_back( WeightLiteral(~a, 1) );
00807 bMin.push_back( WeightLiteral(d, 1) );
00808 data = MinimizeBuilder()
00809 .addRule(aMin)
00810 .addRule(bMin)
00811 .build(ctx);
00812 newMin = static_cast<DefaultMinimize*>(data->attach(*ctx.master()));
00813 SumVec opt;
00814 opt.push_back(1);
00815 opt.push_back(1);
00816 setOptimum(*ctx.master(), opt, true);
00817
00818 CPPUNIT_ASSERT(ctx.master()->value(a.var()) == value_free);
00819 CPPUNIT_ASSERT(ctx.master()->assume(a) && ctx.master()->propagate());
00820 CPPUNIT_ASSERT(ctx.master()->assume(~b) && ctx.master()->propagate());
00821 CPPUNIT_ASSERT(ctx.master()->assume(~d) && ctx.master()->propagate());
00822 }
00823
00824 void testWeightNullBug() {
00825 WeightLitVec min1;
00826 min1.push_back( WeightLiteral(a, 1) );
00827 min1.push_back( WeightLiteral(b, 0) );
00828 newMin = buildAndAttach(MinimizeBuilder().addRule(min1));
00829 Solver& solver = *ctx.master();
00830 CPPUNIT_ASSERT_EQUAL(true, solver.assume(a) && solver.propagate());
00831 CPPUNIT_ASSERT_EQUAL(true, solver.assume(b) && solver.force(~c,0) && solver.propagate());
00832 newMin->commitUpperBound(solver);
00833 newMin->integrateBound(solver);
00834 CPPUNIT_ASSERT(0u == solver.decisionLevel() && solver.isFalse(a));
00835 }
00836
00837 void testAdjust() {
00838 WeightLitVec min1;
00839 min1.push_back( WeightLiteral(a, 1) );
00840 min1.push_back( WeightLiteral(b, 1) );
00841 newMin = buildAndAttach(MinimizeBuilder().addRule(min1, -2));
00842 Solver& solver = *ctx.master();
00843 CPPUNIT_ASSERT_EQUAL(true, solver.assume(a) && solver.propagate());
00844 CPPUNIT_ASSERT_EQUAL(true, solver.assume(b) && solver.propagate());
00845 newMin->commitUpperBound(solver);
00846 CPPUNIT_ASSERT(0 == newMin->shared()->optimum(0));
00847
00848 solver.clearAssumptions();
00849 CPPUNIT_ASSERT_EQUAL(true, solver.assume(~a) && solver.propagate());
00850 CPPUNIT_ASSERT_EQUAL(true, solver.assume(~b) && solver.propagate());
00851 newMin->commitUpperBound(solver);
00852 CPPUNIT_ASSERT(-2 == newMin->shared()->optimum(0));
00853 }
00854
00855 void testAdjustFact() {
00856 WeightLitVec min1;
00857 min1.push_back( WeightLiteral(a, 2) );
00858 min1.push_back( WeightLiteral(b, 1) );
00859 min1.push_back( WeightLiteral(c, 1) );
00860 min1.push_back( WeightLiteral(d, 1) );
00861 data = MinimizeBuilder().addRule(min1, -2).build(ctx);
00862 Solver& solver = *ctx.master();
00863 ctx.addUnary(a);
00864 solver.propagate();
00865 newMin = createMin(ctx, solver, data);
00866 newMin->integrateBound(solver);
00867 CPPUNIT_ASSERT_EQUAL(true, solver.assume(b) && solver.propagate());
00868 CPPUNIT_ASSERT_EQUAL(true, solver.assume(c) && solver.propagate());
00869 CPPUNIT_ASSERT_EQUAL(true, solver.assume(d) && solver.propagate());
00870 newMin->commitUpperBound(solver);
00871 newMin->integrateBound(solver);
00872 CPPUNIT_ASSERT(2 == solver.decisionLevel());
00873 }
00874
00875 void testAssumption() {
00876 SharedContext ctx;
00877 a = posLit(ctx.addVar(Var_t::atom_var));
00878 b = posLit(ctx.addVar(Var_t::atom_var));
00879 c = posLit(ctx.addVar(Var_t::atom_var));
00880 ctx.startAddConstraints();
00881 WeightLitVec min1;
00882 min1.push_back( WeightLiteral(a, 1) );
00883 min1.push_back( WeightLiteral(b, 1) );
00884 min1.push_back( WeightLiteral(c, 1) );
00885 Solver& solver = *ctx.master();
00886 data = MinimizeBuilder().addRule(min1).build(ctx);
00887 newMin = createMin(ctx, solver, data, SolverStrategies::opt_inc);
00888 Literal minAssume = posLit(solver.pushTagVar(true));
00889 SumVec opt(1, 0);
00890 setOptimum(solver, opt, false);
00891 CPPUNIT_ASSERT(solver.isFalse(a) && solver.reason(~a).constraint() == newMin);
00892 CPPUNIT_ASSERT(solver.isFalse(b) && solver.reason(~b).constraint() == newMin);
00893 CPPUNIT_ASSERT(solver.isFalse(c) && solver.reason(~c).constraint() == newMin);
00894
00895 LitVec r;
00896 solver.reason(~a, r);
00897 CPPUNIT_ASSERT(r.size() == 1 && r[0] == minAssume);
00898
00899 solver.clearAssumptions();
00900 CPPUNIT_ASSERT(solver.numAssignedVars() == 0);
00901 }
00902
00903 void testHierarchicalSetModel() {
00904 WeightLitVec min;
00905 min.push_back( WeightLiteral(a, 1) );
00906 min.push_back( WeightLiteral(b, 1) );
00907 min.push_back( WeightLiteral(c, 1) );
00908 MinimizeBuilder builder;
00909 builder.addRule(min);
00910 min.clear();
00911 min.push_back( WeightLiteral(d, 1) );
00912 min.push_back( WeightLiteral(e, 1) );
00913 min.push_back( WeightLiteral(f, 1) );
00914 builder.addRule(min);
00915 Solver& solver = *ctx.master();
00916 data = builder.build(ctx);
00917 newMin = createMin(ctx, solver, data, SolverStrategies::opt_hier);
00918 newMin->integrateBound(solver);
00919 solver.assume(a); solver.propagate();
00920 solver.assume(b); solver.propagate();
00921 solver.assume(c); solver.propagate();
00922 solver.assume(d); solver.propagate();
00923 solver.assume(e); solver.propagate();
00924 solver.assume(f); solver.propagate();
00925 newMin->commitUpperBound(solver);
00926 solver.undoUntil(solver.level(b.var()));
00927 newMin->integrateBound(solver);
00928 CPPUNIT_ASSERT(solver.isFalse(c));
00929 CPPUNIT_ASSERT(solver.numAssignedVars() == 4);
00930 }
00931
00932 void testHierarchical() {
00933 MinimizeBuilder builder;
00934 WeightLitVec min;
00935 min.push_back( WeightLiteral(a, 1) );
00936 builder.addRule(min);
00937 min.clear();
00938 min.push_back( WeightLiteral(~b, 1) );
00939 builder.addRule(min);
00940
00941 ctx.addBinary(~a, b);
00942 ctx.addBinary(a, ~b);
00943 Solver& solver = *ctx.master();
00944 data = builder.build(ctx);
00945 newMin = createMin(ctx, solver, data, SolverStrategies::opt_hier);
00946 newMin->integrateBound(solver);
00947 solver.assume(a);
00948 solver.propagate();
00949 newMin->commitUpperBound(solver);
00950 solver.backtrack();
00951 CPPUNIT_ASSERT(newMin->integrateBound(solver));
00952 CPPUNIT_ASSERT(solver.propagate() == true);
00953 newMin->commitUpperBound(solver);
00954 CPPUNIT_ASSERT(!newMin->integrateBound(solver));
00955 }
00956 void testInconsistent() {
00957 MinimizeBuilder builder;
00958 WeightLitVec min;
00959 min.push_back( WeightLiteral(a, 1) );
00960 min.push_back( WeightLiteral(b, 1) );
00961 min.push_back( WeightLiteral(c, 1) );
00962 builder.addRule(min);
00963 wsum_t bound = 1;
00964 ctx.addUnary(a);
00965 ctx.addUnary(b);
00966 CPPUNIT_ASSERT(buildAndAttach(builder, MinimizeMode_t::optimize, &bound, 1) == 0);
00967 }
00968 private:
00969 uint32 countMinLits() const {
00970 uint32 lits = 0;
00971 const WeightLiteral* it = newMin->shared()->lits;
00972 for (; !isSentinel(it->first); ++it, ++lits) { ; }
00973 return lits;
00974 }
00975
00976 bool setOptimum(Solver& s, SumVec& vec, bool less) {
00977 SharedMinimizeData* data = const_cast<SharedMinimizeData*>(newMin->shared());
00978 if (!less) {
00979 vec.back() += 1;
00980 }
00981 data->setOptimum(&vec[0]);
00982 while (!newMin->integrateBound(s)) {
00983 if (!s.resolveConflict()) { return false; }
00984 }
00985 return true;
00986 }
00987 DefaultMinimize* createMin(SharedContext& ctx, Solver& s, SharedMinimizeData* data, SolverStrategies::OptStrategy str = SolverStrategies::opt_def) {
00988 ctx.endInit();
00989 return static_cast<DefaultMinimize*>(data->attach(s, str));
00990 }
00991 DefaultMinimize* buildAndAttach(MinimizeBuilder& x, MinimizeMode m = MinimizeMode_t::optimize, const wsum_t* b = 0, uint32 bs = 0) {
00992 DefaultMinimize* con = 0;
00993 if ( (data = x.build(ctx)) != 0 && data->setMode(m, b, bs) ) {
00994 con = createMin(ctx, *ctx.master(), data);
00995 con->integrateBound(*ctx.master());
00996 }
00997 return con;
00998 }
00999 SharedContext ctx;
01000 DefaultMinimize* newMin;
01001 SharedMinimizeData* data;
01002 Literal a, b, c, d, e, f, x, y;
01003 };
01004
01005 class UncoreMinimizeTest : public CppUnit::TestFixture {
01006 CPPUNIT_TEST_SUITE(UncoreMinimizeTest);
01007 CPPUNIT_TEST(testEmpty);
01008 CPPUNIT_TEST(testEnumerate);
01009 CPPUNIT_TEST(testOptimize);
01010 CPPUNIT_TEST(testOptimizeGP);
01011 CPPUNIT_TEST(testMtBug1);
01012 CPPUNIT_TEST(testNegativeLower);
01013 CPPUNIT_TEST_SUITE_END();
01014 public:
01015 void setUp() {
01016 data = 0;
01017 min = 0;
01018 }
01019 void tearDown() {
01020 if (min) {
01021 min->destroy(0,false);
01022 }
01023 if (data) {
01024 data->release();
01025 }
01026 }
01027 void testEmpty() {
01028 MinimizeBuilder b;
01029 ctx.startAddConstraints();
01030 data = b.build(ctx);
01031 ctx.endInit();
01032 min = data->attach(*ctx.master(), SolverStrategies::opt_unsat_pre);
01033 CPPUNIT_ASSERT(min->integrate(*ctx.master()));
01034 }
01035 void testEnumerate() {
01036 Var a = ctx.addVar(Var_t::atom_var);
01037 Var b = ctx.addVar(Var_t::atom_var);
01038 Var c = ctx.addVar(Var_t::atom_var);
01039 ctx.startAddConstraints();
01040 WeightLitVec lits;
01041 MinimizeBuilder builder;
01042 lits.push_back(WeightLiteral(posLit(a), 1));
01043 lits.push_back(WeightLiteral(posLit(b), 1));
01044 lits.push_back(WeightLiteral(posLit(c), 1));
01045 builder.addRule(lits);
01046 data = builder.build(ctx);
01047 ctx.endInit();
01048 wsum_t bound = 1;
01049 data->setMode(MinimizeMode_t::enumerate, &bound, 1);
01050 min = data->attach(*ctx.master(), SolverStrategies::opt_unsat_pre);
01051 CPPUNIT_ASSERT(min->integrate(*ctx.master()));
01052
01053 ctx.master()->assume(posLit(a));
01054 ctx.master()->propagate();
01055 CPPUNIT_ASSERT(ctx.master()->isFalse(posLit(b)));
01056 CPPUNIT_ASSERT(ctx.master()->isFalse(posLit(c)));
01057 }
01058 void testOptimize() {
01059 Var a = ctx.addVar(Var_t::atom_var);
01060 Var b = ctx.addVar(Var_t::atom_var);
01061 Solver& s = ctx.startAddConstraints();
01062 WeightLitVec lits;
01063 MinimizeBuilder builder;
01064 lits.push_back(WeightLiteral(posLit(a), 1));
01065 lits.push_back(WeightLiteral(posLit(b), 1));
01066 builder.addRule(lits);
01067 data = builder.build(ctx);
01068 ctx.endInit();
01069 data->setMode(MinimizeMode_t::optimize);
01070 min = data->attach(s, SolverStrategies::opt_unsat_pre);
01071 BasicSolve solve(s);
01072 LitVec gp;
01073 while (min->integrate(s) || min->handleUnsat(s, true, gp)) {
01074 ValueRep v = solve.solve();
01075 CPPUNIT_ASSERT(v == value_true);
01076 min->handleModel(s);
01077 }
01078 CPPUNIT_ASSERT(gp.empty());
01079 CPPUNIT_ASSERT(s.isFalse(lits[0].first) && s.isFalse(lits[1].first));
01080 }
01081 void testOptimizeGP() {
01082 Var a = ctx.addVar(Var_t::atom_var);
01083 Var b = ctx.addVar(Var_t::atom_var);
01084 Solver& s = ctx.startAddConstraints();
01085 WeightLitVec lits;
01086 MinimizeBuilder builder;
01087 lits.push_back(WeightLiteral(posLit(a), 1));
01088 lits.push_back(WeightLiteral(posLit(b), 1));
01089 builder.addRule(lits);
01090 data = builder.build(ctx);
01091 ctx.endInit();
01092 data->setMode(MinimizeMode_t::optimize);
01093 min = data->attach(s, SolverStrategies::opt_unsat_pre);
01094 BasicSolve solve(s);
01095 LitVec gp; gp.push_back(posLit(a));
01096 solve.assume(gp);
01097 gp.clear();
01098 while (min->integrate(s) || min->handleUnsat(s, true, gp)) {
01099 ValueRep v = solve.solve();
01100 CPPUNIT_ASSERT(v == value_true);
01101 min->handleModel(s);
01102 }
01103 CPPUNIT_ASSERT(s.rootLevel() == 1 && s.decision(1) == posLit(a));
01104 CPPUNIT_ASSERT(s.isTrue(lits[0].first) && s.isFalse(lits[1].first));
01105 }
01106
01107 void testMtBug1() {
01108 WeightLitVec lits;
01109 lits.push_back(WeightLiteral(posLit(ctx.addVar(Var_t::atom_var)), 1));
01110 lits.push_back(WeightLiteral(posLit(ctx.addVar(Var_t::atom_var)), 1));
01111 Solver& s1 = ctx.startAddConstraints();
01112 data = MinimizeBuilder().addRule(lits).build(ctx);
01113 ctx.setConcurrency(2);
01114 ctx.endInit(true);
01115 Solver& s2 = *ctx.solver(1);
01116 data->setMode(MinimizeMode_t::enumOpt);
01117 MinimizeConstraint* m1 = data->attach(s1, SolverStrategies::opt_unsat_pre);
01118 MinimizeConstraint* m2 = data->attach(s2, SolverStrategies::opt_unsat_pre);
01119 s1.setEnumerationConstraint(m1);
01120 s2.setEnumerationConstraint(m2);
01121 BasicSolve solve(s1);
01122 LitVec gp;
01123 while (m1->integrate(s1) || m1->handleUnsat(s1, true, gp)) {
01124 ValueRep v = solve.solve();
01125 CPPUNIT_ASSERT(v == value_true);
01126 m1->handleModel(s1);
01127 }
01128 data->markOptimal();
01129 m1->relax(s1, true);
01130 m2->relax(s2, true);
01131 solve.reset(s2, s2.searchConfig());
01132 uint32 numModels = 0;
01133 s2.setPref(1, ValueSet::user_value, value_true);
01134 for (;;) {
01135 ValueRep v = m2->integrate(s2) ? solve.solve() : value_false;
01136 if (v == value_true) {
01137 ++numModels;
01138 CPPUNIT_ASSERT(s2.isFalse(lits[0].first));
01139 CPPUNIT_ASSERT(s2.isFalse(lits[1].first));
01140 if (!s2.backtrack()) { break; }
01141 }
01142 else if (v == value_false) {
01143 break;
01144 }
01145 }
01146 CPPUNIT_ASSERT(numModels == 1);
01147 }
01148 void testNegativeLower() {
01149 Literal a = posLit(ctx.addVar(Var_t::atom_var));
01150 Literal b = posLit(ctx.addVar(Var_t::atom_var));
01151 Solver& s = ctx.startAddConstraints();
01152 ctx.addBinary(a, b);
01153 WeightLitVec aMin, bMin;
01154 aMin.push_back( WeightLiteral(a, 1) );
01155 aMin.push_back( WeightLiteral(b, 1) );
01156 bMin.push_back( WeightLiteral(~a, 1) );
01157 data = MinimizeBuilder()
01158 .addRule(aMin)
01159 .addRule(bMin)
01160 .build(ctx);
01161 ctx.endInit();
01162 data->setMode(MinimizeMode_t::optimize);
01163 min = data->attach(s, SolverStrategies::opt_unsat_pre);
01164
01165 LitVec ignore;
01166 while (!min->integrate(*ctx.master()) && min->handleUnsat(s, true, ignore)) { ; }
01167 CPPUNIT_ASSERT(s.assume(~a) && s.propagate());
01168 CPPUNIT_ASSERT(s.assume(b) && s.propagate());
01169 CPPUNIT_ASSERT(min->handleModel(s));
01170 s.undoUntil(0);
01171 while (!min->integrate(*ctx.master()) && min->handleUnsat(s, true, ignore)) { ; }
01172 CPPUNIT_ASSERT(s.assume(a) && s.propagate());
01173 CPPUNIT_ASSERT(s.isFalse(b));
01174 min->handleModel(s);
01175 s.undoUntil(0);
01176 while (!min->integrate(*ctx.master()) && min->handleUnsat(s, true, ignore)) { ; }
01177 CPPUNIT_ASSERT(s.hasConflict());
01178 }
01179 private:
01180 SharedContext ctx;
01181 SharedMinimizeData* data;
01182 MinimizeConstraint* min;
01183 };
01184 CPPUNIT_TEST_SUITE_REGISTRATION(DefaultMinimizeTest);
01185 CPPUNIT_TEST_SUITE_REGISTRATION(UncoreMinimizeTest);
01186 } }