View Javadoc

1   /*******************************************************************************
2   * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
3   *
4   * All rights reserved. This program and the accompanying materials
5   * are made available under the terms of the Eclipse Public License v1.0
6   * which accompanies this distribution, and is available at
7   * http://www.eclipse.org/legal/epl-v10.html
8   *
9   * Alternatively, the contents of this file may be used under the terms of
10  * either the GNU Lesser General Public License Version 2.1 or later (the
11  * "LGPL"), in which case the provisions of the LGPL are applicable instead
12  * of those above. If you wish to allow use of your version of this file only
13  * under the terms of the LGPL, and not to allow others to use your version of
14  * this file under the terms of the EPL, indicate your decision by deleting
15  * the provisions above and replace them with the notice and other provisions
16  * required by the LGPL. If you do not delete the provisions above, a recipient
17  * may use your version of this file under the terms of the EPL or the LGPL.
18  *******************************************************************************/
19  package org.sat4j.csp.constraints;
20  
21  import org.sat4j.core.VecInt;
22  import org.sat4j.csp.Clausifiable;
23  import org.sat4j.csp.Evaluable;
24  import org.sat4j.csp.Var;
25  import org.sat4j.specs.ContradictionException;
26  import org.sat4j.specs.ISolver;
27  import org.sat4j.specs.IVec;
28  import org.sat4j.specs.IVecInt;
29  import org.sat4j.specs.IteratorInt;
30  
31  public class AllDiff implements Clausifiable {
32  
33      public void toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
34              throws ContradictionException {
35          int n = scope.size();
36          IVecInt clause = new VecInt();
37          int vali,valj;
38          for (int i = 0; i < n; i++) {
39              Var vi = scope.get(i);
40              for (int j = i + 1; j < n; j++) {
41                  // make all values differents
42                  Var vj = scope.get(j);
43                  for (IteratorInt iti = vi.domain().iterator(); iti.hasNext();) {
44                      vali = iti.next();
45                      for (IteratorInt itj = vj.domain().iterator(); itj.hasNext();) {
46                          valj = itj.next();
47                          // the two variables share a common value
48                          if (vali == valj) {
49                              clause.push(-vi.translate(vali));
50                              clause.push(-vj.translate(valj));
51                              solver.addClause(clause);
52                              clause.clear();
53                          }
54                      }
55                  }
56              }
57          }
58      }
59      
60      @Override
61      public String toString() {
62      	return "AllDiff encoding using binary clauses";
63      }
64  }