CVC3

minisat_varorder.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file minisat_varorder.h
00004  *\brief MiniSat decision heuristics
00005  *
00006  * Author: Alexander Fuchs
00007  *
00008  * Created: Fri Sep 08 11:04:00 2006
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  */
00019 /*****************************************************************************/
00020 
00021 /**************************************************************************************[VarOrder.h]
00022 MiniSat -- Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson
00023 
00024 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
00025 associated documentation files (the "Software"), to deal in the Software without restriction,
00026 including without limitation the rights to use, copy, modify, merge, publish, distribute,
00027 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
00028 furnished to do so, subject to the following conditions:
00029 
00030 The above copyright notice and this permission notice shall be included in all copies or
00031 substantial portions of the Software.
00032 
00033 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
00034 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00035 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
00036 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
00037 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00038 **************************************************************************************************/
00039 
00040 #ifndef _cvc3__minisat__varorder_h_
00041 #define _cvc3__minisat__varorder_h_
00042 
00043 //=================================================================================================
00044 
00045 #include "minisat_types.h"
00046 #include "minisat_heap.h"
00047 #include <iostream>
00048 #include <vector>
00049 
00050 // implements the decision heuristics by using a heap over variable ids (which are ints)
00051 
00052 namespace MiniSat {
00053 
00054 struct VarOrder_lt {
00055   const std::vector<double>&  activity;
00056   bool operator () (Var x, Var y) { return activity[x] > activity[y]; }
00057   VarOrder_lt(const std::vector<double>&  act) : activity(act) { }
00058 };
00059 
00060 class VarOrder {
00061   const std::vector<signed char>&    assigns;     // var->val. Pointer to external assignment table.
00062   const std::vector<double>&  activity;    // var->act. Pointer to external activity table.
00063   Heap<VarOrder_lt>   heap;
00064   double              random_seed; // For the internal random number generator
00065 
00066 public:
00067   VarOrder(const std::vector<signed char>& ass, const std::vector<double>& act) :
00068     assigns(ass), activity(act), heap(VarOrder_lt(act)), random_seed(91648253)
00069   { }
00070 
00071     inline void newVar(void);
00072     inline void newVar(int varIndex);
00073     inline void update(Var x);                  // Called when variable increased in activity.
00074     inline void undo(Var x);                    // Called when variable is unassigned and may be selected again.
00075     inline Var  select(double random_freq =.0); // Selects a new, unassigned variable (or 'var_Undef' if none exists).
00076 };
00077 
00078 
00079 void VarOrder::newVar(void)
00080 {
00081     heap.setBounds(assigns.size());
00082     heap.insert(assigns.size()-1);
00083 }
00084 
00085 void VarOrder::newVar(int varIndex)
00086 {
00087     heap.setBounds(assigns.size());
00088     heap.insert(varIndex);
00089 }
00090 
00091 void VarOrder::update(Var x)
00092 {
00093     if (heap.inHeap(x))
00094         heap.increase(x);
00095 }
00096 
00097 void VarOrder::undo(Var x)
00098 {
00099     if (!heap.inHeap(x))
00100         heap.insert(x);
00101 }
00102 
00103 
00104 Var VarOrder::select(double random_var_freq)
00105 {
00106   // Random decision:
00107   /*
00108     if (drand(random_seed) < random_var_freq && !heap.empty()){
00109     Var next = irand(random_seed,assigns.size());
00110     
00111     // find var which is not undefined or in the heap
00112     while (toLbool(assigns[next]) == l_Undef && !heap.inHeap(next)) {
00113     next = irand(random_seed,assigns.size());
00114     }
00115     if (toLbool(assigns[next]) == l_Undef) {
00116     return next;
00117     }
00118 
00119     // cvc does not necessarily use all variable ids without gaps,
00120     // so need to check if the picked id is a valid variable.
00121     //if (toLbool(assigns[next]) == l_Undef && heap.inHeap(next)) {
00122     //    return next;
00123     //}
00124     }
00125   */
00126   
00127   // Activity based decision:
00128   while (!heap.empty()){
00129     Var next = heap.getMin();
00130     if (toLbool(assigns[next]) == l_Undef)
00131       return next;
00132   }
00133   
00134   return var_Undef;
00135 }
00136 
00137 }
00138 
00139 //=================================================================================================
00140 #endif