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 void addClause(int[] literals);
73
74 /**
75 * To access the truth value of a specific literal under current assignment.
76 *
77 * @param literal
78 * a Dimacs literal, i.e. a non-zero integer.
79 * @return true or false if the literal is assigned, else undefined.
80 */
81 Lbool truthValue(int literal);
82
83 /**
84 * To access the current decision level
85 */
86 int currentDecisionLevel();
87
88 /**
89 * To access the literals propagated at a specific decision level.
90 *
91 * @param decisionLevel
92 * a decision level between 0 and #currentDecisionLevel()
93 */
94 int[] getLiteralsPropagatedAt(int decisionLevel);
95
96 /**
97 * Suggests to the SAT solver to branch next on the given literal.
98 *
99 * @param l
100 * a literal in Dimacs format.
101 */
102 void suggestNextLiteralToBranchOn(int l);
103
104 /**
105 * Read-Only access to the value of the heuristics for each variable. Note
106 * that for efficiency reason, the real array storing the value of the
107 * heuristics is returned. DO NOT CHANGE THE VALUES IN THAT ARRAY.
108 *
109 * @return the value of the heuristics for each variable (using Dimacs
110 * index).
111 */
112 double[] getVariableHeuristics();
113
114 /**
115 * Read-Only access to the list of constraints learned and not deleted so
116 * far in the solver. Note that for efficiency reason, the real list of
117 * constraints managed by the solver is returned. DO NOT MODIFY THAT LIST
118 * NOR ITS CONSTRAINTS.
119 *
120 * @return the constraints learned and kept so far by the solver.
121 */
122 IVec<? extends IConstr> getLearnedConstraints();
123
124 /**
125 * Read-Only access to the number of variables declared in the solver.
126 *
127 * @return the maximum variable id (Dimacs format) reserved in the solver.
128 */
129 int nVars();
130 }