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.specs;
31
32 /**
33 * The aim on that interface is to allow power users to communicate with the SAT
34 * solver using Dimacs format. That way, there is no need to know the internals
35 * of the solver.
36 *
37 * @author leberre
38 * @since 2.3.2
39 */
40 public interface ISolverService {
41
42 /**
43 * Ask the SAT solver to stop the search.
44 */
45 void stop();
46
47 /**
48 * Ask the SAT solver to backtrack. It is mandatory to provide a reason for
49 * backtracking, in terms of literals (which should be falsified under
50 * current assignment). The reason is not added to the clauses of the
51 * solver: only the result of the analysis is stored in the learned clauses.
52 * Note that these clauses may be removed latter.
53 *
54 * @param reason
55 * a set of literals, in Dimacs format, currently falsified, i.e.
56 * for (int l : reason) assert truthValue(l) == Lbool.FALSE
57 */
58 void backtrack(int[] reason);
59
60 /**
61 * Add a new clause in the SAT solver. The new clause may contain new
62 * variables. The clause may be falsified, in that case, the difference with
63 * backtrack() is that the new clause is appended to the solver as a regular
64 * clause. Thus it will not be removed by aggressive clause deletion. The
65 * clause may be assertive at a given decision level. In that case, the
66 * solver should backtrack to the proper decision level. In other cases, the
67 * search should simply proceed.
68 *
69 * @param literals
70 * a set of literals in Dimacs format.
71 */
72 IConstr addClauseOnTheFly(int[] literals);
73
74 /**
75 * Add a new pseudo cardinality constraint sum literals <= degree in the
76 * solver. The constraint must be falsified under current assignment.
77 *
78 * @param literals
79 * a set of literals in Dimacs format.
80 * @param degree
81 * the maximal number of literals which can be satisfied.
82 */
83 IConstr addAtMostOnTheFly(int[] literals, int degree);
84
85 /**
86 * To access the truth value of a specific literal under current assignment.
87 *
88 * @param literal
89 * a Dimacs literal, i.e. a non-zero integer.
90 * @return true or false if the literal is assigned, else undefined.
91 */
92 Lbool truthValue(int literal);
93
94 /**
95 * To access the current decision level
96 */
97 int currentDecisionLevel();
98
99 /**
100 * To access the literals propagated at a specific decision level.
101 *
102 * @param decisionLevel
103 * a decision level between 0 and #currentDecisionLevel()
104 */
105 int[] getLiteralsPropagatedAt(int decisionLevel);
106
107 /**
108 * Suggests to the SAT solver to branch next on the given literal.
109 *
110 * @param l
111 * a literal in Dimacs format.
112 */
113 void suggestNextLiteralToBranchOn(int l);
114
115 /**
116 * Read-Only access to the value of the heuristics for each variable. Note
117 * that for efficiency reason, the real array storing the value of the
118 * heuristics is returned. DO NOT CHANGE THE VALUES IN THAT ARRAY.
119 *
120 * @return the value of the heuristics for each variable (using Dimacs
121 * index).
122 */
123 double[] getVariableHeuristics();
124
125 /**
126 * Read-Only access to the list of constraints learned and not deleted so
127 * far in the solver. Note that for efficiency reason, the real list of
128 * constraints managed by the solver is returned. DO NOT MODIFY THAT LIST
129 * NOR ITS CONSTRAINTS.
130 *
131 * @return the constraints learned and kept so far by the solver.
132 */
133 IVec<? extends IConstr> getLearnedConstraints();
134
135 /**
136 * Read-Only access to the number of variables declared in the solver.
137 *
138 * @return the maximum variable id (Dimacs format) reserved in the solver.
139 */
140 int nVars();
141
142 /**
143 * Remove a constraint returned by one of the add method from the solver
144 * that is subsumed by a constraint already in the solver or to be added to
145 * the solver.
146 *
147 * Unlike the removeConstr() method, learned clauses will NOT be cleared.
148 *
149 * That method is expected to be used to remove constraints used in the
150 * optimization process.
151 *
152 * In order to prevent a wrong from the user, the method will only work if
153 * the argument is the last constraint added to the solver. An illegal
154 * argument exception will be thrown in other cases.
155 *
156 * @param c
157 * a constraint returned by one of the add method. It must be the
158 * latest constr added to the solver.
159 * @return true if the constraint was successfully removed.
160 */
161 boolean removeSubsumedConstr(IConstr c);
162
163 /**
164 *
165 * @return the string used to prefix the output.
166 * @since 2.3.3
167 */
168 String getLogPrefix();
169 }