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 * delete a clause
91 */
92 void delete(int[] clause);
93
94 /**
95 * a conflict has been found.
96 *
97 * @param confl
98 * TODO
99 * @param dlevel
100 * TODO
101 * @param trailLevel
102 * TODO
103 *
104 */
105 void conflictFound(IConstr confl, int dlevel, int trailLevel);
106
107 /**
108 * a conflict has been found while propagating values.
109 *
110 * @param p
111 * the conflicting value.
112 */
113 void conflictFound(int p);
114
115 /**
116 * a solution is found.
117 *
118 * @param model
119 * the model found
120 *
121 */
122 void solutionFound(int[] model);
123
124 /**
125 * starts a propagation
126 */
127 void beginLoop();
128
129 /**
130 * Start the search.
131 *
132 */
133 void start();
134
135 /**
136 * End the search.
137 *
138 * @param result
139 * the result of the search.
140 */
141 void end(Lbool result);
142
143 /**
144 * The solver restarts the search.
145 */
146 void restarting();
147
148 /**
149 * The solver is asked to backjump to a given decision level.
150 *
151 * @param backjumpLevel
152 */
153 void backjump(int backjumpLevel);
154
155 /**
156 * The solver is going to delete some learned clauses.
157 */
158 void cleaning();
159 }