View Javadoc

1   /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    * 
4    * Based on the original minisat specification from:
5    * 
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    * 
10   * This library is free software; you can redistribute it and/or modify it under
11   * the terms of the GNU Lesser General Public License as published by the Free
12   * Software Foundation; either version 2.1 of the License, or (at your option)
13   * any later version.
14   * 
15   * This library is distributed in the hope that it will be useful, but WITHOUT
16   * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17   * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18   * details.
19   * 
20   * You should have received a copy of the GNU Lesser General Public License
21   * along with this library; if not, write to the Free Software Foundation, Inc.,
22   * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23   * 
24   */
25  package org.sat4j.reader.csp;
26  
27  import java.util.HashMap;
28  import java.util.Map;
29  
30  import org.sat4j.specs.ContradictionException;
31  import org.sat4j.specs.ISolver;
32  import org.sat4j.specs.IVec;
33  
34  public abstract class Supports implements Relation {
35  
36      private Encoding encoding;
37  
38      private final int arity;
39  
40      private int[][] tuples;
41  
42      private int lastmatch;
43  
44      private Map<Evaluable, Integer> mtuple;
45  
46      public Supports(int arity, int nbtuples) {
47          this.arity = arity;
48          tuples = new int[nbtuples][];
49      }
50  
51      public void addTuple(int index, int[] tuple) {
52          tuples[index] = tuple;
53      }
54  
55      public int arity() {
56          return arity;
57      }
58  
59      public void toClause(ISolver solver, IVec<Var> scope, IVec<Evaluable> vars)
60              throws ContradictionException {
61          assert vars.size() == 0;
62          assert scope.size() == arity;
63          int[] tuple = new int[scope.size()];
64          mtuple = new HashMap<Evaluable, Integer>();
65          lastmatch = -1;
66          encoding = chooseEncoding(scope);
67          encoding.onInit(solver, scope);
68          find(tuple, 0, scope, solver);
69          encoding.onFinish(solver, scope);
70      }
71  
72      protected abstract Encoding chooseEncoding(IVec<Var> scope);
73  
74      private void find(int[] tuple, int n, IVec<Var> scope, ISolver solver)
75              throws ContradictionException {
76          if (n == scope.size()) {
77              assert mtuple.size() == n;
78              if (notPresent(tuple)) {
79                  encoding.onNogood(solver, scope, mtuple);
80              } else {
81                  encoding.onSupport(solver, scope, mtuple);
82              }
83          } else {
84              Domain domain = scope.get(n).domain();
85              for (int i = 0; i < domain.size(); i++) {
86                  tuple[n] = domain.get(i);
87                  mtuple.put(scope.get(n), tuple[n]);
88                  find(tuple, n + 1, scope, solver);
89              }
90              mtuple.remove(scope.get(n));
91  
92          }
93  
94      }
95  
96      private boolean notPresent(int[] tuple) {
97          // System.out.println("Checking:" + Arrays.asList(tuple));
98          // find the first tuple begining with the same
99          // initial number
100         int i = lastmatch + 1;
101         int j = 0;
102         final int[][] ltuples = tuples;
103         int searchedvalue, currentvalue;
104         while (i < ltuples.length && j < tuple.length) {
105             searchedvalue = ltuples[i][j];
106             currentvalue = tuple[j];
107             if (searchedvalue < currentvalue) {
108                 i++;
109                 j = 0;
110                 continue;
111             }
112             if (searchedvalue > currentvalue)
113                 return true;
114             j++;
115         }
116         if (j == tuple.length) {
117             lastmatch = i;
118             return false;
119         }
120         return true;
121     }
122 }