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 java.util.HashMap;
22  import java.util.Map;
23  
24  import org.sat4j.csp.Domain;
25  import org.sat4j.csp.Encoding;
26  import org.sat4j.csp.Evaluable;
27  import org.sat4j.csp.Var;
28  import org.sat4j.specs.ContradictionException;
29  import org.sat4j.specs.ISolver;
30  import org.sat4j.specs.IVec;
31  
32  public abstract class Supports implements Relation {
33  
34      private Encoding encoding;
35  
36      private final int arity;
37  
38      private int[][] tuples;
39  
40      private int lastmatch;
41  
42      private Map<Evaluable, Integer> mtuple;
43  
44      public Supports(int arity, int nbtuples) {
45          this.arity = arity;
46          tuples = new int[nbtuples][];
47      }
48  
49      public void addTuple(int index, int[] tuple) {
50          tuples[index] = tuple;
51      }
52  
53      public int arity() {
54          return arity;
55      }
56  
57      public void toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
58              throws ContradictionException {
59          assert vars.size() == 0;
60          assert scope.size() == arity;
61          int[] tuple = new int[scope.size()];
62          mtuple = new HashMap<Evaluable, Integer>();
63          lastmatch = -1;
64          encoding = chooseEncoding(scope);
65          encoding.onInit(solver, scope);
66          find(tuple, 0, scope, solver);
67          encoding.onFinish(solver, scope);
68      }
69  
70      protected abstract Encoding chooseEncoding(IVec<Var> scope);
71  
72      private void find(int[] tuple, int n, IVec<Var> scope, ISolver solver)
73              throws ContradictionException {
74          if (n == scope.size()) {
75              assert mtuple.size() == n;
76              if (notPresent(tuple)) {
77                  encoding.onNogood(solver, scope, mtuple);
78              } else {
79                  encoding.onSupport(solver, scope, mtuple);
80              }
81          } else {
82              Domain domain = scope.get(n).domain();
83              for (int i = 0; i < domain.size(); i++) {
84                  tuple[n] = domain.get(i);
85                  mtuple.put(scope.get(n), tuple[n]);
86                  find(tuple, n + 1, scope, solver);
87              }
88              mtuple.remove(scope.get(n));
89  
90          }
91  
92      }
93  
94      private boolean notPresent(int[] tuple) {
95          // System.out.println("Checking:" + Arrays.asList(tuple));
96          // find the first tuple begining with the same
97          // initial number
98          int i = lastmatch + 1;
99          int j = 0;
100         final int[][] ltuples = tuples;
101         int searchedvalue, currentvalue;
102         while (i < ltuples.length && j < tuple.length) {
103             searchedvalue = ltuples[i][j];
104             currentvalue = tuple[j];
105             if (searchedvalue < currentvalue) {
106                 i++;
107                 j = 0;
108                 continue;
109             }
110             if (searchedvalue > currentvalue)
111                 return true;
112             j++;
113         }
114         if (j == tuple.length) {
115             lastmatch = i;
116             return false;
117         }
118         return true;
119     }
120 }