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.PrintWriter; 28 29 /** 30 * Interface for the variable ordering heuristics. It has both the 31 * responsibility to choose the next variable to branch on and the phase of the 32 * literal (positive or negative one). 33 * 34 * @author daniel 35 * 36 */ 37 public interface IOrder<L extends ILits> { 38 39 /** 40 * Method used to provide an easy access the the solver vocabulary. 41 * 42 * @param lits 43 * the vocabulary 44 */ 45 void setLits(L lits); 46 47 /** 48 * Method called each time Solver.newVar() is called. 49 * 50 */ 51 @Deprecated 52 void newVar(); 53 54 /** 55 * Method called when Solver.newVar(int) is called. 56 * 57 * @param howmany 58 * the maximum number of variables 59 * @see Solver#newVar(int) 60 */ 61 void newVar(int howmany); 62 63 /** 64 * Selects the next "best" unassigned literal. 65 * 66 * Note that it means selecting the best variable and the phase to branch on 67 * first. 68 * 69 * @return an unassigned literal or Lit.UNDEFINED no such literal exists. 70 */ 71 int select(); 72 73 /** 74 * Method called when a variable is unassigned. 75 * 76 * It is useful to add back a variable in the pool of variables to order. 77 * 78 * @param x 79 * a variable. 80 */ 81 void undo(int x); 82 83 /** 84 * To be called when the activity of a literal changed. 85 * 86 * @param p 87 * a literal. The associated variable will be updated. 88 */ 89 void updateVar(int p); 90 91 /** 92 * that method has the responsibility to initialize all arrays in the 93 * heuristics. PLEASE CALL super.init() IF YOU OVERRIDE THAT METHOD. 94 */ 95 void init(); 96 97 /** 98 * Display statistics regarding the heuristics. 99 * 100 * @param out 101 * the writer to display the information in 102 * @param prefix 103 * to be used in front of each newline. 104 */ 105 void printStat(PrintWriter out, String prefix); 106 107 /** 108 * Sets the variable activity decay as a growing factor for the next 109 * variable activity. 110 * 111 * @param d 112 * a number bigger than 1 that will increase the activity of the 113 * variables involved in future conflict. This is similar but 114 * more efficient than decaying all the activities by a similar 115 * factor. 116 */ 117 void setVarDecay(double d); 118 119 /** 120 * Decay the variables activities. 121 * 122 */ 123 void varDecayActivity(); 124 125 /** 126 * To obtain the current activity of a variable. 127 * 128 * @param p 129 * a literal 130 * @return the activity of the variable associated to that literal. 131 */ 132 double varActivity(int p); 133 134 /** 135 * indicate that a literal has been satisfied. 136 * 137 * @param p 138 */ 139 void assignLiteral(int p); 140 }