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 java.util.ArrayList;
33 import java.util.Arrays;
34 import java.util.List;
35
36 import org.sat4j.core.ASolverFactory;
37 import org.sat4j.core.VecInt;
38 import org.sat4j.specs.ContradictionException;
39 import org.sat4j.specs.ISolver;
40 import org.sat4j.specs.IVecInt;
41 import org.sat4j.specs.TimeoutException;
42
43 public class CheckMUSSolutionListener implements SolutionFoundListener {
44
45 private List<IVecInt> clauses;
46
47 private String explain;
48
49 // public CheckThatItIsAMUS(List<IVecInt> clauses) {
50 // this.clauses = clauses;
51 // }
52 private final ASolverFactory<? extends ISolver> factory;
53
54 public CheckMUSSolutionListener(ASolverFactory<? extends ISolver> factory) {
55 this.clauses = new ArrayList<IVecInt>();
56 this.factory = factory;
57 }
58
59 // public void setOriginalClauses(List<IVecInt> clauses) {
60 // this.clauses = clauses;
61 // }
62
63 public void addOriginalClause(IVecInt clause) {
64 IVecInt newClause = new VecInt(clause.size());
65 if (clauses == null) {
66 this.clauses = new ArrayList<IVecInt>();
67 }
68 clause.copyTo(newClause);
69 clauses.add(newClause);
70 }
71
72 /**
73 *
74 * @param mus
75 * containing the clauses identifiers
76 * @param clauses
77 * the original set of clauses
78 * @return
79 */
80 public boolean checkThatItIsAMUS(IVecInt mus) {
81 boolean result = false;
82
83 ISolver solver = factory.defaultSolver();
84
85 try {
86 for (int i = 0; i < mus.size(); i++) {
87 solver.addClause(clauses.get(mus.get(i) - 1));
88 }
89
90 result = !solver.isSatisfiable();
91
92 if (!result) {
93 explain = "The set of clauses in the MUS is SAT : "
94 + Arrays.toString(solver.model());
95 return result;
96 }
97
98 } catch (ContradictionException e) {
99 result = true;
100 } catch (TimeoutException e) {
101 e.printStackTrace();
102 }
103
104 try {
105 for (int i = 0; i < mus.size(); i++) {
106 solver = factory.defaultSolver();
107 for (int j = 0; j < mus.size(); j++) {
108 if (j != i) {
109 solver.addClause(clauses.get(mus.get(j) - 1));
110 }
111 }
112 result = result && solver.isSatisfiable();
113 if (!result) {
114 explain = "The subset of clauses in the MUS not containing clause "
115 + (i + 1)
116 + " is SAT : "
117 + Arrays.toString(solver.model());
118 return result;
119 }
120 }
121 } catch (ContradictionException e) {
122 result = false;
123 } catch (TimeoutException e) {
124 e.printStackTrace();
125 }
126
127 return result;
128
129 }
130
131 public void onSolutionFound(int[] solution) {
132
133 }
134
135 public void onSolutionFound(IVecInt solution) {
136 if (checkThatItIsAMUS(solution)) {
137 System.out.println(solution + " is a MUS");
138 } else {
139 System.out.println(solution + " is not a MUS \n" + explain);
140 }
141 }
142
143 public void onUnsatTermination() {
144 // do nothing
145 }
146 }