1 /*******************************************************************************
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004, 2012 Artois University and CNRS
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 * Based on the original MiniSat specification from:
20 *
21 * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22 * Sixth International Conference on Theory and Applications of Satisfiability
23 * Testing, LNCS 2919, pp 502-518, 2003.
24 *
25 * See www.minisat.se for the original solver in C++.
26 *
27 * Contributors:
28 * CRIL - initial API and implementation
29 *******************************************************************************/
30
31 package org.sat4j.tools.encoding;
32
33 import org.sat4j.core.ConstrGroup;
34 import org.sat4j.core.VecInt;
35 import org.sat4j.specs.ContradictionException;
36 import org.sat4j.specs.IConstr;
37 import org.sat4j.specs.ISolver;
38 import org.sat4j.specs.IVecInt;
39
40 /**
41 *
42 * Ladder encoding for the "at most one" and "exactly one" cases.
43 *
44 * The ladder encoding described in: I. P. Gent and P. Nightingale,
45 * "A new encoding for AllDifferent into SAT", in International Workshop on
46 * Modeling and Reformulating Constraint Satisfaction Problems, 2004
47 *
48 * @author sroussel
49 * @since 2.3.1
50 */
51 public class Ladder extends EncodingStrategyAdapter {
52
53 /**
54 *
55 */
56 private static final long serialVersionUID = 1L;
57
58 @Override
59 /**
60 * If n is the number of variables in the constraint,
61 * this encoding adds n variables and 4n clauses
62 * (3n+1 size 2 clauses and n-1 size 3 clauses)
63 */
64 public IConstr addAtMostOne(ISolver solver, IVecInt literals)
65 throws ContradictionException {
66 ConstrGroup group = new ConstrGroup(false);
67 final int n = literals.size() + 1;
68
69 int xN = solver.nextFreeVarId(true);
70 int y[] = new int[n - 1];
71
72 for (int i = 0; i < n - 1; i++) {
73 y[i] = solver.nextFreeVarId(true);
74 }
75
76 IVecInt clause = new VecInt();
77
78 // Constraint \bigwedge_{i=1}{n-2} (\neg y_{i+1} \vee y_i)
79 for (int i = 1; i <= n - 2; i++) {
80 clause.push(-y[i]);
81 clause.push(y[i - 1]);
82 group.add(solver.addClause(clause));
83 clause.clear();
84 }
85
86 // Constraint \bigwedge_{i=2}{n-1} (\neg y_{i-1} \vee y_i \vee x_i)
87 for (int i = 2; i <= n - 1; i++) {
88 clause.push(-y[i - 2]);
89 clause.push(y[i - 1]);
90 clause.push(literals.get(i - 1));
91 group.add(solver.addClause(clause));
92 clause.clear();
93 }
94
95 // Constraint \bigwedge_{i=2}{n-1} (\neg x_i \vee y_{i-1)})
96 for (int i = 2; i <= n - 1; i++) {
97 clause.push(-literals.get(i - 1));
98 clause.push(y[i - 2]);
99 group.add(solver.addClause(clause));
100 clause.clear();
101 }
102
103 // Constraint \bigwedge_{i=2}{n-1} (\neg x_i \vee \neg y_i)
104 for (int i = 2; i <= n - 1; i++) {
105 clause.push(-literals.get(i - 1));
106 clause.push(-y[i - 1]);
107 group.add(solver.addClause(clause));
108 clause.clear();
109 }
110
111 // Constraint y_1 \vee x_1
112 clause.push(y[0]);
113 clause.push(literals.get(0));
114 group.add(solver.addClause(clause));
115 clause.clear();
116
117 // Constraint \neg y_1 \vee \neg x_1
118 clause.push(-y[0]);
119 clause.push(-literals.get(0));
120 group.add(solver.addClause(clause));
121 clause.clear();
122
123 // Constraint \neg y_{n-1} \vee x_n
124 clause.push(-y[n - 2]);
125 clause.push(xN);
126 group.add(solver.addClause(clause));
127 clause.clear();
128
129 // Constraint y_{n-1} \vee \neg x_n
130 clause.push(y[n - 2]);
131 clause.push(-xN);
132 group.add(solver.addClause(clause));
133 clause.clear();
134
135 return group;
136 }
137
138 @Override
139 /**
140 * If n is the number of variables in the constraint,
141 * this encoding adds n-1 variables and 4(n-1) clauses
142 * (3n-2 size 2 clauses and n-2 size 3 clauses)
143 */
144 public IConstr addExactlyOne(ISolver solver, IVecInt literals)
145 throws ContradictionException {
146 ConstrGroup group = new ConstrGroup(false);
147 final int n = literals.size();
148
149 IVecInt clause = new VecInt();
150
151 if (n == 1) {
152 clause.push(literals.get(0));
153 group.add(solver.addClause(clause));
154 return group;
155 }
156
157 int y[] = new int[n - 1];
158
159 for (int i = 0; i < n - 1; i++) {
160 y[i] = solver.nextFreeVarId(true);
161 }
162
163 // Constraint \bigwedge_{i=1}{n-2} (\neg y_{i+1} \vee y_i)
164 for (int i = 1; i <= n - 2; i++) {
165 clause.push(-y[i]);
166 clause.push(y[i - 1]);
167 group.add(solver.addClause(clause));
168 clause.clear();
169 }
170
171 // Constraint \bigwedge_{i=2}{n-1} (\neg y_{i-1} \vee y_i \vee x_i)
172 for (int i = 2; i <= n - 1; i++) {
173 clause.push(-y[i - 2]);
174 clause.push(y[i - 1]);
175 clause.push(literals.get(i - 1));
176 group.add(solver.addClause(clause));
177 clause.clear();
178 }
179
180 // Constraint \bigwedge_{i=2}{n-1} (\neg x_i \vee y_{i-1)})
181 for (int i = 2; i <= n - 1; i++) {
182 clause.push(-literals.get(i - 1));
183 clause.push(y[i - 2]);
184 group.add(solver.addClause(clause));
185 clause.clear();
186 }
187
188 // Constraint \bigwedge_{i=2}{n-1} (\neg x_i \vee \neg y_i)
189 for (int i = 2; i <= n - 1; i++) {
190 clause.push(-literals.get(i - 1));
191 clause.push(-y[i - 1]);
192 group.add(solver.addClause(clause));
193 clause.clear();
194 }
195
196 // Constraint y_1 \vee x_1
197 clause.push(y[0]);
198 clause.push(literals.get(0));
199 group.add(solver.addClause(clause));
200 clause.clear();
201
202 // Constraint \neg y_1 \vee \neg x_1
203 clause.push(-y[0]);
204 clause.push(-literals.get(0));
205 group.add(solver.addClause(clause));
206 clause.clear();
207
208 // Constraint \neg y_{n-1} \vee x_n
209 clause.push(-y[n - 2]);
210 clause.push(literals.get(n - 1));
211 group.add(solver.addClause(clause));
212 clause.clear();
213
214 // Constraint y_{n-1} \vee \neg x_n
215 clause.push(y[n - 2]);
216 clause.push(-literals.get(n - 1));
217 group.add(solver.addClause(clause));
218 clause.clear();
219
220 return group;
221 }
222 }