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 package org.sat4j.tools;
31
32 import org.sat4j.core.VecInt;
33 import org.sat4j.specs.ContradictionException;
34 import org.sat4j.specs.ISolver;
35 import org.sat4j.specs.IVecInt;
36 import org.sat4j.specs.TimeoutException;
37
38 /**
39 * That class allows to iterate through all the models (implicants) of a
40 * formula.
41 *
42 * <pre>
43 * ISolver solver = new ModelIterator(SolverFactory.OneSolver());
44 * boolean unsat = true;
45 * while (solver.isSatisfiable()) {
46 * unsat = false;
47 * int[] model = solver.model();
48 * // do something with model
49 * }
50 * if (unsat) {
51 * // UNSAT case
52 * }
53 * </pre>
54 *
55 * It is also possible to limit the number of models returned:
56 *
57 * <pre>
58 * ISolver solver = new ModelIterator(SolverFactory.OneSolver(), 10);
59 * </pre>
60 *
61 * will return at most 10 models.
62 *
63 * @author leberre
64 */
65 public class ModelIterator extends SolverDecorator<ISolver> {
66
67 private static final long serialVersionUID = 1L;
68
69 private boolean trivialfalsity = false;
70 private final long bound;
71 private long nbModelFound = 0;
72
73 /**
74 * Create an iterator over the solutions available in <code>solver</code>.
75 * The iterator will look for one new model at each call to isSatisfiable()
76 * and will discard that model at each call to model().
77 *
78 * @param solver
79 * a solver containing the constraints to satisfy.
80 * @see #isSatisfiable()
81 * @see #isSatisfiable(boolean)
82 * @see #isSatisfiable(IVecInt)
83 * @see #isSatisfiable(IVecInt, boolean)
84 * @see #model()
85 */
86 public ModelIterator(ISolver solver) {
87 this(solver, Long.MAX_VALUE);
88 }
89
90 /**
91 * Create an iterator over a limited number of solutions available in
92 * <code>solver</code>. The iterator will look for one new model at each
93 * call to isSatisfiable() and will discard that model at each call to
94 * model(). At most <code>bound</code> calls to models() will be allowed
95 * before the method <code>isSatisfiable()</code> returns false.
96 *
97 * @param solver
98 * a solver containing the constraints to satisfy.
99 * @param bound
100 * the maximum number of models to return.
101 * @since 2.1
102 * @see #isSatisfiable()
103 * @see #isSatisfiable(boolean)
104 * @see #isSatisfiable(IVecInt)
105 * @see #isSatisfiable(IVecInt, boolean)
106 * @see #model()
107 */
108 public ModelIterator(ISolver solver, long bound) {
109 super(solver);
110 this.bound = bound;
111 }
112
113 /*
114 * (non-Javadoc)
115 *
116 * @see org.sat4j.ISolver#model()
117 */
118 @Override
119 public int[] model() {
120 int[] last = super.model();
121 this.nbModelFound++;
122 IVecInt clause = new VecInt(last.length);
123 for (int q : last) {
124 clause.push(-q);
125 }
126 try {
127 addBlockingClause(clause);
128 } catch (ContradictionException e) {
129 this.trivialfalsity = true;
130 }
131 return last;
132 }
133
134 /*
135 * (non-Javadoc)
136 *
137 * @see org.sat4j.ISolver#isSatisfiable()
138 */
139 @Override
140 public boolean isSatisfiable() throws TimeoutException {
141 if (this.trivialfalsity || this.nbModelFound >= this.bound) {
142 return false;
143 }
144 this.trivialfalsity = false;
145 return super.isSatisfiable(true);
146 }
147
148 /*
149 * (non-Javadoc)
150 *
151 * @see org.sat4j.ISolver#isSatisfiable(org.sat4j.datatype.VecInt)
152 */
153 @Override
154 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
155 if (this.trivialfalsity || this.nbModelFound >= this.bound) {
156 return false;
157 }
158 this.trivialfalsity = false;
159 return super.isSatisfiable(assumps, true);
160 }
161
162 /*
163 * (non-Javadoc)
164 *
165 * @see org.sat4j.ISolver#reset()
166 */
167 @Override
168 public void reset() {
169 this.trivialfalsity = false;
170 this.nbModelFound = 0;
171 super.reset();
172 }
173
174 @Override
175 public int[] primeImplicant() {
176 int[] last = super.primeImplicant();
177 this.nbModelFound += Math.pow(2, nVars() - last.length);
178 IVecInt clause = new VecInt(last.length);
179 for (int q : last) {
180 clause.push(-q);
181 }
182 try {
183 addBlockingClause(clause);
184 } catch (ContradictionException e) {
185 this.trivialfalsity = true;
186 }
187 return last;
188 }
189
190 /**
191 * To know the number of models already found.
192 *
193 * @return the number of models found so far.
194 * @since 2.3
195 */
196 public long numberOfModelsFoundSoFar() {
197 return this.nbModelFound;
198 }
199 }