70 void parse(
int& argc,
char* argv[]) {
76 if (_size.
value() == 0U)
77 return static_cast<int>(_height.
value());
79 return static_cast<int>(_size.
value());
83 if (_size.
value() == 0U)
84 return static_cast<int>(_width.
value());
86 return static_cast<int>(_size.
value());
89 int colors(
void)
const {
return static_cast<int>(_colors.
value()); }
98 return _no_monochrome_rectangle.
value();
118 DFA same_or_0_dfa(
int colors);
126 TupleSet same_or_0_tuple_set(
int colors);
130 DFA distinct_except_0_dfa(
int colors);
134 DFA no_monochrome_rectangle_dfa(
int colors);
142 DFA not_all_equal_dfa(
int colors);
188 switch (
opt.same_or_0()) {
189 case SAME_OR_0_REIFIED: {
190 IntVar result(*
this, 0, colors);
197 case SAME_OR_0_TUPLE_SET: {
198 static TupleSet table = same_or_0_tuple_set(colors);
199 IntVar result(*
this, 0, colors);
203 case SAME_OR_0_DFA: {
204 static const DFA automaton = same_or_0_dfa(colors);
205 IntVar result(*
this, 0, colors);
211 return IntVar(*
this, 0, 0);
219 switch (
opt.distinct_except_0()) {
220 case DISTINCT_EXCEPT_0_REIFIED:
221 for (
int i =
v.size();
i--; ) {
223 for (
int j =
i; j--; ) {
224 rel(*
this, viIsZero || (
v[
i] !=
v[j]));
228 case DISTINCT_EXCEPT_0_DFA: {
229 static const DFA automaton = distinct_except_0_dfa(colors);
233 case DISTINCT_EXCEPT_0_COUNT: {
234 static const IntSetArgs counts = distinct_except_0_counts(colors,
std::max(width, height));
245 switch (
opt.not_all_equal()) {
246 case NOT_ALL_EQUAL_NQ: {
250 case NOT_ALL_EQUAL_NAIVE: {
254 for (
int i =
v.size();
i--; )
255 for (
int j =
i; j--; )
256 disequalities <<
expr(*
this,
v[
i] !=
v[j]);
260 case NOT_ALL_EQUAL_REIFIED: {
263 for (
int i = 0;
i <
v.size()-1; ++
i)
264 equalities <<
expr(*
this,
v[
i] ==
v[
i+1]);
268 case NOT_ALL_EQUAL_NVALUES:
272 case NOT_ALL_EQUAL_COUNT:
276 case NOT_ALL_EQUAL_DFA: {
277 static const DFA automaton = not_all_equal_dfa(colors);
288 const int length =
v1.
size();
289 switch (
opt.no_monochrome_rectangle()) {
290 case NO_MONOCHROME_DECOMPOSITION: {
292 for (
int i = 0;
i < length; ++
i) {
295 distinct_except_0(
z);
298 case NO_MONOCHROME_DFA: {
299 static const DFA automaton = no_monochrome_rectangle_dfa(colors);
301 for (
int i = length;
i--; ) {
361 opt(opt0), height(
opt.height()), width(
opt.width()), colors(
opt.colors()),
362 x(*this, height*width, 1, colors),
363 max_color(*this, 1, colors)
366 max(*
this,
x, max_color);
371 if (
opt.model() & MODEL_CORNERS) {
372 for (
int c1 = 0; c1 < width; ++c1) {
373 for (
int c2 = c1+1; c2 < width; ++c2) {
374 for (
int r1 = 0; r1 < height; ++r1) {
375 for (
int r2 = r1+1; r2 < height; ++r2) {
376 not_all_equal(
IntVarArgs() << m(c1,r1) << m(c1,r2) << m(c2,r1) << m(c2,r2));
386 if (
opt.model() & MODEL_ROWS) {
387 for (
int r1 = 0; r1 < height; ++r1) {
388 for (
int r2 = r1+1; r2 < height; ++r2) {
389 no_monochrome_rectangle(m.
row(r1), m.
row(r2));
393 if (
opt.model() & MODEL_COLUMNS) {
394 for (
int c1 = 0; c1 < width; ++c1) {
395 for (
int c2 = c1+1; c2 < width; ++c2) {
396 no_monochrome_rectangle(m.
col(c1), m.
col(c2));
404 if (
opt.symmetry() & SYMMETRY_MATRIX) {
405 for (
int r = 0;
r < height-1; ++
r) {
408 for (
int c = 0;
c < width-1; ++
c) {
414 if (
opt.symmetry() & SYMMETRY_VALUES) {
431 for (
int r = 0;
r < height; ++
r) {
433 for (
int c = 0;
c < width; ++
c) {
434 os << m(
c,
r) <<
" ";
439 os <<
"\tmax color: " << max_color << std::endl;
446 height(s.height), width(s.width), colors(s.colors) {
459 _height(
"height",
"Height of matrix", 8),
460 _width(
"width",
"Width of matrix", 8),
461 _size(
"size",
"If different from 0, used as both width and height", 0),
462 _colors(
"colors",
"Maximum number of colors", 4),
463 _not_all_equal(
"not-all-equal",
"How to implement the not all equals constraint (used in corners model)",
465 _same_or_0(
"same-or-0",
"How to implement the same or 0 constraint (used in the decomposed no monochrome rectangle constraint)",
467 _distinct_except_0(
"distinct-except-0",
"How to implement the distinct except 0 constraint (used in the decomposed no monochrome rectangle constraint)",
469 _no_monochrome_rectangle(
"no-monochrome-rectangle",
"How to implement no monochrome rectangle (used in the rows model)",
478 add(_distinct_except_0);
479 add(_no_monochrome_rectangle);
491 "both",
"Order both rows/columns and values");
498 "both",
"Use both rows and corners model");
501 "matrix",
"Use both rows and columns model");
525 "Use decompositions into same_or_0 and distinct_except_0.");
528 "Use DFA as direct implementation.");
539 Script::run<ColoredMatrix,DFS,ColoredMatrixOptions>(
opt);
541 Script::run<ColoredMatrix,BAB,ColoredMatrixOptions>(
opt);
563 const int start_state = 0;
564 const int not_equal_state = 2*colors+1;
565 const int final_state = 2*colors+2;
567 int n_transitions = colors*colors + 2*colors + 2;
570 int current_transition = 0;
573 for (
int color = 1; color <= colors; ++color) {
574 trans[current_transition++] =
580 for (
int state = 1; state <= colors; ++state) {
581 for (
int color = 1; color <= colors; ++color) {
582 if (color == state) {
583 trans[current_transition++] =
586 trans[current_transition++] =
594 for (
int color = 1; color <= colors; ++color) {
595 trans[current_transition++] =
600 trans[current_transition++] =
604 trans[current_transition++] =
607 int final_states[] = {final_state, -1};
609 DFA result(start_state, trans, final_states,
true);
618 for (
int i = 1;
i <= colors; ++
i) {
619 for (
int j = 1; j <= colors; ++j) {
621 result.add({
i, j,
i});
623 result.add({
i, j, 0});
642 const int nstates = 1 << colors;
643 const int start_state = nstates-1;
647 int current_transition = 0;
649 for (
int state = nstates; state--; ) {
652 for (
int color = 1; color <= colors; ++color) {
653 const int color_bit = (1 << (color-1));
654 if (state & color_bit) {
655 trans[current_transition++] =
662 int* final_states =
new int[nstates+1];
663 final_states[nstates] = -1;
664 for (
int i = nstates;
i--; ) {
668 DFA result(start_state, trans, final_states);
671 delete[] final_states;
692 const int base_states = 1 << colors;
693 const int start_state = base_states-1;
694 const int nstates = base_states + colors*base_states;
697 int current_transition = 0;
699 for (
int state = base_states; state--; ) {
700 for (
int color = 1; color <= colors; ++color) {
701 const int color_bit = (1 << (color-1));
702 const int color_remembered_state = state + color*base_states;
704 trans[current_transition++] =
707 for (
int next_color = 1; next_color <= colors; ++next_color) {
708 if (next_color == color) {
710 if (state & color_bit) {
711 trans[current_transition++] =
715 trans[current_transition++] =
722 assert(current_transition <= nstates*colors+1);
724 int* final_states =
new int[base_states+1];
725 final_states[base_states] = -1;
726 for (
int i = base_states;
i--; ) {
730 DFA result(start_state, trans, final_states);
733 delete[] final_states;
744 for (
int i = 1;
i <= colors; ++
i) {
762 const int nstates = 1 + colors + 1;
763 const int start_state = 0;
764 const int final_state = nstates-1;
767 int current_transition = 0;
770 for (
int color = 1; color <= colors; ++color) {
771 trans[current_transition++] =
DFA::Transition(start_state, color, color);
775 for (
int state = 1; state <= colors; ++state) {
776 for (
int color = 1; color <= colors; ++color) {
777 if (state == color) {
780 trans[current_transition++] =
DFA::Transition(state, color, final_state);
786 for (
int color = 1; color <= colors; ++color) {
787 trans[current_transition++] =
DFA::Transition(final_state, color, final_state);
792 int final_states[] = {final_state, -1};
794 DFA result(start_state, trans, final_states);