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.tools;
26
27 import org.sat4j.core.VecInt;
28 import org.sat4j.specs.ContradictionException;
29 import org.sat4j.specs.IConstr;
30 import org.sat4j.specs.ISolver;
31 import org.sat4j.specs.IVecInt;
32 import org.sat4j.specs.TimeoutException;
33
34 /**
35 * This solver decorator allows to detect whether or not the set of constraints
36 * available in the solver has only one solution or not.
37 *
38 * NOTE THAT THIS DECORATOR CANNOT BE USED WITH SOLVERS USING SPECIFIC DATA
39 * STRUCTURES FOR BINARY OR TERNARY CLAUSES!
40 *
41 * <code>
42 SingleSolutionDetector problem =
43 new SingleSolutionDetector(SolverFactory.newMiniSAT());
44 // feed problem/solver as usual
45
46 if (problem.isSatisfiable()) {
47 if (problem.hasASingleSolution()) {
48 // great, the instance has a unique solution
49 int [] uniquesolution = problem.getModel();
50 } else {
51 // too bad, got more than one
52 }
53 }
54 * </code>
55 *
56 * @author leberre
57 *
58 */
59 public class SingleSolutionDetector extends SolverDecorator {
60
61 /**
62 *
63 */
64 private static final long serialVersionUID = 1L;
65
66 public SingleSolutionDetector(ISolver solver) {
67 super(solver);
68 }
69
70 /**
71 * Please use that method only after a positive answer from isSatisfiable()
72 * (else a runtime exception will be launched).
73 *
74 * @return true iff there is only one way to satisfy all the constraints in
75 * the solver.
76 * @throws TimeoutException
77 */
78 public boolean hasASingleSolution() throws TimeoutException {
79 return hasASingleSolution(new VecInt());
80 }
81
82 /**
83 * Please use that method only after a positive answer from
84 * isSatisfiable(assumptions) (else a runtime exception will be launched).
85 *
86 * @param assumptions
87 * a set of literals (dimacs numbering) that must be satisfied.
88 * @return true iff there is only one way to satisfy all the constraints in
89 * the solver using the provided set of assumptions.
90 * @throws TimeoutException
91 */
92 public boolean hasASingleSolution(IVecInt assumptions)
93 throws TimeoutException {
94 int[] firstmodel = model();
95 assert firstmodel != null;
96 IVecInt clause = new VecInt(firstmodel.length);
97 for (int q : firstmodel) {
98 clause.push(-q);
99 }
100 boolean result = false;
101 try {
102 IConstr added = addClause(clause);
103 result = !isSatisfiable(assumptions);
104 removeConstr(added);
105 } catch (ContradictionException e) {
106 result = true;
107 }
108 return result;
109 }
110 }