1 /////////////////////////////////////////////////////////////////////////////// 2 /*! 3 * \file search_fast.h 4 * 5 * Author: Mark Zavislak 6 * 7 * Created: Mon Jul 21 17:33:18 UTC 2003 8 * 9 * <hr> 10 * 11 * License to use, copy, modify, sell and/or distribute this software 12 * and its documentation for any purpose is hereby granted without 13 * royalty, subject to the terms and conditions defined in the \ref 14 * LICENSE file provided with this distribution. 15 * 16 * <hr> 17 * 18 * A faster implementation of the proof search engine 19 */ 20 /////////////////////////////////////////////////////////////////////////////// 21 22 #ifndef _cvc3__include__search_fast_h_ 23 #define _cvc3__include__search_fast_h_ 24 25 #include <deque> 26 #include <utility> 27 #include "search_impl_base.h" 28 #include "variable.h" 29 #include "circuit.h" 30 #include "statistics.h" 31 #include <set> 32 #include "smartcdo.h" 33 34 namespace CVC3 { 35 36 class VariableManager; 37 class DecisionEngine; 38 39 //////////////////////////////////////////////////////////////////////////// 40 //////////// Definition of modules (groups) for doxygen //////////////////// 41 //////////////////////////////////////////////////////////////////////////// 42 43 /*! 44 * \defgroup SE_Fast Fast Search Engine 45 * \ingroup SE 46 * 47 * This module includes all the components of the fast search 48 * engine. 49 * @{ 50 */ 51 52 //! Implementation of a faster search engine, using newer techniques. 53 /*! 54 55 This search engine is engineered for greater speed. It seeks to 56 eliminate the use of recursion, and instead replace it with 57 iterative procedures that have cleanly defined invariants. This 58 will hopefully not only eliminate bugs or inefficiencies that have 59 been difficult to track down in the default version, but it should 60 also make it easier to trace, read, and understand. It strives to 61 be in line with the most modern SAT techniques. 62 63 There are three other significant changes. 64 65 One, we want to improve the performance on heavily non-CNF problems. 66 Unlike the older CVC, CVC3 does not expand problems into CNF and 67 solve, but rather uses decision procedures to effect the same thing, 68 but often much more slowly. This search engine will leverage off 69 knowledge gained from the DPs in the form of conflict clauses as 70 much as possible. 71 72 Two, the solver has traditionally had a difficult time getting 73 started on non-CNF problems. Modern satsolvers also have this 74 problem, and so they employ "restarts" to try solving the problem 75 again after gaining more knowledge about the problem at hand. This 76 allows a more accurate choice of splitters, and in the case of 77 non-CNF problems, the solver can immediately leverage off CNF 78 conflict clauses that were not initially available. 79 80 Third, this code is specifically designed to deal with the new 81 dependency tracking. Lazy maps will be eliminated in favor implicit 82 conflict graphs, reducing computation time in two different ways. 83 84 */ 85 86 class SearchEngineFast : public SearchImplBase { 87 88 friend class Circuit; 89 90 /*! \addtogroup SE_Fast 91 * @{ 92 */ 93 94 //! Name 95 std::string d_name; 96 //! Decision Engine 97 DecisionEngine *d_decisionEngine; 98 //! Total number of unit propagations 99 StatCounter d_unitPropCount; 100 //! Total number of circuit propagations 101 StatCounter d_circuitPropCount; 102 //! Total number of conflicts 103 StatCounter d_conflictCount; 104 //! Total number of conflict clauses generated (not all may be active) 105 StatCounter d_conflictClauseCount; 106 107 //! Backtrackable list of clauses. 108 /*! New clauses may come into play 109 from the decision procedures that are context dependent. */ 110 CDList<ClauseOwner> d_clauses; 111 112 //! Backtrackable set of pending unprocessed literals. 113 /*! These can be discovered at any scope level during conflict 114 analysis. */ 115 CDMap<Expr,Theorem> d_unreportedLits; 116 CDMap<Expr,bool> d_unreportedLitsHandled; 117 118 //! Backtrackable list of non-literals (non-CNF formulas). 119 /*! We treat nonliterals like clauses, because they are a superset 120 of clauses. We stick the real clauses into d_clauses, but all 121 the rest have to be stored elsewhere. */ 122 CDList<SmartCDO<Theorem> > d_nonLiterals; 123 CDMap<Expr,Theorem> d_nonLiteralsSaved; //!< prevent reprocessing 124 // CDMap<Expr,bool> d_nonLiteralSimplified; //!< Simplified non-literals 125 126 //! Theorem which records simplification of the last query 127 CDO<Theorem> d_simplifiedThm; 128 129 //! Size of d_nonLiterals before most recent query 130 CDO<unsigned> d_nonlitQueryStart; 131 //! Size of d_nonLiterals after query (not including DP-generated non-literals) 132 CDO<unsigned> d_nonlitQueryEnd; 133 //! Size of d_clauses before most recent query 134 CDO<unsigned> d_clausesQueryStart; 135 //! Size of d_clauses after query 136 CDO<unsigned> d_clausesQueryEnd; 137 138 //! Array of conflict clauses: one deque for each outstanding query 139 std::vector<std::deque<ClauseOwner>* > d_conflictClauseStack; 140 //! Reference to top deque of conflict clauses 141 std::deque<ClauseOwner>* d_conflictClauses; 142 143 //! Helper class for managing conflict clauses 144 /*! Conflict clauses should only get popped when the context in which a 145 * call to checkValid originates is popped. This helper class checks 146 * every time there's a pop to see if the conflict clauses need to be 147 * restored. 148 */ 149 friend class ConflictClauseManager; 150 class ConflictClauseManager :public ContextNotifyObj { 151 SearchEngineFast* d_se; 152 std::vector<int> d_restorePoints; 153 public: ConflictClauseManager(Context * context,SearchEngineFast * se)154 ConflictClauseManager(Context* context, SearchEngineFast* se) 155 : ContextNotifyObj(context), d_se(se) {} 156 void setRestorePoint(); 157 void notify(); 158 }; 159 ConflictClauseManager d_conflictClauseManager; 160 161 //! Unprocessed unit conflict clauses 162 /*! When we find unit conflict clauses, we are automatically going 163 to jump back to the original scope. Hopefully we won't find 164 multiple ones, but you never know with those wacky decision 165 procedures just spitting new information out. These are then 166 directly asserted then promptly forgotten about. Chaff keeps 167 them around (for correctness maybe), but we already have the 168 proofs stored in the literals themselves. */ 169 std::vector<Clause> d_unitConflictClauses; 170 171 172 //! Set of literals to be processed by bcp. 173 /*! These are emptied out upon backtracking, because they can only 174 be valid if they were already all processed without conflicts. 175 Therefore, they don't need to be context dependent. */ 176 std::vector<Literal> d_literals; 177 //! Set of asserted literals which may survive accross checkValid() calls 178 /*! 179 * When a literal is asserted outside of checkValid() call, its 180 * value is remembered in a Literal database, but the literal 181 * queue for BCP is cleared. We add literals to this set at the 182 * proper scope levels, and propagate them at the beginning of a 183 * checkValid() call. 184 */ 185 CDMap<Expr,Literal> d_literalSet; 186 187 //! Queue of derived facts to be sent to DPs 188 /*! \sa addFact() and commitFacts() */ 189 std::vector<Theorem> d_factQueue; 190 /*! @brief When true, use TheoryCore::enqueueFact() instead of 191 * addFact() in commitFacts() 192 */ 193 bool d_useEnqueueFact; 194 //! True when checkSAT() is running 195 /*! Used by addLiteralFact() to determine whether to BCP the 196 * literals immediately (outside of checkSAT()) or not. 197 */ 198 bool d_inCheckSAT; 199 200 201 //! Set of alive literals that shouldn't be garbage-collected 202 /*! Unfortunately, I have a keep-alive issue. I think literals 203 actually have to hang around, so I assert them to a separate 204 d_litsAlive CDList. */ 205 CDList<Literal> d_litsAlive; 206 207 /*! @brief Mappings of literals to vectors of pointers to the 208 corresponding watched literals. */ 209 /*! A pointer is a pair (clause,i), where 'i' in {0,1} is the index 210 of the watch pointer in the clause. 211 */ 212 // ExprHashMap<std::vector<std::pair<Clause, int> > > d_wp; 213 214 std::vector<Circuit*> d_circuits; 215 ExprHashMap<std::vector<Circuit*> > d_circuitsByExpr; 216 217 //! The scope of the last conflict 218 /*! This is the true scope of the conflict, not necessarily the 219 scope where the conflict was detected. */ 220 int d_lastConflictScope; 221 //! The last conflict clause (for checkSAT()). May be Null. 222 /*! It records which conflict clause must be processed by BCP after 223 backtracking from a conflict. A conflict may generate several 224 conflict clauses, but only one of them will cause a unit 225 propagation. 226 */ 227 Clause d_lastConflictClause; 228 //! Theorem(FALSE) which generated a conflict 229 Theorem d_conflictTheorem; 230 231 /*! @brief Return a ref to the vector of watched literals. If no 232 such vector exists, create it. */ 233 std::vector<std::pair<Clause, int> >& wp(const Literal& literal); 234 235 /*! @brief \return true if SAT, false otherwise. 236 * 237 * When false is returned, proof is saved in d_lastConflictTheorem */ 238 QueryResult checkSAT(); 239 240 //! Choose a splitter. 241 /*! Preconditions: The current context is consistent. 242 * 243 * \return true if splitter available, and it asserts it through 244 * newIntAssumption() after first pushing a new context. 245 * 246 * \return false if no splitters are available, which means the 247 * context is SAT. 248 * 249 * Postconditions: A literal has been asserted through 250 * newIntAssumption(). 251 */ 252 bool split(); 253 254 // Moved from the decision engine: 255 //! Returns a splitter 256 Expr findSplitter(); 257 //! Position of a literal with max score in d_litsByScores 258 unsigned d_litsMaxScorePos; 259 //! Vector of literals sorted by score 260 std::vector<Literal> d_litsByScores; 261 /* 262 //! Mapping of literals to scores 263 ExprHashMap<unsigned> d_litScores; 264 //! Mapping of literals to their counters 265 ExprHashMap<unsigned> d_litCounts; 266 //! Mapping of literals to previous counters (what's that, anyway?) 267 ExprHashMap<unsigned> d_litCountPrev; 268 */ 269 //! Internal splitter counter for delaying updateLitScores() 270 int d_splitterCount; 271 //! Internal (decrementing) count of added splitters, to sort d_litByScores 272 int d_litSortCount; 273 274 //! Flag to switch on/off the berkmin heuristic 275 const bool d_berkminFlag; 276 277 //! Clear the list of asserted literals (d_literals) 278 void clearLiterals(); 279 280 void updateLitScores(bool firstTime); 281 //! Add the literals of a new clause to d_litsByScores 282 void updateLitCounts(const Clause& c); 283 284 285 //! Boolean constraint propagation. 286 /*! Preconditions: On every run besides the first, the CNF clause 287 * database must not have any unit or unsat clauses, and there 288 * must be a literal queued up for processing. The current 289 * context must be consistent. Any and all assertions and 290 * assignments must actually be made within the bcp loop. Other 291 * parts of the solver may queue new facts with addLiteralFact() 292 * and addNonLiteralFact(). bcp() will either process them, or 293 * it will find a conflict, in which case they will no longer be 294 * valid and will be dumped. Any nonLiterals must already be 295 * simplified. 296 * 297 * Description: BCP will systematically work through all the 298 * literals and nonliterals, using boolean constraint propagation 299 * by detecting unit clauses and using addLiteralFact() on the 300 * unit literal while also marking the clause as SAT. Any 301 * clauses marked SAT are guaranteed to be SAT, but clauses not 302 * marked SAT are not guaranteed to be unsat. 303 * 304 * \return false if a conflict is found, true otherwise. 305 * 306 * Postconditions: False indicates conflict. If the conflict was 307 * discovered in CNF, we call the proof rule, then store that 308 * clause pointer so fixConflict() can skip over it during the 309 * search (when we finally change dependency tracking). 310 * 311 * True indicates success. All literals and nonLiterals have 312 * been processed without causing a conflict. Processing 313 * nonliterals implies running simplify on them, immediately 314 * asserting any simplifications back to the core, and marking 315 * the original nonLiteral as simplified, to be ignored by all 316 * future (this context or deeper) splitters and bcp runs. 317 * Therefore, there will be no unsimplified nonliterals 318 * remaining. 319 */ 320 bool bcp(); 321 322 //! Determines backtracking level and adds conflict clauses. 323 /*! Preconditions: The current context is inconsistent. If it 324 * resulted from a conflictRule() application, then the theorem 325 * is stored inside d_lastConflictTheorem. 326 * 327 * If this was caused from bcp, we obtain the conflictRule() 328 * theorem from the d_lastConflictTheorem instance variable. 329 * From here we build conflict clauses and determine the correct 330 * backtracking level, at which point we actually backtrack 331 * there. Finally, we also call addLiteralFact() on the "failure 332 * driven assertion" literal so that bcp has some place to begin 333 * (and it satisfies the bcp preconditions) 334 * 335 * Postconditions: If True is returned: The current context is 336 * consistent, and a literal is queued up for bcp to process. If 337 * False is returned: The context cannot be made consistent 338 * without backtracking past the original one, so the formula is 339 * unsat. 340 */ 341 bool fixConflict(); 342 //! FIXME: document this 343 void assertAssumptions(); 344 //! Queue up a fact to assert to the DPs later 345 void enqueueFact(const Theorem& thm); 346 //! Set the context inconsistent. Takes Theorem(FALSE). 347 void setInconsistent(const Theorem& thm); 348 //! Commit all the enqueued facts to the DPs 349 void commitFacts(); 350 //! Clear the local fact queue 351 void clearFacts(); 352 353 /*! @name Processing a Conflict */ 354 //@{ 355 /*! @brief Take a conflict in the form of Literal, or 356 Theorem, and generate all the necessary conflict clauses. */ 357 Theorem processConflict(const Literal& l); 358 Theorem processConflict(const Theorem& thm); 359 //@} 360 361 //! Auxiliary function for unit propagation 362 bool propagate(const Clause &c, int idx, bool& wpUpdated); 363 //! Do the unit propagation for the clause 364 void unitPropagation(const Clause &c, unsigned idx); 365 //! Analyse the conflict, find the UIPs, etc. 366 void analyzeUIPs(const Theorem &falseThm, int conflictScope); 367 368 ///////////////////////////// 369 // New convenience methods // 370 ///////////////////////////// 371 372 //! Go through all the clauses and check the watch pointers (for debugging) 373 IF_DEBUG(void fullCheck();) 374 //! Set up the watch pointers for the new clause 375 void addNewClause(Clause &c); 376 //! Process a new derived fact (auxiliary function) 377 void recordFact(const Theorem& thm); 378 379 //! First pass in conflict analysis; takes a theorem of FALSE 380 void traceConflict(const Theorem& conflictThm); 381 //! Private helper function for checkValid and restart 382 QueryResult checkValidMain(const Expr& e2); 383 384 public: 385 //! The main Constructor 386 SearchEngineFast(TheoryCore* core); 387 //! Destructor 388 virtual ~SearchEngineFast(); 389 getName()390 const std::string& getName() { return d_name; } 391 //! Implementation of the API call 392 virtual QueryResult checkValidInternal(const Expr& e); 393 virtual QueryResult restartInternal(const Expr& e); 394 //! Redefine the counterexample generation. 395 virtual void getCounterExample(std::vector<Expr>& assertions); 396 //! Notify the search engine about a new literal fact. 397 void addLiteralFact(const Theorem& thm); 398 //! Notify the search engine about a new non-literal fact. 399 void addNonLiteralFact(const Theorem& thm); 400 /*! @brief Redefine newIntAssumption(): we need to add the new theorem 401 to the appropriate Literal */ 402 virtual Theorem newIntAssumption(const Expr& e); 403 virtual bool isAssumption(const Expr& e); 404 void addSplitter(const Expr& e, int priority); 405 406 /*! @} */ // end of addtogroup SE_Fast 407 408 //! Return next clause whose satisfiability is unknown 409 //virtual Clause nextClause(); 410 //! Return next non-clause which does not reduce to false 411 //virtual Expr nextNonClause(); 412 }; 413 /*! @} */ // end of SE_Fast 414 } 415 416 417 #endif 418