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 }