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 * Binary encoding for the "at most one" and "at most k" cases.
42 *
43 * For the case "at most one", we can use the binary encoding (also called
44 * birwise encoding) first described in A. M. Frisch, T. J. Peugniez, A. J.
45 * Dogget and P. Nightingale, "Solving Non-Boolean Satisfiability Problems With
46 * Stochastic Local Search: A Comparison of Encodings" in Journal of Automated
47 * Reasoning, vol. 35, n 1-3, 2005.
48 *
49 * The approach is generalized for the "at most k" case in A. M. Frisch and P.
50 * A. Giannaros, "SAT Encodings of the At-Most-k Constraint", in International
51 * Workshop on Modelling and Reformulating Constraint Satisfaction Problems,
52 * 2010
53 *
54 * @author sroussel
55 * @since 2.3.1
56 */
57 public class Binary extends EncodingStrategyAdapter {
58
59 /**
60 *
61 */
62 private static final long serialVersionUID = 1L;
63
64 /**
65 * p being the smaller integer greater than log_2(n), this encoding adds p
66 * variables and n*p clauses.
67 *
68 */
69 @Override
70 public IConstr addAtMostOne(ISolver solver, IVecInt literals)
71 throws ContradictionException {
72 ConstrGroup group = new ConstrGroup(false);
73
74 final int n = literals.size();
75 final int p = (int) Math.ceil(Math.log(n) / Math.log(2));
76 final int k = (int) Math.pow(2, p) - n;
77
78 IVecInt clause = new VecInt();
79 String binary = "";
80
81 if (p == 0) {
82 return group;
83 }
84
85 int y[] = new int[p];
86 for (int i = 0; i < p; i++) {
87 y[i] = solver.nextFreeVarId(true);
88 }
89
90 for (int i = 0; i < k; i++) {
91 binary = Integer.toBinaryString(i);
92 while (binary.length() != p - 1) {
93 binary = "0" + binary;
94 }
95
96 for (int j = 0; j < p - 1; j++) {
97 clause.push(-literals.get(i));
98 if (binary.charAt(j) == '0') {
99 clause.push(-y[j]);
100 } else {
101 clause.push(y[j]);
102 }
103 group.add(solver.addClause(clause));
104 clause.clear();
105
106 }
107 }
108
109 for (int i = k; i < n; i++) {
110 binary = Integer.toBinaryString(2 * k + i - k);
111 while (binary.length() != p) {
112 binary = "0" + binary;
113 }
114 for (int j = 0; j < p; j++) {
115 clause.push(-literals.get(i));
116 if (binary.charAt(j) == '0') {
117 clause.push(-y[j]);
118 } else {
119 clause.push(y[j]);
120 }
121 group.add(solver.addClause(clause));
122 clause.clear();
123 }
124
125 }
126
127 return group;
128 }
129
130 @Override
131 public IConstr addAtMost(ISolver solver, IVecInt literals, int k)
132 throws ContradictionException {
133
134 final int n = literals.size();
135 final int p = (int) Math.ceil(Math.log(n) / Math.log(2));
136
137 ConstrGroup group = new ConstrGroup(false);
138
139 int[][] b = new int[k][p];
140
141 for (int i = 0; i < k; i++) {
142 for (int j = 0; j < p; j++) {
143 b[i][j] = solver.nextFreeVarId(true);
144 }
145 }
146
147 int[][] t = new int[k][n];
148
149 for (int i = 0; i < k; i++) {
150 for (int j = 0; j < n; j++) {
151 t[i][j] = solver.nextFreeVarId(true);
152 }
153 }
154
155 int max, min;
156 IVecInt clause1 = new VecInt();
157 IVecInt clause2 = new VecInt();
158 String binary = "";
159 for (int i = 0; i < n; i++) {
160 max = Math.max(1, k - n + i + 1);
161 min = Math.min(i + 1, k);
162 clause1.push(-literals.get(i));
163
164 binary = Integer.toBinaryString(i);
165 while (binary.length() != p) {
166 binary = "0" + binary;
167 }
168
169 for (int g = max - 1; g < min; g++) {
170 clause1.push(t[g][i]);
171 for (int j = 0; j < p; j++) {
172 clause2.push(-t[g][i]);
173 if (binary.charAt(j) == '0') {
174 clause2.push(-b[g][j]);
175 } else {
176 clause2.push(b[g][j]);
177 }
178 group.add(solver.addClause(clause2));
179 clause2.clear();
180 }
181 }
182 group.add(solver.addClause(clause1));
183 clause1.clear();
184 }
185
186 return group;
187 }
188
189 @Override
190 public IConstr addExactlyOne(ISolver solver, IVecInt literals)
191 throws ContradictionException {
192 ConstrGroup group = new ConstrGroup();
193
194 group.add(addAtLeastOne(solver, literals));
195 group.add(addAtMostOne(solver, literals));
196
197 return group;
198 }
199
200 @Override
201 public IConstr addExactly(ISolver solver, IVecInt literals, int degree)
202 throws ContradictionException {
203 ConstrGroup group = new ConstrGroup();
204
205 group.add(addAtLeast(solver, literals, degree));
206 group.add(addAtMost(solver, literals, degree));
207
208 return group;
209 }
210 }