CVC3
minisat_derivation.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file minisat_derivation.h
4  *\brief MiniSat proof logging
5  *
6  * Author: Alexander Fuchs
7  *
8  * Created: Sun Dec 07 11:09:00 2007
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__sat__minisat_derivation_h_
22 #define _cvc3__sat__minisat_derivation_h_
23 
24 
25 #include "minisat_types.h"
26 #include <hash_map.h>
27 #include <hash_set.h>
28 #include <set>
29 #include <vector>
30 #include <deque>
31 #include <algorithm>
32 #include <string>
33 
34 namespace SAT {
35  class SatProof;
36 }
37 
38 namespace MiniSat {
39  // a resolution inference as a sequence of binary resolution steps
40  class Inference {
41  public:
42  typedef std::vector<std::pair<Lit, int> > TSteps;
43 
44  private:
45  // id of first clause
46  int d_start;
47 
48  // binary resolution step:
49  // result of previous step (or d_start)
50  // on literal with next clause (given by id)
52 
53  public:
54  Inference(int clauseID) : d_start(clauseID) {
55  // std::cout << "Start inference: " << clauseID << std::endl;
56  };
57 
58  void add(Lit lit, int clauseID) {
59  d_steps.push_back(std::make_pair(lit, clauseID));
60  };
61 
62  void add(Lit lit, Clause* clause) {
63  add(lit, clause->id());
64  };
65 
66  int getStart() const {
67  return d_start;
68  }
69 
70  const TSteps& getSteps() const {
71  return d_steps;
72  }
73 
74  // returns steps as a lits: clauseId0 literal0.toString clauseID1 ...
75  std::string toString() const;
76  };
77 
78 
79  class Solver;
80 
81  // Heavily based on the proof logging version of MiniSat (1.14p)
82  //
83  // Note: this implementation keeps the whole derivation in memory -
84  // for many problems this is not feasible.
85  // should provide an alternative implementation that logs the derivation
86  // to a file and constructs the proof from it.
87  class Derivation {
88  public:
92 
93  private:
94  // mapping from id to clause
96 
97  // as an additional check, explicitely mark which clauses are input clauses
98  // by adding their id to this set.
99  //
100  // as an invariant an id should be either in d_inferences or d_inputClauses,
101  // as a clause does exactly have no inference attached if it is an input clause.
103 
104  // unit clauses derived with computeRootReason
105  // mapping from index of literal to clause
107 
108  // mapping from clause id to the inference it was derived by
110 
111  // clauses removed from the solver
112  std::deque<Clause*> d_removedClauses;
113 
114  // empty clause of derivation, if derived
116 
117  public:
118  Derivation() : d_emptyClause(NULL) {};
119  ~Derivation();
120 
121  // note: allow for duplicate insertion of clauses registerClause and registerInputClause,
122  // as this can happen in the current implementation
123  // for theory clauses which are inconsistent on insertion.
124 
125  // register a new clause
126  void registerClause(Clause* clause) {
127  // std::cout << "register clause : " << clause->id() << " : " << clause->toString() << std::endl;
128 
129  //IF_DEBUG (
130  if (d_clauses.contains(clause->id())) {
131  // if clause with id does already exist,
132  // then it must be a simplification of the original clause
133  Clause* old = d_clauses[clause->id()];
134  FatalAssert(old->size() == clause->size(),
135  "MiniSat::Derivation::registerClause: new clause of different size than old clause of same id");
136 
137  std::set<Lit> oldS;
138  for (int i = 0; i < old->size(); ++i) {
139  oldS.insert((*old)[i]);
140  }
141 
142  for (int i = 0; i < clause->size(); ++i) {
143  FatalAssert(oldS.find((*clause)[i]) != oldS.end(),
144  "MiniSat::Derivation::registerClause: new clause not subset of old clause of same id");
145  oldS.erase((*clause)[i]);
146  }
147  FatalAssert(oldS.empty(),
148  "MiniSat::Derivation::registerClause: old clause not subset of new clause of same id");
149  }
150  //)
151  d_clauses[clause->id()] = clause;
152  };
153 
154  // mark clause as input clause, i.e. true without premises
155  void registerInputClause(int clauseID) {
156  // std::cout << "registerInputClause: " << clauseID << std::endl;
157  d_inputClauses.insert(clauseID);
158  };
159 
160  // clause has been removed from the solver or created internally in Derivation,
161  // so store it here for later garbage collection.
162  void removedClause(Clause* clause) {
163  FatalAssert(clause != NULL, "MiniSat::derivation:removedClause: NULL");
164  d_removedClauses.push_back(clause);
165  };
166 
167  // register the inference of a clause; takes ownership of inference
168  void registerInference(int clauseID, Inference* inference) {
169  FatalAssert(!d_inferences.contains(clauseID),
170  "MiniSat::Derivation::registerInference: inference for clauseID already registered");
171  // std::cout << "Register inference: " << clauseID << " : " << inference->toString() << std::endl;
172  d_inferences[clauseID] = inference;
173  };
174 
175  // implied is a literal that is implied at the root level.
176  // return the id of the implying unit clause [literal], if it exists.
177  //
178  // otherwise derive it from its reasons and return the new clause id.
179  // derived unit clauses are stored internally, independently of the Solver
180  //
181  // may resolve theory implications with Solver::resolveTheoryImplication
182  int computeRootReason(Lit implied, Solver* solver);
183 
184 
185  // register the empty clause (or a clause falsified in the root level)
186  // showing that the clause set is unsatisfiable.
187  //
188  // if clause is not the empty clause, the empty clause is derived from it,
189  // possible using computeRootReason
190  void finish(Clause* clause, Solver* solver);
191 
192 
193  // print the derivation of the given clause
194  //
195  // output is of the form:
196  // ID D : L1 ... Ln : C1 K1 C2 K2 ... Cm
197  // where:
198  // ID - the id of a clause
199  // D - 'I' for an input clause, 'D' for a clause derived from other clauses
200  // Li - the clause literals
201  // Ci Ki - the clause is derived from these clauses by binary resolution on the given literals
202  //
203  // factoring is done after each resolution step, i.e. duplicate literals are removed from the clause.
204  //
205  // example:
206  // 3 D : +12 -2 -33 : 1 +10 2
207  // says that the clause with the id 3 consists of the literals +12, -2, -33,
208  // and was derived by resolution between the clauses with ids 1 and 2,
209  // where the literal +10 is in clause 1 and -10 is in clause 2.
210  //
211  // for example, 1 may be the clause +12 +10 -2, and 2 may be -10 -2 -33,
212  // which resolved on +10 yield the clause +12 -2 -2 -33,
213  // which after factoring simplified to +12 -2 -33.
214  void printDerivation(Clause* clause);
215 
216  // print the derivation of the empty clause.
217  void printDerivation();
218 
219  // for debugging only
220  void checkDerivation(Clause* clause);
221 
222  // creates a new proof; ownership transferred to caller
224  SAT::SatProof* createProof(Clause* clause);
225 
226  // see Solver::push - clauseID is the highest currently used clause id
227  void push(int clauseID);
228 
229  // see Solver::pop - clauseID corresponds to a clause id used in a push
230  void pop(int clauseID);
231  };
232 }
233 
234 
235 #endif