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 import java.io.Serializable;
33
34 /**
35 * Interface to the solver main steps. Useful for integrating search
36 * visualization or debugging.
37 *
38 * (that class moved from org.sat4j.minisat.core in earlier version of SAT4J).
39 *
40 * @author daniel
41 * @since 2.1
42 */
43 public interface SearchListener<S extends ISolverService> extends Serializable {
44
45 /**
46 * Provide access to the solver's controllable interface.
47 *
48 * @param solverService
49 * a way to safely control the solver.
50 * @since 2.3.2
51 */
52 void init(S solverService);
53
54 /**
55 * decision variable
56 *
57 * @param p
58 */
59 void assuming(int p);
60
61 /**
62 * Unit propagation
63 *
64 * @param p
65 * @param reason
66 * TODO
67 */
68 void propagating(int p, IConstr reason);
69
70 /**
71 * backtrack on a decision variable
72 *
73 * @param p
74 */
75 void backtracking(int p);
76
77 /**
78 * adding forced variable (conflict driven assignment)
79 */
80 void adding(int p);
81
82 /**
83 * learning a new clause
84 *
85 * @param c
86 */
87 void learn(IConstr c);
88
89 /**
90 * learn a new unit clause (a literal)
91 *
92 * @param p
93 * a literal in Dimacs format.
94 * @since 2.3.4
95 */
96 void learnUnit(int p);
97
98 /**
99 * delete a clause
100 */
101 void delete(int[] clause);
102
103 /**
104 * a conflict has been found.
105 *
106 * @param confl
107 * TODO
108 * @param dlevel
109 * TODO
110 * @param trailLevel
111 * TODO
112 *
113 */
114 void conflictFound(IConstr confl, int dlevel, int trailLevel);
115
116 /**
117 * a conflict has been found while propagating values.
118 *
119 * @param p
120 * the conflicting value.
121 */
122 void conflictFound(int p);
123
124 /**
125 * a solution is found.
126 *
127 * @param model
128 * the model found
129 * @param lazyModel
130 * TODO
131 *
132 */
133 void solutionFound(int[] model, RandomAccessModel lazyModel);
134
135 /**
136 * starts a propagation
137 */
138 void beginLoop();
139
140 /**
141 * Start the search.
142 *
143 */
144 void start();
145
146 /**
147 * End the search.
148 *
149 * @param result
150 * the result of the search.
151 */
152 void end(Lbool result);
153
154 /**
155 * The solver restarts the search.
156 */
157 void restarting();
158
159 /**
160 * The solver is asked to backjump to a given decision level.
161 *
162 * @param backjumpLevel
163 */
164 void backjump(int backjumpLevel);
165
166 /**
167 * The solver is going to delete some learned clauses.
168 */
169 void cleaning();
170 }