minisat_derivation.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file minisat_derivation.h
00004  *\brief MiniSat proof logging
00005  *
00006  * Author: Alexander Fuchs
00007  *
00008  * Created: Sun Dec 07 11:09:00 2007
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 #ifndef _cvc3__sat__minisat_derivation_h_
00022 #define _cvc3__sat__minisat_derivation_h_
00023 
00024 
00025 #include "minisat_types.h"
00026 #include <hash_map.h>
00027 #include <hash_set.h>
00028 #include <vector>
00029 #include <deque>
00030 #include <algorithm>
00031 #include <string>
00032 
00033 namespace MiniSat {
00034   // a resolution inference as a sequence of binary resolution steps
00035   class Inference {
00036   public:
00037     typedef std::vector<std::pair<Lit, int> > TSteps;
00038 
00039   private:
00040     // id of first clause
00041     int d_start;
00042 
00043     // binary resolution step:
00044     // result of previous step (or d_start)
00045     // on literal with next clause (given by id)
00046     TSteps d_steps;
00047 
00048   public:
00049     Inference(int clauseID) : d_start(clauseID) {};
00050 
00051     void add(Lit lit, int clauseID) {
00052       d_steps.push_back(std::make_pair(lit, clauseID));
00053     };
00054 
00055     void add(Lit lit, Clause* clause) {
00056       add(lit, clause->id());
00057     };
00058 
00059     int getStart() const {
00060       return d_start;
00061     }
00062 
00063     const TSteps& getSteps() const {
00064       return d_steps;
00065     }
00066 
00067     // returns steps as a lits: clauseId0 literal0.toString clauseID1 ...
00068     std::string toString() const;
00069   };
00070 
00071 
00072 
00073   class Solver;
00074 
00075   // Heavily based on the proof logging version of MiniSat (1.14p)
00076   //
00077   // Note: this implementation keeps the whole derivation in memory -
00078   // for many problems this is not feasible.
00079   // should provide an alternative implementation that logs the derivation
00080   // to a file and constructs the proof from it.
00081   class Derivation {
00082   public:
00083     typedef Hash::hash_map<int, Clause*> TClauses;
00084     typedef Hash::hash_set<int> TInputClauses;
00085     typedef Hash::hash_map<int, Inference*> TInferences;
00086 
00087   private:
00088     // mapping from id to clause
00089     TClauses d_clauses;
00090 
00091     // as an additional check, explicitely mark which clauses are input clauses
00092     // by adding their id to this set.
00093     //
00094     // as an invariant an id should be either in d_inferences or d_inputClauses,
00095     // as a clause does exactly have no inference attached if it is an input clause.
00096     TInputClauses d_inputClauses;
00097 
00098     // unit clauses derived with computeRootReason
00099     // mapping from index of literal to clause
00100     TClauses d_unitClauses;
00101 
00102     // mapping from clause id to the inference it was derived by
00103     TInferences d_inferences;
00104 
00105     // clauses removed from the solver
00106     std::deque<Clause*> d_removedClauses;
00107 
00108     // empty clause of derivation, if derived
00109     Clause* d_emptyClause;
00110 
00111   public:
00112     Derivation() : d_emptyClause(NULL) {};
00113     ~Derivation();
00114 
00115     // note: allow for duplicate insertion of clauses registerClause and registerInputClause,
00116     // as this can happen in the current implementation
00117     // for theory clauses which are inconsistent on insertion.
00118 
00119     // register a new clause
00120     void registerClause(Clause* clause) {
00121       // if clause with id does already exist,
00122       // then it must be the same clause wrt. its literals
00123       IF_DEBUG (
00124         if (d_clauses.contains(clause->id())) {
00125     Clause* old = d_clauses[clause->id()];
00126     DebugAssert(old->size() == clause->size(),
00127           "MiniSat::Derivation::registerClause: two clauses of different size registered with same id");
00128 
00129     std::vector<int> oldLiterals;
00130     for (int i = 0; i < old->size(); ++i) {
00131       oldLiterals.push_back((*old)[i].index());
00132     }
00133     
00134     std::vector<int> newLiterals;
00135     for (int i = 0; i < clause->size(); ++i) {
00136       newLiterals.push_back((*clause)[i].index());
00137     }
00138 
00139     std::sort(oldLiterals.begin(), oldLiterals.end());
00140     std::sort(newLiterals.begin(), newLiterals.end());
00141     for (std::vector<int>::size_type i = 0; i < oldLiterals.size(); ++i) {
00142       DebugAssert(oldLiterals[i] == newLiterals[i],
00143       "MiniSat::Derivation::registerClause: two clauses with different literals registered with same id");
00144     }
00145         }
00146       )
00147 
00148       d_clauses[clause->id()] = clause;
00149     };
00150 
00151     // mark clause as input clause, i.e. true without premises
00152     void registerInputClause(int clauseID) {
00153       d_inputClauses.insert(clauseID);
00154     };
00155 
00156     // clause has been removed from the solver or created internally in Derivation,
00157     // so store it here for later garbage collection.
00158     void removedClause(Clause* clause) {
00159       DebugAssert(clause != NULL, "MiniSat::derivation:removedClause: NULL");
00160       d_removedClauses.push_back(clause);
00161     };
00162 
00163     // register the inference of a clause; takes ownership of inference
00164     void registerInference(int clauseID, Inference* inference) {
00165       DebugAssert(!d_inferences.contains(clauseID),
00166       "MiniSat::Derivation::registerInference: inference for clauseID already registered");
00167       d_inferences[clauseID] = inference;
00168     };
00169 
00170     // implied is a literal that is implied at the root level.
00171     // return the id of the implying unit clause [literal], if it exists.
00172     //
00173     // otherwise derive it from its reasons and return the new clause id.
00174     // derived unit clauses are stored internally, independently of the Solver
00175     //
00176     // may resolve theory implications with Solver::resolveTheoryImplication
00177     int computeRootReason(Lit implied, Solver* solver);
00178 
00179 
00180     // register the empty clause (or a clause falsified in the root level)
00181     // showing that the clause set is unsatisfiable.
00182     //
00183     // if clause is not the empty clause, the empty clause is derived from it,
00184     // possible using computeRootReason
00185     void finish(Clause* clause, Solver* solver);
00186 
00187 
00188     // print the derivation of the given clause
00189     //
00190     // output is of the form:
00191     // ID D : L1 ... Ln : C1 K1 C2 K2 ... Cm
00192     // where:
00193     // ID - the id of a clause
00194     // D - 'I' for an input clause, 'D' for a clause derived from other clauses
00195     // Li - the clause literals
00196     // Ci Ki - the clause is derived from these clauses by binary resolution on the given literals
00197     //
00198     // factoring is done after each resolution step, i.e. duplicate literals are removed from the clause.
00199     //
00200     // example:
00201     // 3 D : +12 -2 -33 : 1 +10 2
00202     // says that the clause with the id 3 consists of the literals +12, -2, -33,
00203     // and was derived by resolution between the clauses with ids 1 and 2,
00204     // where the literal +10 is in clause 1 and -10 is in clause 2.
00205     //
00206     // for example, 1 may be the clause +12 +10 -2, and 2 may be -10 -2 -33,
00207     // which resolved on +10 yield the clause +12 -2 -2 -33,
00208     // which after factoring simplified to +12 -2 -33.
00209     void printProof(Clause* clause);
00210 
00211     // print the derivation of the empty clause.
00212     void printProof();
00213 
00214     // see Solver::push - clauseID is the highest currently used clause id
00215     void push(int clauseID);
00216 
00217     // see Solver::pop - clauseID corresponds to a clause id used in a push
00218     void pop(int clauseID);
00219   };
00220 }
00221 
00222 
00223 #endif

Generated on Tue Jul 3 14:33:37 2007 for CVC3 by  doxygen 1.5.1