backends/minisat/simp/SimpSolver.h

   1 /************************************************************************************[SimpSolver.h]
   2 MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
   3
   4 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
   5 associated documentation files (the "Software"), to deal in the Software without restriction,
   6 including without limitation the rights to use, copy, modify, merge, publish, distribute,
   7 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
   8 furnished to do so, subject to the following conditions:
   9
  10 The above copyright notice and this permission notice shall be included in all copies or
  11 substantial portions of the Software.
  12
  13 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  14 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  15 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  16 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  17 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  18 **************************************************************************************************/
  19
  20 #ifndef SimpSolver_h
  21 #define SimpSolver_h
  22
  23 #include <cstdio>
  24
  25 #include "Queue.h"
  26 #include "Solver.h"
  27
  28
  29 class SimpSolver : public Solver {
  30  public:
  31     // Constructor/Destructor:
  32     //
  33     SimpSolver();
  34     ~SimpSolver();
  35
  36     // Problem specification:
  37     //
  38     Var     newVar    (bool polarity = true, bool dvar = true);
  39     bool    addClause (vec<Lit>& ps);
  40
  41     // Variable mode:
  42     //
  43     void    setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
  44
  45     // Solving:
  46     //
  47     bool    solve     (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
  48     bool    solve     (bool do_simp = true, bool turn_off_simp = false);
  49     bool    eliminate (bool turn_off_elim = false);  // Perform variable elimination based simplification.
  50
  51     // Generate a (possibly simplified) DIMACS file:
  52     //
  53     void    toDimacs  (const char* file);
  54
  55     // Mode of operation:
  56     //
  57     int     grow;             // Allow a variable elimination step to grow by a number of clauses (default to zero).
  58     bool    asymm_mode;       // Shrink clauses by asymmetric branching.
  59     bool    redundancy_check; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
  60
  61     // Statistics:
  62     //
  63     int     merges;
  64     int     asymm_lits;
  65     int     remembered_clauses;
  66
  67 // protected:
  68   public:
  69
  70     // Helper structures:
  71     //
  72     struct ElimData {
  73         int          order;      // 0 means not eliminated, >0 gives an index in the elimination order
  74         vec<Clause*> eliminated;
  75         ElimData() : order(0) {} };
  76
  77     struct ElimOrderLt {
  78         const vec<ElimData>& elimtable;
  79         ElimOrderLt(const vec<ElimData>& et) : elimtable(et) {}
  80         bool operator()(Var x, Var y) { return elimtable[x].order > elimtable[y].order; } };
  81
  82     struct ElimLt {
  83         const vec<int>& n_occ;
  84         ElimLt(const vec<int>& no) : n_occ(no) {}
  85         int  cost      (Var x)        const { return n_occ[toInt(Lit(x))] * n_occ[toInt(~Lit(x))]; }
  86         bool operator()(Var x, Var y) const { return cost(x) < cost(y); } };
  87
  88
  89     // Solver state:
  90     //
  91     int                 elimorder;
  92     bool                use_simplification;
  93     vec<ElimData>       elimtable;
  94     vec<char>           touched;
  95     vec<vec<Clause*> >  occurs;
  96     vec<int>            n_occ;
  97     Heap<ElimLt>        elim_heap;
  98     Queue<Clause*>      subsumption_queue;
  99     vec<char>           frozen;
 100     int                 bwdsub_assigns;
 101
 102     // Temporaries:
 103     //
 104     Clause*             bwdsub_tmpunit;
 105
 106     // Main internal methods:
 107     //
 108     bool          asymm                    (Var v, Clause& c);
 109     bool          asymmVar                 (Var v);
 110     void          updateElimHeap           (Var v);
 111     void          cleanOcc                 (Var v);
 112     vec<Clause*>& getOccurs                (Var x);
 113     void          gatherTouchedClauses     ();
 114     bool          merge                    (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
 115     bool          merge                    (const Clause& _ps, const Clause& _qs, Var v);
 116     bool          backwardSubsumptionCheck (bool verbose = false);
 117     bool          eliminateVar             (Var v, bool fail = false);
 118     void          remember                 (Var v);
 119     void          extendModel              ();
 120     void          verifyModel              ();
 121
 122     void          removeClause             (Clause& c);
 123     bool          strengthenClause         (Clause& c, Lit l);
 124     void          cleanUpClauses           ();
 125     bool          implied                  (const vec<Lit>& c);
 126     void          toDimacs                 (FILE* f, Clause& c);
 127     bool          isEliminated             (Var v) const;
 128
 129 };
 130
 131
 132 //=================================================================================================
 133 // Implementation of inline methods:
 134
 135 inline void SimpSolver::updateElimHeap(Var v) {
 136     if (elimtable[v].order == 0)
 137         elim_heap.update(v); }
 138
 139 inline void SimpSolver::cleanOcc(Var v) {
 140     assert(use_simplification);
 141     Clause **begin = (Clause**)occurs[v];
 142     Clause **end = begin + occurs[v].size();
 143     Clause **i, **j;
 144     for (i = begin, j = end; i < j; i++)
 145         if ((*i)->mark() == 1){
 146             *i = *(--j);
 147             i--;
 148         }
 149     //occurs[v].shrink_(end - j);  // This seems slower. Why?!
 150     occurs[v].shrink(end - j);
 151 }
 152
 153 inline vec<Clause*>& SimpSolver::getOccurs(Var x) {
 154     cleanOcc(x); return occurs[x]; }
 155
 156 inline bool  SimpSolver::isEliminated (Var v) const { return v < elimtable.size() && elimtable[v].order != 0; }
 157 inline void  SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (b) { updateElimHeap(v); } }
 158 inline bool  SimpSolver::solve        (bool do_simp, bool turn_off_simp) { vec<Lit> tmp; return solve(tmp, do_simp, turn_off_simp); }
 159
 160 //=================================================================================================
 161 #endif