View Javadoc

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