1 /* 2 * Lex.java 3 * This file is part of JaCoP. 4 * <p> 5 * JaCoP is a Java Constraint Programming solver. 6 * <p> 7 * Copyright (C) 2000-2010 Krzysztof Kuchcinski and Radoslaw Szymanek 8 * <p> 9 * This program is free software: you can redistribute it and/or modify 10 * it under the terms of the GNU Affero General Public License as published by 11 * the Free Software Foundation, either version 3 of the License, or 12 * (at your option) any later version. 13 * <p> 14 * This program is distributed in the hope that it will be useful, 15 * but WITHOUT ANY WARRANTY; without even the implied warranty of 16 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 17 * GNU Affero General Public License for more details. 18 * <p> 19 * Notwithstanding any other provision of this License, the copyright 20 * owners of this work supplement the terms of this License with terms 21 * prohibiting misrepresentation of the origin of this work and requiring 22 * that modified versions of this work be marked in reasonable ways as 23 * different from the original version. This supplement of the license 24 * terms is in accordance with Section 7 of GNU Affero General Public 25 * License version 3. 26 * <p> 27 * You should have received a copy of the GNU Affero General Public License 28 * along with this program. If not, see <http://www.gnu.org/licenses/>. 29 */ 30 31 package org.jacop.constraints; 32 33 import org.jacop.constraints.regular.Regular; 34 import org.jacop.core.BooleanVar; 35 import org.jacop.core.IntVar; 36 import org.jacop.core.IntervalDomain; 37 import org.jacop.core.Store; 38 import org.jacop.util.fsm.FSM; 39 import org.jacop.util.fsm.FSMState; 40 import org.jacop.util.fsm.FSMTransition; 41 42 import java.util.ArrayList; 43 import java.util.List; 44 45 /** 46 * It constructs a Lex (lexicographical order) constraint. 47 * 48 * @author Krzysztof Kuchcinski and Radoslaw Szymanek 49 * @version 4.8 50 */ 51 52 public class Lex extends DecomposedConstraint<Constraint> { 53 54 /** 55 * A two dimensional array containing arrays which have to be lexicographically ordered. 56 */ 57 public IntVar[][] x; 58 59 /** 60 * It contains constraints of the lex constraint decomposition. 61 */ 62 List<Constraint> constraints; 63 64 /** 65 * Is the lex enforcing lower then relationship? 66 */ 67 public final boolean lexLT; 68 69 /** 70 * It creates a lexicographical order for vectors x[i], i.e. 71 * forall i, exists j : x[i][k] = x[i+1][k] for k {@literal <} j and x[i][k] {@literal <=} x[i+1][k] 72 * for k {@literal >=} j 73 * <p> 74 * vectors x[i] does not need to be of the same size. 75 * boolea lt defines if we require Lex_{{@literal <}} (lt = false) or Lex_{{@literal =<}} (lt = true) 76 * 77 * @param x vector of vectors which assignment is constrained by Lex constraint. 78 */ Lex(IntVar[][] x)79 public Lex(IntVar[][] x) { 80 81 this(x, false); 82 83 } 84 85 Lex(IntVar[][] x, boolean lt)86 public Lex(IntVar[][] x, boolean lt) { 87 88 assert (x != null) : "x list is null."; 89 this.x = new IntVar[x.length][]; 90 91 lexLT = lt; 92 93 for (int i = 0; i < x.length; i++) { 94 95 assert (x[i] != null) : i + "-th vector in x is null"; 96 this.x[i] = new IntVar[x[i].length]; 97 98 for (int j = 0; j < x[i].length; j++) { 99 assert (x[i][j] != null) : j + "-th element of " + i + "-th vector in x is null"; 100 this.x[i][j] = x[i][j]; 101 } 102 103 } 104 105 } 106 107 imposeDecomposition(Store store)108 @Override public void imposeDecomposition(Store store) { 109 110 if (constraints == null) 111 constraints = decompose(store); 112 113 for (Constraint c : constraints) 114 store.impose(c, queueIndex); 115 116 } 117 decompose(Store store)118 @Override public List<Constraint> decompose(Store store) { 119 120 if (constraints != null) 121 return constraints; 122 123 if (x.length == 2) // && x[0].length > 100) 124 if (lexLT) 125 return decomposeLT(store); 126 else 127 return decomposeLE(store); 128 129 // smaller Lex with several lists can be decompose with Regular 130 if (lexLT) 131 return decomposeLTRegular(store); 132 else 133 return decomposeLERegular(store); 134 135 } 136 137 decomposeLERegular(Store store)138 public List<Constraint> decomposeLERegular(Store store) { 139 140 if (constraints == null) 141 constraints = new ArrayList<Constraint>(); 142 else 143 return constraints; 144 145 // first index represents compared vectors and the second variables within vectors 146 // int numberStates = 0; 147 int numberVar = 0; 148 149 BooleanVar[][] lt = new BooleanVar[x.length - 1][]; 150 BooleanVar[][] eq = new BooleanVar[x.length - 1][]; 151 FSMState[][][] state = new FSMState[x.length - 1][][]; 152 FSMState[][] addState = new FSMState[x.length - 2][]; 153 154 for (int i = 0; i < x.length - 1; ++i) { 155 156 int sizeToCompare = (x[i].length < x[i + 1].length) ? x[i].length : x[i + 1].length; 157 158 lt[i] = new BooleanVar[sizeToCompare]; 159 eq[i] = new BooleanVar[sizeToCompare]; 160 state[i] = new FSMState[sizeToCompare][]; 161 162 for (int j = 0; j < sizeToCompare; j++) { 163 lt[i][j] = new BooleanVar(store, "lt_" + i + "_" + j); 164 eq[i][j] = new BooleanVar(store, "eq_" + i + "_" + j); 165 166 constraints.add(new Reified(new XltY(x[i][j], x[i + 1][j]), lt[i][j])); 167 constraints.add(new Reified(new XeqY(x[i][j], x[i + 1][j]), eq[i][j])); 168 169 if (x[i].length > x[i + 1].length && j == sizeToCompare - 1) 170 constraints.add(new XeqC(eq[i][j], 0)); 171 172 state[i][j] = new FSMState[2]; 173 state[i][j][0] = new FSMState(); 174 state[i][j][1] = new FSMState(); 175 numberVar += 2; 176 // numberStates += 2; 177 178 if (i < x.length - 2) { 179 // numberStates += 2*(sizeToCompare-j) - 1; 180 if (j == 0) { 181 addState[i] = new FSMState[2 * (sizeToCompare - j) - 1]; 182 183 for (int k = 0; k < addState[i].length; k++) 184 addState[i][k] = new FSMState(); 185 } 186 } 187 } 188 } 189 // numberStates++; 190 191 IntVar[] var = new IntVar[numberVar]; 192 FSM g = new FSM(); 193 int k = 0; 194 for (int i = 0; i < lt.length; i++) { 195 for (int j = 0; j < lt[i].length; j++) { 196 var[k++] = lt[i][j]; 197 var[k++] = eq[i][j]; 198 199 g.allStates.add(state[i][j][0]); 200 g.allStates.add(state[i][j][1]); 201 } 202 } 203 for (int i = 0; i < addState.length; i++) 204 for (int j = 0; j < addState[i].length; j++) 205 g.allStates.add(addState[i][j]); 206 207 208 g.initState = state[0][0][0]; 209 FSMState terminate = new FSMState(); 210 g.allStates.add(terminate); 211 g.finalStates.add(terminate); 212 213 for (int i = 0; i < state.length; i++) { 214 for (int j = 0; j < state[i].length; j++) { 215 216 if (i != state.length - 1) { 217 // cannot go directly- must go through other states :( 218 if (addState[i].length != 0) { 219 if (j == 0) { 220 state[i][j][0].transitions.add(new FSMTransition(new IntervalDomain(1, 1), addState[i][0])); 221 222 for (int s = 1; s < addState[i].length; s++) 223 addState[i][s - 1].transitions.add(new FSMTransition(new IntervalDomain(0, 1), addState[i][s])); 224 addState[i][addState[i].length - 1].transitions 225 .add(new FSMTransition(new IntervalDomain(0, 1), state[i + 1][0][0])); 226 } else 227 state[i][j][0].transitions.add(new FSMTransition(new IntervalDomain(1, 1), addState[i][2 * j])); 228 229 state[i][j][0].transitions.add(new FSMTransition(new IntervalDomain(0, 0), state[i][j][1])); 230 } 231 } else { // i == state.length 232 state[i][j][0].transitions.add(new FSMTransition(new IntervalDomain(1, 1), terminate)); 233 state[i][j][0].transitions.add(new FSMTransition(new IntervalDomain(0, 0), state[i][j][1])); 234 } 235 236 if (i != state.length - 1) { 237 if (j != state[i].length - 1) 238 state[i][j][1].transitions.add(new FSMTransition(new IntervalDomain(1, 1), state[i][j + 1][0])); 239 else 240 state[i][j][1].transitions.add(new FSMTransition(new IntervalDomain(1, 1), state[i + 1][0][0])); 241 } else { // i == state.length 242 if (j != state[i].length - 1) 243 state[i][j][1].transitions.add(new FSMTransition(new IntervalDomain(1, 1), state[i][j + 1][0])); 244 else { 245 state[i][j][1].transitions.add(new FSMTransition(new IntervalDomain(1, 1), terminate)); 246 } 247 } 248 } 249 } 250 251 terminate.transitions.add(new FSMTransition(new IntervalDomain(0, 1), terminate)); 252 253 constraints.add(new Regular(g, var)); 254 255 return constraints; 256 } 257 258 decomposeLTRegular(Store store)259 public List<Constraint> decomposeLTRegular(Store store) { 260 261 if (constraints == null) 262 constraints = new ArrayList<Constraint>(); 263 else 264 return constraints; 265 266 // first index represents compared vectors and the second varinbales within vectors 267 // int numberStates = 0; 268 int numberVar = 0; 269 BooleanVar[][] lt = new BooleanVar[x.length - 1][]; 270 BooleanVar[][] eq = new BooleanVar[x.length - 1][]; 271 FSMState[][][] state = new FSMState[x.length - 1][][]; 272 FSMState[][] addState = new FSMState[x.length - 2][]; 273 274 for (int i = 0; i < x.length - 1; ++i) { 275 276 int sizeToCompare = (x[i].length < x[i + 1].length) ? x[i].length : x[i + 1].length; 277 278 lt[i] = new BooleanVar[sizeToCompare]; 279 eq[i] = new BooleanVar[sizeToCompare - 1]; 280 state[i] = new FSMState[sizeToCompare][]; 281 282 for (int j = 0; j < sizeToCompare; j++) { 283 284 if (x[i].length < x[i + 1].length) 285 if (j < sizeToCompare - 1) { 286 lt[i][j] = new BooleanVar(store, "lt_" + i + "_" + j); 287 numberVar++; 288 constraints.add(new Reified(new XltY(x[i][j], x[i + 1][j]), lt[i][j])); 289 } else { // j == sizeToCompare - 1 , i.e., last check 290 lt[i][j] = new BooleanVar(store, "le_" + i + "_" + j); 291 numberVar++; 292 constraints.add(new Reified(new XlteqY(x[i][j], x[i + 1][j]), lt[i][j])); 293 } 294 else { 295 lt[i][j] = new BooleanVar(store, "lt_" + i + "_" + j); 296 numberVar++; 297 constraints.add(new Reified(new XltY(x[i][j], x[i + 1][j]), lt[i][j])); 298 } 299 300 if (j < sizeToCompare - 1) { 301 eq[i][j] = new BooleanVar(store, "eq_" + i + "_" + j); 302 numberVar++; 303 constraints.add(new Reified(new XeqY(x[i][j], x[i + 1][j]), eq[i][j])); 304 } 305 306 state[i][j] = new FSMState[2]; 307 state[i][j][0] = new FSMState(); 308 // numberStates++; 309 if (j < sizeToCompare - 1) { 310 state[i][j][1] = new FSMState(); 311 // numberStates++; 312 } 313 314 if (i < x.length - 2) { 315 // numberStates += 2*(sizeToCompare-j) - 2; 316 317 if (j == 0) { 318 addState[i] = new FSMState[2 * (sizeToCompare - j) - 2]; 319 320 for (int k = 0; k < addState[i].length; k++) 321 addState[i][k] = new FSMState(); 322 } 323 } 324 } 325 } 326 // numberStates++; 327 328 IntVar[] var = new IntVar[numberVar]; 329 FSM g = new FSM(); 330 int k = 0; 331 for (int i = 0; i < lt.length; i++) { 332 for (int j = 0; j < lt[i].length; j++) { 333 var[k++] = lt[i][j]; 334 if (j < eq[i].length) 335 var[k++] = eq[i][j]; 336 337 g.allStates.add(state[i][j][0]); 338 if (j < eq[i].length) 339 g.allStates.add(state[i][j][1]); 340 } 341 } 342 for (int i = 0; i < addState.length; i++) 343 for (int j = 0; j < addState[i].length; j++) 344 g.allStates.add(addState[i][j]); 345 346 347 g.initState = state[0][0][0]; 348 FSMState terminate = new FSMState(); 349 g.allStates.add(terminate); 350 g.finalStates.add(terminate); 351 352 for (int i = 0; i < state.length; i++) { 353 for (int j = 0; j < state[i].length; j++) { 354 355 if (i != state.length - 1) { 356 // cannot go directly - must go through other states :( 357 if (addState[i].length != 0) 358 if (j == 0) { 359 state[i][j][0].transitions.add(new FSMTransition(new IntervalDomain(1, 1), addState[i][0])); 360 361 for (int s = 1; s < addState[i].length; s++) 362 addState[i][s - 1].transitions.add(new FSMTransition(new IntervalDomain(0, 1), addState[i][s])); 363 addState[i][addState[i].length - 1].transitions 364 .add(new FSMTransition(new IntervalDomain(0, 1), state[i + 1][0][0])); 365 } else if (j != state[i].length - 1) { 366 state[i][j][0].transitions.add(new FSMTransition(new IntervalDomain(1, 1), addState[i][2 * j])); 367 } else 368 state[i][j][0].transitions.add(new FSMTransition(new IntervalDomain(1, 1), state[i + 1][0][0])); 369 else 370 state[i][j][0].transitions.add(new FSMTransition(new IntervalDomain(1, 1), state[i + 1][0][0])); 371 if (j != state[i].length - 1) 372 state[i][j][0].transitions.add(new FSMTransition(new IntervalDomain(0, 0), state[i][j][1])); 373 } else { 374 state[i][j][0].transitions.add(new FSMTransition(new IntervalDomain(1, 1), terminate)); 375 if (j != state[i].length - 1) 376 state[i][j][0].transitions.add(new FSMTransition(new IntervalDomain(0, 0), state[i][j][1])); 377 } 378 379 if (j != state[i].length - 1) 380 state[i][j][1].transitions.add(new FSMTransition(new IntervalDomain(1, 1), state[i][j + 1][0])); 381 } 382 } 383 384 terminate.transitions.add(new FSMTransition(new IntervalDomain(0, 1), terminate)); 385 386 constraints.add(new Regular(g, var)); 387 388 return constraints; 389 } 390 decomposeLT(Store store)391 public List<Constraint> decomposeLT(Store store) { 392 393 if (constraints == null) 394 constraints = new ArrayList<Constraint>(); 395 else 396 return constraints; 397 398 int sizeToCompare = (x[0].length < x[1].length) ? x[0].length : x[1].length; 399 400 BooleanVar[] b = new BooleanVar[sizeToCompare + 1]; 401 for (int i = 0; i < b.length; i++) 402 b[i] = new BooleanVar(store); 403 404 constraints.add(new XeqC(b[0], 1)); 405 406 for (int i = 0; i < sizeToCompare; i++) { 407 Constraint c = 408 new Reified(new And(new XlteqY(x[0][i], x[1][i]), new Or(new XltY(x[0][i], x[1][i]), new XeqC(b[i + 1], 1))), b[i]); 409 410 constraints.add(c); 411 } 412 if (x[0].length < x[1].length) 413 constraints.add(new XeqC(b[sizeToCompare], 1)); 414 else 415 constraints.add(new XeqC(b[sizeToCompare], 0)); 416 417 return constraints; 418 } 419 decomposeLE(Store store)420 public List<Constraint> decomposeLE(Store store) { 421 422 if (constraints == null) 423 constraints = new ArrayList<Constraint>(); 424 else 425 return constraints; 426 427 int sizeToCompare = (x[0].length < x[1].length) ? x[0].length : x[1].length; 428 429 BooleanVar[] b = new BooleanVar[sizeToCompare]; 430 for (int i = 0; i < b.length; i++) 431 b[i] = new BooleanVar(store); 432 433 constraints.add(new XeqC(b[0], 1)); 434 435 for (int i = 0; i < sizeToCompare; i++) { 436 if (i == sizeToCompare - 1) 437 constraints.add(new Reified(new XlteqY(x[0][i], x[1][i]), b[i])); 438 else 439 constraints.add( 440 new Reified(new And(new XlteqY(x[0][i], x[1][i]), new Or(new XltY(x[0][i], x[1][i]), new XeqC(b[i + 1], 1))), b[i])); 441 } 442 443 return constraints; 444 } 445 446 } 447