1 /*
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3 *
4 * Based on the original minisat specification from:
5 *
6 * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7 * Sixth International Conference on Theory and Applications of Satisfiability
8 * Testing, LNCS 2919, pp 502-518, 2003.
9 *
10 * This library is free software; you can redistribute it and/or modify it under
11 * the terms of the GNU Lesser General Public License as published by the Free
12 * Software Foundation; either version 2.1 of the License, or (at your option)
13 * any later version.
14 *
15 * This library is distributed in the hope that it will be useful, but WITHOUT
16 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17 * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18 * details.
19 *
20 * You should have received a copy of the GNU Lesser General Public License
21 * along with this library; if not, write to the Free Software Foundation, Inc.,
22 * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23 *
24 */
25 package org.sat4j.minisat.core;
26
27 import java.io.Serializable;
28
29 /**
30 * Interface to the solver main steps. Useful for integrating search
31 * visualization or debugging.
32 *
33 * @author daniel
34 *
35 */
36 public interface SearchListener extends Serializable {
37
38 /**
39 * decision variable
40 *
41 * @param p
42 */
43 void assuming(int p);
44
45 /**
46 * Unit propagation
47 *
48 * @param p
49 */
50 void propagating(int p);
51
52 /**
53 * backtrack on a decision variable
54 *
55 * @param p
56 */
57 void backtracking(int p);
58
59 /**
60 * adding forced variable (conflict driven assignment)
61 */
62 void adding(int p);
63
64 /**
65 * learning a new clause
66 *
67 * @param c
68 */
69 void learn(Constr c);
70
71 /**
72 * delete a clause
73 */
74 void delete(int[] clause);
75
76 /**
77 * a conflict has been found.
78 *
79 */
80 void conflictFound();
81
82 /**
83 * a solution is found.
84 *
85 */
86 void solutionFound();
87
88 /**
89 * starts a propagation
90 */
91 void beginLoop();
92
93 /**
94 * Start the search.
95 *
96 */
97 void start();
98
99 /**
100 * End the search.
101 *
102 * @param result
103 * the result of the search.
104 */
105 void end(Lbool result);
106 }