Home | Examples | Documents | Advanced Usage | Tutorial | Apps |
\( \bigwedge_{i < j} (x_{i} \ne x_{j}) \)
def alldiff(xs: Seq[Var]) = { And(And(for (Seq(x, y) <- xs.combinations(2)) yield x !== y)) }
\(\bigwedge_{i < j} (x_{i} \ne x_{j}) \wedge \bigwedge_{i=lb}^{ub}\left(\bigvee_{j=1}^{n} (x_{j}=i)\right)\)
def alldiff(xs: Seq[Var]) = { var lb = for (x <- xs) yield csp.dom(x).lb var ub = for (x <- xs) yield csp.dom(x).ub And( And(for (Seq(x, y) <- xs.combinations(2)) yield x !== y), And(for (num <- lb.min to ub.max) yield Or(for (x <- xs) yield x === num)) ) }
\(\bigwedge_{i < j} (x_{i} \ne x_{j}) \wedge \neg\bigwedge_{i=1}^{n}(x_{i} < lb + n - 1) \wedge \neg\bigwedge_{i=1}^{n}(x_{i} > ub - n+ 1)\)
def alldiff(xs: Seq[Var]) = { var lb = for (x <- xs) yield csp.dom(x).lb var ub = for (x <- xs) yield csp.dom(x).ub And( And(for (Seq(x, y) <- xs.combinations(2)) yield x !== y), Or(for (x <- xs) yield !(x < lb.min+xs.size-1)), Or(for (x <- xs) yield !(x > ub.max-xs.size+1)) ) }
\(\bigwedge_{i < j} (x_{i} \ne x_{j}) \wedge \bigwedge_{i=lb}^{ub}\left(\bigvee_{j=1}^{n} (x_{j}=i)\right) \wedge \neg\bigwedge_{i=1}^{n}(x_{i} < lb + n - 1) \wedge \neg\bigwedge_{i=1}^{n}(x_{i} > ub - n+ 1)\)
def alldiff(xs: Seq[Var]) = { var lb = for (x <- xs) yield csp.dom(x).lb var ub = for (x <- xs) yield csp.dom(x).ub And( And(for (Seq(x, y) <- xs.combinations(2)) yield x !== y), And(for (num <- lb.min to ub.max) yield Or(for (x <- xs) yield x === num)), Or(for (x <- xs) yield !(x < lb.min+xs.size-1)), Or(for (x <- xs) yield !(x > ub.max-xs.size+1)) ) }
import jp.kobe_u.scarab._ , dsl._ var n: Int = 5 for (i <- 1 to n; j <- 1 to n) int('x(i,j),1,n) for (i <- 1 to n) { add(alldiff((1 to n).map(j => 'x(i,j)))) add(alldiff((1 to n).map(j => 'x(j,i)))) add(alldiff((1 to n).map(j => 'x(j,(i+j-1)%n+1)))) add(alldiff((1 to n).map(j => 'x(j,(i+(j-1)*(n-1))%n+1))))} if (find) println(solution)
7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 | 16 | #Total | |
---|---|---|---|---|---|---|---|---|---|---|---|
Alldiff 1 | 0.210 | T.O. | T.O. | T.O. | 0.347 | T.O. | T.O. | T.O. | T.O. | T.O. | 2 |
Alldiff 2 | 0.232 | 0.245 | 0.230 | 0.391 | 0.317 | 1.150 | T.O. | 14.309 | 953.0 | 1303.0 | 9 |
Alldiff 3 | 0.265 | 0.306 | 0.219 | 0.332 | 0.252 | 0.885 | T.O. | 9.826 | 423.3 | 840.7 | 9 |
Alldiff 4 | 0.221 | 0.212 | 0.235 | 0.370 | 0.332 | 0.981 | 0.545 | 9.792 | 389.9 | 458.1 | 10 |
import jp.kobe_u.scarab._ , dsl._ val n = 15; val s =36 for (i <- 1 to n) { int('x(i),0,s-i) ; int('y(i),0,s-i) } for (i <- 1 to n; j <- i+1 to n) add(('x(i)+i<='x(j)) || ('x(j)+j<='x(i)) || ('y(i)+i<='y(j)) || ('y(j)+j<='y(i))) if (find) println(solution.intMap) var lb = 15; var ub = s; int('m, lb, ub) for (i <- 1 to n) add(('x(i)+i <= 'm) && ('y(i)+i <= 'm)) while(lb <= ub && find('m <= ub)) { add('m <= ub); ub -= 1 } while(find) println(solution.intMap)
var lb = 15; var ub = s; int('m, lb, ub) for (i <- 1 to n) add(('x(i)+i <= 'm) && ('y(i)+i <= 'm)) while(lb < ub && !find('m <= lb)) { add('m > lb); lb += 1 } while(find) println(solution.intMap)
var lb = 5; var ub = s commit while(lb < ub) { var size = (lb + ub) / 2 for (i <- 1 to n) add(('x(i)+i<=size)&&('y(i)+i<=size)) if (find) { ub = size; commit; } else { lb = size + 1; rollback; } }
Created: 2019-02-11 月 15:00