1 /******************************************************************************* 2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre 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 *******************************************************************************/ 28 package org.sat4j.minisat.core; 29 30 import java.io.Serializable; 31 32 /** 33 * Interface to the solver main steps. Useful for integrating search 34 * visualization or debugging. 35 * 36 * @author daniel 37 * 38 */ 39 public interface SearchListener extends Serializable { 40 41 /** 42 * decision variable 43 * 44 * @param p 45 */ 46 void assuming(int p); 47 48 /** 49 * Unit propagation 50 * 51 * @param p 52 */ 53 void propagating(int p); 54 55 /** 56 * backtrack on a decision variable 57 * 58 * @param p 59 */ 60 void backtracking(int p); 61 62 /** 63 * adding forced variable (conflict driven assignment) 64 */ 65 void adding(int p); 66 67 /** 68 * learning a new clause 69 * 70 * @param c 71 */ 72 void learn(Constr c); 73 74 /** 75 * delete a clause 76 */ 77 void delete(int[] clause); 78 79 /** 80 * a conflict has been found. 81 * 82 */ 83 void conflictFound(); 84 85 /** 86 * a solution is found. 87 * 88 */ 89 void solutionFound(); 90 91 /** 92 * starts a propagation 93 */ 94 void beginLoop(); 95 96 /** 97 * Start the search. 98 * 99 */ 100 void start(); 101 102 /** 103 * End the search. 104 * 105 * @param result 106 * the result of the search. 107 */ 108 void end(Lbool result); 109 }