|
|||||||||||||||||||
Source file | Conditionals | Statements | Methods | TOTAL | |||||||||||||||
SingleSolutionDetector.java | - | 92,3% | 100% | 93,8% |
|
1 | package org.sat4j.tools; | |
2 | ||
3 | import org.sat4j.core.VecInt; | |
4 | import org.sat4j.specs.ContradictionException; | |
5 | import org.sat4j.specs.IConstr; | |
6 | import org.sat4j.specs.ISolver; | |
7 | import org.sat4j.specs.IVecInt; | |
8 | import org.sat4j.specs.TimeoutException; | |
9 | ||
10 | /** | |
11 | * This solver decorator allows to detect whether or not the set of constraints | |
12 | * available in the solver has only one solution or not. | |
13 | * | |
14 | * NOTE THAT THIS DECORATOR CANNOT BE USED WITH SOLVERS USING SPECIFIC | |
15 | * DATA STRUCTURES FOR BINARY OR TERNARY CLAUSES! | |
16 | * | |
17 | * <code> | |
18 | SingleSolutionDetector problem = | |
19 | new SingleSolutionDetector(SolverFactory.newMiniSAT()); | |
20 | // feed problem/solver as usual | |
21 | ||
22 | if (problem.isSatisfiable()) { | |
23 | if (problem.hasASingleSolution()) { | |
24 | // great, the instance has a unique solution | |
25 | int [] uniquesolution = problem.getModel(); | |
26 | } else { | |
27 | // too bad, got more than one | |
28 | } | |
29 | } | |
30 | * </code> | |
31 | * @author leberre | |
32 | * | |
33 | */ | |
34 | public class SingleSolutionDetector extends SolverDecorator { | |
35 | ||
36 | /** | |
37 | * | |
38 | */ | |
39 | private static final long serialVersionUID = 1L; | |
40 | ||
41 | 2 | public SingleSolutionDetector(ISolver solver) { |
42 | 2 | super(solver); |
43 | } | |
44 | ||
45 | /** | |
46 | * Please use that method only after a positive answer from | |
47 | * isSatisfiable() (else a runtime exception will be launched). | |
48 | * | |
49 | * @return true iff there is only one way to satisfy all the constraints | |
50 | * in the solver. | |
51 | * @throws TimeoutException | |
52 | */ | |
53 | 3 | public boolean hasASingleSolution() throws TimeoutException { |
54 | 3 | return hasASingleSolution(new VecInt()); |
55 | } | |
56 | ||
57 | /** | |
58 | * Please use that method only after a positive answer from | |
59 | * isSatisfiable(assumptions) (else a runtime exception will be launched). | |
60 | * | |
61 | * @param assumptions a set of literals (dimacs numbering) that must be | |
62 | * satisfied. | |
63 | * @return true iff there is only one way to satisfy all the constraints | |
64 | * in the solver using the provided set of assumptions. | |
65 | * @throws TimeoutException | |
66 | */ | |
67 | 6 | public boolean hasASingleSolution(IVecInt assumptions) |
68 | throws TimeoutException { | |
69 | 6 | int [] firstmodel = model(); |
70 | assert firstmodel != null; | |
71 | 4 | IVecInt clause = new VecInt(firstmodel.length); |
72 | 4 | for (int q : firstmodel) { |
73 | 8 | clause.push(-q); |
74 | } | |
75 | 4 | boolean result = false; |
76 | 4 | try { |
77 | 4 | IConstr added = addClause(clause); |
78 | 4 | result = !isSatisfiable(assumptions); |
79 | 4 | removeConstr(added); |
80 | } catch (ContradictionException e) { | |
81 | 0 | result = true; |
82 | } | |
83 | 4 | return result; |
84 | } | |
85 | } |
|