nogoods.cpp
Go to the documentation of this file.
/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
/*
* Main authors:
* Christian Schulte <schulte@gecode.org>
*
* Contributing authors:
* Guido Tack <tack@gecode.org>
*
* Copyright:
* Christian Schulte, 2013
* Guido Tack, 2004
*
* This file is part of Gecode, the generic constraint
* development environment:
* http://www.gecode.org
*
* Permission is hereby granted, free of charge, to any person obtaining
* a copy of this software and associated documentation files (the
* "Software"), to deal in the Software without restriction, including
* without limitation the rights to use, copy, modify, merge, publish,
* distribute, sublicense, and/or sell copies of the Software, and to
* permit persons to whom the Software is furnished to do so, subject to
* the following conditions:
*
* The above copyright notice and this permission notice shall be
* included in all copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
* EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
* MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
* NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
* LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
* OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
* WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*
*/
#include <gecode/minimodel.hh>
#include <gecode/search.hh>
#include "test/test.hh"
namespace Test {
namespace NoGoods {
using namespace Gecode;
void dummy(Space&) {
}
class Queens : public Space {
public:
const static int n = 18;
IntVarArray q;
Queens(IntValBranch ivb, bool assign, bool null)
: q(*this,n,0,n-1) {
distinct(*this, IntArgs::create(n,0,1), q, IPL_VAL);
distinct(*this, IntArgs::create(n,0,-1), q, IPL_VAL);
distinct(*this, q, IPL_VAL);
if (assign) {
IntVar x(*this,0,1); Gecode::assign(*this, x, INT_ASSIGN_MIN());
}
{
IntVarArgs q1(n/2), q2(n/2);
for (int i=0; i<n/2; i++) {
q1[i] = q[i]; q2[i] = q[n/2 + i];
}
branch(*this, q1, INT_VAR_NONE(), ivb);
if (null)
branch(*this, &dummy);
branch(*this, q2, INT_VAR_NONE(), ivb);
}
if (assign) {
IntVar x(*this,0,1); Gecode::assign(*this, x, INT_ASSIGN_MIN());
}
}
Queens(Queens& s) : Space(s) {
q.update(*this, s.q);
}
virtual Space* copy(void) {
return new Queens(*this);
}
bool same(const Queens& s) const {
for (int i=0; i<q.size(); i++)
if (q[i].val() != s.q[i].val())
return false;
return true;
}
static unsigned int nodeinc(void) {
return 500;
}
static std::string name(void) {
return "Queens";
}
static std::string val(IntValBranch ivb) {
switch (ivb.select()) {
case IntValBranch::SEL_MIN: return "INT_VAL_MIN";
case IntValBranch::SEL_MAX: return "INT_VAL_MAX";
case IntValBranch::SEL_SPLIT_MIN: return "INT_VAL_SPLIT_MIN";
case IntValBranch::SEL_SPLIT_MAX: return "INT_VAL_SPLIT_MAX";
case IntValBranch::SEL_VALUES_MIN: return "INT_VALUES_MIN";
case IntValBranch::SEL_VALUES_MAX: return "INT_VALUES_MAX";
default: GECODE_NEVER;
}
return "";
}
};
#ifdef GECODE_HAS_SET_VARS
class Hamming : public Space {
private:
static const int size = 16;
static const int distance = 4;
static const int bits = 8;
SetVarArray x;
public:
Hamming(SetValBranch svb, bool assign, bool null) :
x(*this,size,IntSet::empty,1,bits) {
SetVarArgs cx(x.size());
for (int i=x.size(); i--;)
cx[i] = expr(*this, -x[i]);
for (int i=0; i<x.size(); i++)
for (int j=i+1; j<x.size(); j++)
rel(*this,
cardinality(x[j] & cx[i]) +
cardinality(x[i] & cx[j]) >= distance);
if (assign) {
IntVar x(*this,0,1); Gecode::assign(*this, x, INT_ASSIGN_MIN());
}
{
SetVarArgs x1(size/2), x2(size/2);
for (int i=0; i<size/2; i++) {
x1[i] = x[i]; x2[i] = x[size/2 + i];
}
branch(*this, x1, SET_VAR_NONE(), svb);
if (null)
branch(*this, &dummy);
branch(*this, x2, SET_VAR_NONE(), svb);
}
if (assign) {
IntVar x(*this,0,1); Gecode::assign(*this, x, INT_ASSIGN_MIN());
}
}
Hamming(Hamming& s) : Space(s) {
x.update(*this, s.x);
}
virtual Space* copy(void) {
return new Hamming(*this);
}
bool same(const Hamming& s) const {
for (int i=0; i<x.size(); i++) {
SetVarGlbRanges a(x[i]), b(s.x[i]);
if (!Iter::Ranges::equal(a,b))
return false;
}
return true;
}
static unsigned int nodeinc(void) {
return 35;
}
static std::string name(void) {
return "Hamming";
}
static std::string val(SetValBranch svb) {
switch (svb.select()) {
case SetValBranch::SEL_MIN_INC: return "SET_VAL_MIN_INC";
case SetValBranch::SEL_MAX_INC: return "SET_VAL_MAX_INC";
case SetValBranch::SEL_MIN_EXC: return "SET_VAL_MIN_EXC";
case SetValBranch::SEL_MAX_EXC: return "SET_VAL_MAX_EXC";
default: GECODE_NEVER;
}
return "";
}
};
#endif
template<class Model, class ValBranch>
class NoGoods : public Base {
protected:
ValBranch vb;
unsigned int t;
bool a;
bool n;
public:
static std::string str(unsigned int i) {
std::stringstream s;
s << i;
return s.str();
}
NoGoods(ValBranch vb0, unsigned int t0, bool a0, bool n0)
: Base("NoGoods::"+Model::name()+"::"+Model::val(vb0)+"::"+str(t0)+
"::"+(a0 ? "+" : "-")+"::"+(n0 ? "+" : "-")),
vb(vb0), t(t0), a(a0), n(n0) {}
virtual bool run(void) {
Model* m = new Model(vb,a,n);
// Solution without no-goods
Model* s_plain = dfs(m);
// Stop and re-start for a while to collect no-goods
{
Search::NodeStop ns(Model::nodeinc());
Search::Options o;
o.stop = &ns;
o.threads = t;
o.nogoods_limit = 256U;
Search::Engine* e = Search::dfsengine(m,o);
while (true) {
Model* s = static_cast<Model*>(e->next());
delete s;
if (!e->stopped())
break;
// Add no-goods
e->nogoods().post(*m);
ns.limit(ns.limit()+Model::nodeinc());
}
delete e;
}
// Compare whether the a or the same solution is found with no-goods
Model* s_nogoods = dfs(m);
bool ok = ((s_nogoods != NULL) &&
((t != 1) || s_plain->same(*s_nogoods)));
delete m;
delete s_nogoods;
delete s_plain;
return ok;
}
};
class Create {
public:
Create(void) {
bool a = false;
do {
bool n = false;
do {
for (unsigned int t = 1; t<=4; t++) {
(void) new NoGoods<Queens,IntValBranch>(INT_VAL_MIN(),t,a,n);
(void) new NoGoods<Queens,IntValBranch>(INT_VAL_MAX(),t,a,n);
(void) new NoGoods<Queens,IntValBranch>(INT_VAL_SPLIT_MIN(),t,a,n);
(void) new NoGoods<Queens,IntValBranch>(INT_VAL_SPLIT_MAX(),t,a,n);
(void) new NoGoods<Queens,IntValBranch>(INT_VALUES_MIN(),t,a,n);
(void) new NoGoods<Queens,IntValBranch>(INT_VALUES_MAX(),t,a,n);
#ifdef GECODE_HAS_SET_VARS
(void) new NoGoods<Hamming,SetValBranch>(SET_VAL_MIN_INC(),t,a,n);
(void) new NoGoods<Hamming,SetValBranch>(SET_VAL_MIN_EXC(),t,a,n);
(void) new NoGoods<Hamming,SetValBranch>(SET_VAL_MAX_INC(),t,a,n);
(void) new NoGoods<Hamming,SetValBranch>(SET_VAL_MAX_EXC(),t,a,n);
#endif
}
n = !n;
} while (n);
a = !a;
} while (a);
}
};
Create c;
}
}
// STATISTICS: test-search
Gecode::ArgArrayBase::size
int size(void) const
Return size of array (number of elements).
Definition array.hpp:1607
Gecode::IntArgs::create
static IntArgs create(int n, int start, int inc=1)
Allocate array with n elements such that for all .
Definition array.hpp:76
Gecode::IntSet
Integer sets.
Definition int.hh:174
Gecode::IntValBranch
Which values to select for branching first.
Definition int.hh:4854
Gecode::IntValBranch::SEL_VALUES_MIN
@ SEL_VALUES_MIN
Select all values starting from smallest.
Definition int.hh:4867
Gecode::IntValBranch::SEL_SPLIT_MAX
@ SEL_SPLIT_MAX
Select values greater than mean of smallest and largest value.
Definition int.hh:4863
Gecode::IntValBranch::SEL_MIN
@ SEL_MIN
Select smallest value.
Definition int.hh:4858
Gecode::IntValBranch::SEL_MAX
@ SEL_MAX
Select largest value.
Definition int.hh:4860
Gecode::IntValBranch::SEL_VALUES_MAX
@ SEL_VALUES_MAX
Select all values starting from largest.
Definition int.hh:4868
Gecode::IntValBranch::SEL_SPLIT_MIN
@ SEL_SPLIT_MIN
Select values not greater than mean of smallest and largest value.
Definition int.hh:4862
Gecode::IntValBranch::select
Select select(void) const
Return selection strategy.
Definition val.hpp:49
Gecode::IntVarArgs
Passing integer variables.
Definition int.hh:656
Gecode::IntVarArray
Integer variable array.
Definition int.hh:763
Gecode::IntVar
Integer variables.
Definition int.hh:371
Gecode::NoGoods
No-goods recorded from restarts.
Definition core.hpp:1588
Gecode::NoGoods::post
virtual void post(Space &home) const
Post no-goods.
Definition core.cpp:82
Gecode::Search::Engine
Search engine implementation interface
Definition search.hh:899
Gecode::Search::Engine::next
virtual Space * next(void)=0
Return next solution (NULL, if none exists or search has been stopped).
Gecode::Search::Engine::stopped
virtual bool stopped(void) const =0
Check whether engine has been stopped.
Gecode::Search::Engine::nogoods
virtual NoGoods & nogoods(void)
Return no-goods (the no-goods are empty).
Definition engine.cpp:48
Gecode::Search::NodeStop
Stop-object based on number of nodes
Definition search.hh:829
Gecode::Search::NodeStop::limit
unsigned long int limit(void) const
Return current limit.
Definition stop.hpp:55
Gecode::Search::Options
Search engine options
Definition search.hh:746
Gecode::Search::Options::stop
Stop * stop
Stop object for stopping search.
Definition search.hh:765
Gecode::Search::Options::nogoods_limit
unsigned int nogoods_limit
Depth limit for extraction of no-goods.
Definition search.hh:763
Gecode::Search::Options::threads
double threads
Number of threads to use.
Definition search.hh:751
Gecode::SetValBranch
Which values to select for branching first.
Definition set.hh:1447
Gecode::SetValBranch::SEL_MAX_INC
@ SEL_MAX_INC
Include largest element.
Definition set.hh:1455
Gecode::SetValBranch::SEL_MIN_EXC
@ SEL_MIN_EXC
Exclude smallest element.
Definition set.hh:1452
Gecode::SetValBranch::SEL_MIN_INC
@ SEL_MIN_INC
Include smallest element.
Definition set.hh:1451
Gecode::SetValBranch::SEL_MAX_EXC
@ SEL_MAX_EXC
Exclude largest element.
Definition set.hh:1456
Gecode::SetValBranch::select
Select select(void) const
Return selection strategy.
Definition val.hpp:49
Gecode::SetVarArgs
Passing set variables.
Definition set.hh:488
Gecode::SetVarArray
Set variable array
Definition set.hh:570
Gecode::SetVarGlbRanges
Iterator for the greatest lower bound ranges of a set variable.
Definition set.hh:270
Gecode::Space
Computation spaces.
Definition core.hpp:1742
Gecode::ValBranch
Value branching information.
Definition val.hpp:41
Test::Base::Base
Base(const std::string &s)
Create and register test with name s.
Definition test.cpp:59
Test::Base::name
const std::string & name(void) const
Return name of test.
Definition test.hpp:50
Test::NoGoods::Create
Help class to create and register tests.
Definition nogoods.cpp:268
Test::NoGoods::Create::Create
Create(void)
Perform creation and registration.
Definition nogoods.cpp:271
Test::NoGoods::Hamming::Hamming
Hamming(Hamming &s)
Constructor for copying s.
Definition nogoods.cpp:166
Test::NoGoods::Hamming::nodeinc
static unsigned int nodeinc(void)
Return increment for node stop.
Definition nogoods.cpp:183
Test::NoGoods::Hamming::same
bool same(const Hamming &s) const
Check whether two solutions are the same.
Definition nogoods.cpp:174
Test::NoGoods::Hamming::name
static std::string name(void)
Return name.
Definition nogoods.cpp:187
Test::NoGoods::Hamming::copy
virtual Space * copy(void)
Copy during cloning.
Definition nogoods.cpp:170
Test::NoGoods::Hamming::val
static std::string val(SetValBranch svb)
Return name for branching.
Definition nogoods.cpp:191
Test::NoGoods::Hamming::Hamming
Hamming(SetValBranch svb, bool assign, bool null)
Actual model.
Definition nogoods.cpp:136
Test::NoGoods::NoGoods::str
static std::string str(unsigned int i)
Map unsigned integer to string.
Definition nogoods.cpp:218
Test::NoGoods::NoGoods::n
bool n
Whether to also create branchers without no-good literals.
Definition nogoods.cpp:215
Test::NoGoods::NoGoods::t
unsigned int t
Number of threads to use.
Definition nogoods.cpp:211
Test::NoGoods::NoGoods::run
virtual bool run(void)
Run test.
Definition nogoods.cpp:229
Test::NoGoods::NoGoods::NoGoods
NoGoods(ValBranch vb0, unsigned int t0, bool a0, bool n0)
Initialize test.
Definition nogoods.cpp:224
Test::NoGoods::NoGoods::a
bool a
Whether to also assign some variables.
Definition nogoods.cpp:213
Test::NoGoods::NoGoods::vb
ValBranch vb
How to branch.
Definition nogoods.cpp:209
Test::NoGoods::Queens::n
static const int n
Number of queens (must be even).
Definition nogoods.cpp:58
Test::NoGoods::Queens::name
static std::string name(void)
Return name.
Definition nogoods.cpp:104
Test::NoGoods::Queens::copy
virtual Space * copy(void)
Perform copying during cloning.
Definition nogoods.cpp:89
Test::NoGoods::Queens::Queens
Queens(Queens &s)
Constructor for cloning s.
Definition nogoods.cpp:85
Test::NoGoods::Queens::nodeinc
static unsigned int nodeinc(void)
Return increment for node stop.
Definition nogoods.cpp:100
Test::NoGoods::Queens::same
bool same(const Queens &s) const
Check whether two solutions are the same.
Definition nogoods.cpp:93
Test::NoGoods::Queens::q
IntVarArray q
Position of queens on boards.
Definition nogoods.cpp:60
Test::NoGoods::Queens::Queens
Queens(IntValBranch ivb, bool assign, bool null)
The actual problem.
Definition nogoods.cpp:62
Test::NoGoods::Queens::val
static std::string val(IntValBranch ivb)
Return name for branching.
Definition nogoods.cpp:108
Gecode::assign
void assign(Home home, const FloatVarArgs &x, FloatVarBranch vars, FloatAssign vals, FloatBranchFilter bf=nullptr, FloatVarValPrint vvp=nullptr)
Assign all x with variable selection vars and value selection vals.
Definition branch.cpp:111
Gecode::branch
void branch(Home home, const FloatVarArgs &x, FloatVarBranch vars, FloatValBranch vals, FloatBranchFilter bf=nullptr, FloatVarValPrint vvp=nullptr)
Branch over x with variable selection vars and value selection vals.
Definition branch.cpp:39
Gecode::rel
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVar x1)
Post propagator for .
Definition rel.cpp:68
Gecode::IPL_VAL
@ IPL_VAL
Value propagation.
Definition int.hh:977
Gecode::Space::Space
Space(void)
Default constructor.
Definition core.cpp:115
minimodel.hh
Gecode::Iter::Ranges::equal
bool equal(I &i, J &j)
Check whether range iterators i and j are equal.
Definition ranges-operations.hpp:84
Gecode::Search::dfsengine
Engine * dfsengine(Space *s, const Options &o)
Create depth-first engine.
Definition dfs.cpp:45
Gecode
Gecode toplevel namespace
Gecode::INT_VAL_SPLIT_MIN
IntValBranch INT_VAL_SPLIT_MIN(void)
Select values not greater than mean of smallest and largest value.
Definition val.hpp:75
Gecode::INT_VALUES_MAX
IntValBranch INT_VALUES_MAX(void)
Try all values starting from largest.
Definition val.hpp:105
Gecode::SET_VAR_NONE
SetVarBranch SET_VAR_NONE(void)
Select first unassigned variable.
Definition var.hpp:96
Gecode::expr
IntVar expr(Home home, const LinIntExpr &e, const IntPropLevels &ipls=IntPropLevels::def)
Post linear expression and return its value.
Definition int-expr.cpp:915
Gecode::distinct
void distinct(Home home, const IntVarArgs &x, IntPropLevel ipl=IPL_DEF)
Post propagator for for all .
Definition distinct.cpp:46
Gecode::INT_VAR_NONE
IntVarBranch INT_VAR_NONE(void)
Select first unassigned variable.
Definition var.hpp:96
Gecode::INT_VALUES_MIN
IntValBranch INT_VALUES_MIN(void)
Try all values starting from smallest.
Definition val.hpp:100
Gecode::INT_VAL_MAX
IntValBranch INT_VAL_MAX(void)
Select largest value.
Definition val.hpp:65
Gecode::SET_VAL_MAX_INC
SetValBranch SET_VAL_MAX_INC(void)
Include largest element.
Definition val.hpp:75
Gecode::INT_VAL_SPLIT_MAX
IntValBranch INT_VAL_SPLIT_MAX(void)
Select values greater than mean of smallest and largest value.
Definition val.hpp:80
Gecode::INT_VAL_MIN
IntValBranch INT_VAL_MIN(void)
Select smallest value.
Definition val.hpp:55
Gecode::dfs
T * dfs(T *s, const Search::Options &o=Search::Options::def)
Invoke depth-first search engine for subclass T of space s with options o.
Definition dfs.hpp:73
Gecode::INT_ASSIGN_MIN
IntAssign INT_ASSIGN_MIN(void)
Select smallest value.
Definition assign.hpp:55
Gecode::SET_VAL_MIN_INC
SetValBranch SET_VAL_MIN_INC(void)
Include smallest element.
Definition val.hpp:55
Gecode::SET_VAL_MAX_EXC
SetValBranch SET_VAL_MAX_EXC(void)
Exclude largest element.
Definition val.hpp:80
Gecode::cardinality
LinIntExpr cardinality(const SetExpr &)
Cardinality of set expression.
Definition set-expr.cpp:817
Gecode::SET_VAL_MIN_EXC
SetValBranch SET_VAL_MIN_EXC(void)
Exclude smallest element.
Definition val.hpp:60
Test::NoGoods::c
Create c
Definition nogoods.cpp:297
Test::NoGoods::dummy
void dummy(Space &)
A dummy function for branching.
Definition nogoods.cpp:51
Test
General test support.
Definition afc.cpp:39
search.hh
GECODE_NEVER
#define GECODE_NEVER
Assert that this command is never executed.
Definition macros.hpp:56
test.hh