Generated on Tue Feb 11 2025 17:33:26 for Gecode by doxygen 1.12.0
nogoods.cpp
Go to the documentation of this file.
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Christian Schulte <schulte@gecode.org>
5 *
6 * Contributing authors:
7 * Guido Tack <tack@gecode.org>
8 *
9 * Copyright:
10 * Christian Schulte, 2013
11 * Guido Tack, 2004
12 *
13 * This file is part of Gecode, the generic constraint
14 * development environment:
15 * http://www.gecode.org
16 *
17 * Permission is hereby granted, free of charge, to any person obtaining
18 * a copy of this software and associated documentation files (the
19 * "Software"), to deal in the Software without restriction, including
20 * without limitation the rights to use, copy, modify, merge, publish,
21 * distribute, sublicense, and/or sell copies of the Software, and to
22 * permit persons to whom the Software is furnished to do so, subject to
23 * the following conditions:
24 *
25 * The above copyright notice and this permission notice shall be
26 * included in all copies or substantial portions of the Software.
27 *
28 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
29 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
30 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
31 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
32 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
33 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
34 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
35 *
36 */
37
38#include <gecode/minimodel.hh>
39#include <gecode/search.hh>
40
41#include "test/test.hh"
42
43namespace Test {
44
46 namespace NoGoods {
47
48 using namespace Gecode;
49
51 void dummy(Space&) {
52 }
53
55 class Queens : public Space {
56 public:
58 const static int n = 18;
62 Queens(IntValBranch ivb, bool assign, bool null)
63 : q(*this,n,0,n-1) {
64 distinct(*this, IntArgs::create(n,0,1), q, IPL_VAL);
65 distinct(*this, IntArgs::create(n,0,-1), q, IPL_VAL);
66 distinct(*this, q, IPL_VAL);
67 if (assign) {
68 IntVar x(*this,0,1); Gecode::assign(*this, x, INT_ASSIGN_MIN());
69 }
70 {
71 IntVarArgs q1(n/2), q2(n/2);
72 for (int i=0; i<n/2; i++) {
73 q1[i] = q[i]; q2[i] = q[n/2 + i];
74 }
75 branch(*this, q1, INT_VAR_NONE(), ivb);
76 if (null)
77 branch(*this, &dummy);
78 branch(*this, q2, INT_VAR_NONE(), ivb);
79 }
80 if (assign) {
81 IntVar x(*this,0,1); Gecode::assign(*this, x, INT_ASSIGN_MIN());
82 }
83 }
85 Queens(Queens& s) : Space(s) {
86 q.update(*this, s.q);
87 }
89 virtual Space* copy(void) {
90 return new Queens(*this);
91 }
93 bool same(const Queens& s) const {
94 for (int i=0; i<q.size(); i++)
95 if (q[i].val() != s.q[i].val())
96 return false;
97 return true;
98 }
100 static unsigned int nodeinc(void) {
101 return 500;
102 }
104 static std::string name(void) {
105 return "Queens";
106 }
108 static std::string val(IntValBranch ivb) {
109 switch (ivb.select()) {
110 case IntValBranch::SEL_MIN: return "INT_VAL_MIN";
111 case IntValBranch::SEL_MAX: return "INT_VAL_MAX";
112 case IntValBranch::SEL_SPLIT_MIN: return "INT_VAL_SPLIT_MIN";
113 case IntValBranch::SEL_SPLIT_MAX: return "INT_VAL_SPLIT_MAX";
114 case IntValBranch::SEL_VALUES_MIN: return "INT_VALUES_MIN";
115 case IntValBranch::SEL_VALUES_MAX: return "INT_VALUES_MAX";
116 default: GECODE_NEVER;
117 }
118 return "";
119 }
120 };
121
122#ifdef GECODE_HAS_SET_VARS
124 class Hamming : public Space {
125 private:
127 static const int size = 16;
129 static const int distance = 4;
131 static const int bits = 8;
133 SetVarArray x;
134 public:
136 Hamming(SetValBranch svb, bool assign, bool null) :
137 x(*this,size,IntSet::empty,1,bits) {
138 SetVarArgs cx(x.size());
139 for (int i=x.size(); i--;)
140 cx[i] = expr(*this, -x[i]);
141
142 for (int i=0; i<x.size(); i++)
143 for (int j=i+1; j<x.size(); j++)
144 rel(*this,
145 cardinality(x[j] & cx[i]) +
146 cardinality(x[i] & cx[j]) >= distance);
147
148 if (assign) {
149 IntVar x(*this,0,1); Gecode::assign(*this, x, INT_ASSIGN_MIN());
150 }
151 {
152 SetVarArgs x1(size/2), x2(size/2);
153 for (int i=0; i<size/2; i++) {
154 x1[i] = x[i]; x2[i] = x[size/2 + i];
155 }
156 branch(*this, x1, SET_VAR_NONE(), svb);
157 if (null)
158 branch(*this, &dummy);
159 branch(*this, x2, SET_VAR_NONE(), svb);
160 }
161 if (assign) {
162 IntVar x(*this,0,1); Gecode::assign(*this, x, INT_ASSIGN_MIN());
163 }
164 }
167 x.update(*this, s.x);
168 }
170 virtual Space* copy(void) {
171 return new Hamming(*this);
172 }
174 bool same(const Hamming& s) const {
175 for (int i=0; i<x.size(); i++) {
176 SetVarGlbRanges a(x[i]), b(s.x[i]);
177 if (!Iter::Ranges::equal(a,b))
178 return false;
179 }
180 return true;
181 }
183 static unsigned int nodeinc(void) {
184 return 35;
185 }
187 static std::string name(void) {
188 return "Hamming";
189 }
191 static std::string val(SetValBranch svb) {
192 switch (svb.select()) {
193 case SetValBranch::SEL_MIN_INC: return "SET_VAL_MIN_INC";
194 case SetValBranch::SEL_MAX_INC: return "SET_VAL_MAX_INC";
195 case SetValBranch::SEL_MIN_EXC: return "SET_VAL_MIN_EXC";
196 case SetValBranch::SEL_MAX_EXC: return "SET_VAL_MAX_EXC";
197 default: GECODE_NEVER;
198 }
199 return "";
200 }
201 };
202#endif
203
205 template<class Model, class ValBranch>
206 class NoGoods : public Base {
207 protected:
211 unsigned int t;
213 bool a;
215 bool n;
216 public:
218 static std::string str(unsigned int i) {
219 std::stringstream s;
220 s << i;
221 return s.str();
222 }
224 NoGoods(ValBranch vb0, unsigned int t0, bool a0, bool n0)
225 : Base("NoGoods::"+Model::name()+"::"+Model::val(vb0)+"::"+str(t0)+
226 "::"+(a0 ? "+" : "-")+"::"+(n0 ? "+" : "-")),
227 vb(vb0), t(t0), a(a0), n(n0) {}
229 virtual bool run(void) {
230 Model* m = new Model(vb,a,n);
231 // Solution without no-goods
232 Model* s_plain = dfs(m);
233 // Stop and re-start for a while to collect no-goods
234 {
235 Search::NodeStop ns(Model::nodeinc());
237 o.stop = &ns;
238 o.threads = t;
239 o.nogoods_limit = 256U;
241 while (true) {
242 Model* s = static_cast<Model*>(e->next());
243 delete s;
244 if (!e->stopped())
245 break;
246 // Add no-goods
247 e->nogoods().post(*m);
248 ns.limit(ns.limit()+Model::nodeinc());
249 }
250 delete e;
251 }
252 // Compare whether the a or the same solution is found with no-goods
253 Model* s_nogoods = dfs(m);
254
255 bool ok = ((s_nogoods != NULL) &&
256 ((t != 1) || s_plain->same(*s_nogoods)));
257
258 delete m;
259 delete s_nogoods;
260 delete s_plain;
261
262 return ok;
263 }
264 };
265
266
268 class Create {
269 public:
271 Create(void) {
272 bool a = false;
273 do {
274 bool n = false;
275 do {
276 for (unsigned int t = 1; t<=4; t++) {
283#ifdef GECODE_HAS_SET_VARS
288#endif
289 }
290 n = !n;
291 } while (n);
292 a = !a;
293 } while (a);
294 }
295 };
296
298 }
299
300}
301
302// STATISTICS: test-search
struct Gecode::@603::NNF::@65::@66 b
For binary nodes (and, or, eqv)
NodeType t
Type of node.
int n
Number of negative literals for node type.
struct Gecode::@603::NNF::@65::@67 a
For atomic nodes.
Node * x
Pointer to corresponding Boolean expression node.
static IntArgs create(int n, int start, int inc=1)
Allocate array with n elements such that for all .
Definition array.hpp:76
Integer sets.
Definition int.hh:174
Which values to select for branching first.
Definition int.hh:4854
@ SEL_VALUES_MIN
Select all values starting from smallest.
Definition int.hh:4867
@ SEL_SPLIT_MAX
Select values greater than mean of smallest and largest value.
Definition int.hh:4863
@ SEL_MIN
Select smallest value.
Definition int.hh:4858
@ SEL_MAX
Select largest value.
Definition int.hh:4860
@ SEL_VALUES_MAX
Select all values starting from largest.
Definition int.hh:4868
@ SEL_SPLIT_MIN
Select values not greater than mean of smallest and largest value.
Definition int.hh:4862
Select select(void) const
Return selection strategy.
Definition val.hpp:49
Passing integer variables.
Definition int.hh:656
Integer variable array.
Definition int.hh:763
Integer variables.
Definition int.hh:371
No-goods recorded from restarts.
Definition core.hpp:1588
virtual void post(Space &home) const
Post no-goods.
Definition core.cpp:82
unsigned long int n
Number of no-goods.
Definition core.hpp:1591
Search engine implementation interface
Definition search.hh:899
virtual Space * next(void)=0
Return next solution (NULL, if none exists or search has been stopped)
virtual bool stopped(void) const =0
Check whether engine has been stopped.
virtual NoGoods & nogoods(void)
Return no-goods (the no-goods are empty)
Definition engine.cpp:48
Stop-object based on number of nodes
Definition search.hh:829
unsigned long int limit(void) const
Return current limit.
Definition stop.hpp:55
Search engine options
Definition search.hh:746
Stop * stop
Stop object for stopping search.
Definition search.hh:765
unsigned int nogoods_limit
Depth limit for extraction of no-goods.
Definition search.hh:763
double threads
Number of threads to use.
Definition search.hh:751
Which values to select for branching first.
Definition set.hh:1447
@ SEL_MAX_INC
Include largest element.
Definition set.hh:1455
@ SEL_MIN_EXC
Exclude smallest element.
Definition set.hh:1452
@ SEL_MIN_INC
Include smallest element.
Definition set.hh:1451
@ SEL_MAX_EXC
Exclude largest element.
Definition set.hh:1456
Return selection strategy Select select(void) const
Definition val.hpp:49
Passing set variables.
Definition set.hh:488
Set variable array
Definition set.hh:570
Iterator for the greatest lower bound ranges of a set variable.
Definition set.hh:270
Computation spaces.
Definition core.hpp:1742
Value branching information.
Definition val.hpp:41
int size(void) const
Return size of array (number of elements)
Definition array.hpp:926
void update(Space &home, VarArray< Var > &a)
Update array to be a clone of array a.
Definition array.hpp:1013
Base class for all tests to be run
Definition test.hh:103
const std::string & name(void) const
Return name of test.
Definition test.hpp:50
Help class to create and register tests.
Definition nogoods.cpp:268
Create(void)
Perform creation and registration.
Definition nogoods.cpp:271
Example for testing set no-goods.
Definition nogoods.cpp:124
Hamming(Hamming &s)
Constructor for copying s.
Definition nogoods.cpp:166
static unsigned int nodeinc(void)
Return increment for node stop.
Definition nogoods.cpp:183
bool same(const Hamming &s) const
Check whether two solutions are the same.
Definition nogoods.cpp:174
static std::string name(void)
Return name.
Definition nogoods.cpp:187
virtual Space * copy(void)
Copy during cloning.
Definition nogoods.cpp:170
static std::string val(SetValBranch svb)
Return name for branching.
Definition nogoods.cpp:191
Hamming(SetValBranch svb, bool assign, bool null)
Actual model.
Definition nogoods.cpp:136
static std::string str(unsigned int i)
Map unsigned integer to string.
Definition nogoods.cpp:218
bool n
Whether to also create branchers without no-good literals.
Definition nogoods.cpp:215
unsigned int t
Number of threads to use.
Definition nogoods.cpp:211
virtual bool run(void)
Run test.
Definition nogoods.cpp:229
NoGoods(ValBranch vb0, unsigned int t0, bool a0, bool n0)
Initialize test.
Definition nogoods.cpp:224
bool a
Whether to also assign some variables.
Definition nogoods.cpp:213
ValBranch vb
How to branch.
Definition nogoods.cpp:209
Example for testing integer no-goods.
Definition nogoods.cpp:55
static const int n
Number of queens (must be even)
Definition nogoods.cpp:58
static std::string name(void)
Return name.
Definition nogoods.cpp:104
virtual Space * copy(void)
Perform copying during cloning.
Definition nogoods.cpp:89
Queens(Queens &s)
Constructor for cloning s.
Definition nogoods.cpp:85
static unsigned int nodeinc(void)
Return increment for node stop.
Definition nogoods.cpp:100
bool same(const Queens &s) const
Check whether two solutions are the same.
Definition nogoods.cpp:93
IntVarArray q
Position of queens on boards.
Definition nogoods.cpp:60
Queens(IntValBranch ivb, bool assign, bool null)
The actual problem.
Definition nogoods.cpp:62
static std::string val(IntValBranch ivb)
Return name for branching.
Definition nogoods.cpp:108
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
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
void rel(Home home, FloatVar x0, FloatRelType frt, FloatVar x1)
Post propagator for .
Definition rel.cpp:68
@ IPL_VAL
Value propagation.
Definition int.hh:977
bool equal(I &i, J &j)
Check whether range iterators i and j are equal.
Engine * dfsengine(Space *s, const Options &o)
Create depth-first engine.
Definition dfs.cpp:45
Gecode toplevel namespace
IntValBranch INT_VAL_SPLIT_MIN(void)
Select values not greater than mean of smallest and largest value.
Definition val.hpp:75
IntValBranch INT_VALUES_MAX(void)
Try all values starting from largest.
Definition val.hpp:105
Select first unassigned variable SetVarBranch SET_VAR_NONE(void)
Definition var.hpp:96
IntVar expr(Home home, const LinIntExpr &e, const IntPropLevels &ipls=IntPropLevels::def)
Post linear expression and return its value.
Definition int-expr.cpp:915
void distinct(Home home, const IntVarArgs &x, IntPropLevel ipl=IPL_DEF)
Post propagator for for all .
Definition distinct.cpp:46
IntVarBranch INT_VAR_NONE(void)
Select first unassigned variable.
Definition var.hpp:96
IntValBranch INT_VALUES_MIN(void)
Try all values starting from smallest.
Definition val.hpp:100
IntValBranch INT_VAL_MAX(void)
Select largest value.
Definition val.hpp:65
Include largest element SetValBranch SET_VAL_MAX_INC(void)
Definition val.hpp:75
IntValBranch INT_VAL_SPLIT_MAX(void)
Select values greater than mean of smallest and largest value.
Definition val.hpp:80
IntValBranch INT_VAL_MIN(void)
Select smallest value.
Definition val.hpp:55
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
IntAssign INT_ASSIGN_MIN(void)
Select smallest value.
Definition assign.hpp:55
Include smallest element SetValBranch SET_VAL_MIN_INC(void)
Definition val.hpp:55
Exclude largest element SetValBranch SET_VAL_MAX_EXC(void)
Definition val.hpp:80
LinIntExpr cardinality(const SetExpr &)
Cardinality of set expression.
Definition set-expr.cpp:817
Post propagator for SetVar x
Definition set.hh:767
Exclude smallest element SetValBranch SET_VAL_MIN_EXC(void)
Definition val.hpp:60
void dummy(Space &)
A dummy function for branching.
Definition nogoods.cpp:51
General test support.
Definition afc.cpp:39
#define GECODE_NEVER
Assert that this command is never executed.
Definition macros.hpp:56