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 26 package org.sat4j.minisat.core; 27 28 /** 29 * Interface providing the unit propagation capability. 30 * 31 * @author leberre 32 */ 33 public interface UnitPropagationListener { 34 35 /** 36 * satisfies a literal 37 * 38 * @param p 39 * a literal 40 * @return true if the assignment looks possible, false if a conflict 41 * occurs. 42 */ 43 public abstract boolean enqueue(int p); 44 45 /** 46 * satisfies a literal 47 * 48 * @param p 49 * a literal 50 * @param from 51 * a reason explaining why p should be satisfied. 52 * @return true if the assignment looks possible, false if a conflict 53 * occurs. 54 */ 55 public abstract boolean enqueue(int p, Constr from); 56 }