search_fast.h

Go to the documentation of this file.
00001 ///////////////////////////////////////////////////////////////////////////////
00002 /*!
00003  * \file search_fast.h
00004  *
00005  * Author: Mark Zavislak
00006  *
00007  * Created: Mon Jul 21 17:33:18 UTC 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  *
00016  * <hr>
00017  *
00018  * A faster implementation of the proof search engine
00019  */
00020 ///////////////////////////////////////////////////////////////////////////////
00021 
00022 #ifndef _cvc3__include__search_fast_h_
00023 #define _cvc3__include__search_fast_h_
00024 
00025 #include <deque>
00026 #include <utility>
00027 #include "search_impl_base.h"
00028 #include "variable.h"
00029 #include "circuit.h"
00030 #include "statistics.h"
00031 #include <set>
00032 #include "smartcdo.h"
00033 
00034 namespace CVC3 {
00035 
00036   class VariableManager;
00037   class DecisionEngine;
00038 
00039 ////////////////////////////////////////////////////////////////////////////
00040 //////////// Definition of modules (groups) for doxygen ////////////////////
00041 ////////////////////////////////////////////////////////////////////////////
00042 
00043 /*!
00044  * \defgroup SE_Fast Fast Search Engine
00045  * \ingroup SE
00046  *
00047  * This module includes all the components of the fast search
00048  * engine.
00049  * @{
00050  */
00051 
00052   //! Implementation of a faster search engine, using newer techniques.
00053   /*!
00054 
00055   This search engine is engineered for greater speed.  It seeks to
00056   eliminate the use of recursion, and instead replace it with
00057   iterative procedures that have cleanly defined invariants.  This
00058   will hopefully not only eliminate bugs or inefficiencies that have
00059   been difficult to track down in the default version, but it should
00060   also make it easier to trace, read, and understand.  It strives to
00061   be in line with the most modern SAT techniques.
00062 
00063   There are three other significant changes.
00064 
00065   One, we want to improve the performance on heavily non-CNF problems.
00066   Unlike the older CVC, CVC3 does not expand problems into CNF and
00067   solve, but rather uses decision procedures to effect the same thing,
00068   but often much more slowly.  This search engine will leverage off
00069   knowledge gained from the DPs in the form of conflict clauses as
00070   much as possible.
00071 
00072   Two, the solver has traditionally had a difficult time getting
00073   started on non-CNF problems.  Modern satsolvers also have this
00074   problem, and so they employ "restarts" to try solving the problem
00075   again after gaining more knowledge about the problem at hand.  This
00076   allows a more accurate choice of splitters, and in the case of
00077   non-CNF problems, the solver can immediately leverage off CNF
00078   conflict clauses that were not initially available.
00079 
00080   Third, this code is specifically designed to deal with the new
00081   dependency tracking.  Lazy maps will be eliminated in favor implicit
00082   conflict graphs, reducing computation time in two different ways.
00083 
00084   */
00085 
00086   class SearchEngineFast : public SearchImplBase {
00087 
00088     friend class Circuit;
00089 
00090   /*! \addtogroup SE_Fast
00091    * @{
00092    */
00093 
00094     //! Name
00095     std::string d_name;
00096     //! Decision Engine
00097     DecisionEngine *d_decisionEngine;
00098     //! Total number of unit propagations
00099     StatCounter d_unitPropCount;
00100     //! Total number of circuit propagations
00101     StatCounter d_circuitPropCount;
00102     //! Total number of conflicts
00103     StatCounter d_conflictCount;
00104     //! Total number of conflict clauses generated (not all may be active)
00105     StatCounter d_conflictClauseCount;
00106 
00107     //! Backtrackable list of clauses.
00108     /*! New clauses may come into play
00109       from the decision procedures that are context dependent. */
00110     CDList<ClauseOwner> d_clauses;
00111 
00112     //! Backtrackable set of pending unprocessed literals.
00113     /*! These can be discovered at any scope level during conflict
00114       analysis. */
00115     CDMap<Expr,Theorem> d_unreportedLits;
00116     CDMap<Expr,bool> d_unreportedLitsHandled;
00117 
00118     //! Backtrackable list of non-literals (non-CNF formulas).
00119     /*! We treat nonliterals like clauses, because they are a superset
00120         of clauses.  We stick the real clauses into d_clauses, but all
00121         the rest have to be stored elsewhere. */
00122     CDList<SmartCDO<Theorem> > d_nonLiterals;
00123     CDMap<Expr,Theorem> d_nonLiteralsSaved; //!< prevent reprocessing
00124     //    CDMap<Expr,bool> d_nonLiteralSimplified; //!< Simplified non-literals
00125 
00126     //! Theorem which records simplification of the last query
00127     CDO<Theorem> d_simplifiedThm;
00128 
00129     //! Size of d_nonLiterals before most recent query
00130     CDO<unsigned> d_nonlitQueryStart;
00131     //! Size of d_nonLiterals after query (not including DP-generated non-literals)
00132     CDO<unsigned> d_nonlitQueryEnd;
00133     //! Size of d_clauses before most recent query
00134     CDO<unsigned> d_clausesQueryStart;
00135     //! Size of d_clauses after query
00136     CDO<unsigned> d_clausesQueryEnd;
00137 
00138     //! Array of conflict clauses: one deque for each outstanding query
00139     std::vector<std::deque<ClauseOwner>* > d_conflictClauseStack;
00140     //! Reference to top deque of conflict clauses
00141     std::deque<ClauseOwner>* d_conflictClauses;
00142 
00143     //! Helper class for managing conflict clauses
00144     /*! Conflict clauses should only get popped when the context in which a
00145      *  call to checkValid originates is popped.  This helper class checks
00146      *  every time there's a pop to see if the conflict clauses need to be
00147      *  restored.
00148      */
00149     friend class ConflictClauseManager;
00150     class ConflictClauseManager :public ContextNotifyObj {
00151       SearchEngineFast* d_se;
00152       std::vector<int> d_restorePoints;
00153     public:
00154       ConflictClauseManager(Context* context, SearchEngineFast* se)
00155         : ContextNotifyObj(context), d_se(se) {}
00156       void setRestorePoint();
00157       void notify();
00158     };
00159     ConflictClauseManager d_conflictClauseManager;
00160 
00161     //! Unprocessed unit conflict clauses
00162     /*! When we find unit conflict clauses, we are automatically going
00163         to jump back to the original scope.  Hopefully we won't find
00164         multiple ones, but you never know with those wacky decision
00165         procedures just spitting new information out.  These are then
00166         directly asserted then promptly forgotten about.  Chaff keeps
00167         them around (for correctness maybe), but we already have the
00168         proofs stored in the literals themselves. */
00169     std::vector<Clause> d_unitConflictClauses;
00170 
00171 
00172     //! Set of literals to be processed by bcp.
00173     /*! These are emptied out upon backtracking, because they can only
00174         be valid if they were already all processed without conflicts.
00175         Therefore, they don't need to be context dependent. */
00176     std::vector<Literal> d_literals;
00177     //! Set of asserted literals which may survive accross checkValid() calls
00178     /*!
00179      *  When a literal is asserted outside of checkValid() call, its
00180      *  value is remembered in a Literal database, but the literal
00181      *  queue for BCP is cleared.  We add literals to this set at the
00182      *  proper scope levels, and propagate them at the beginning of a
00183      *  checkValid() call.
00184      */
00185     CDMap<Expr,Literal> d_literalSet;
00186 
00187     //! Queue of derived facts to be sent to DPs
00188     /*! \sa addFact() and commitFacts() */
00189     std::vector<Theorem> d_factQueue;
00190     /*! @brief When true, use TheoryCore::enqueueFact() instead of
00191      * addFact() in commitFacts()
00192      */
00193     bool d_useEnqueueFact;
00194     //! True when checkSAT() is running
00195     /*! Used by addLiteralFact() to determine whether to BCP the
00196      *  literals immediately (outside of checkSAT()) or not.
00197      */
00198     bool d_inCheckSAT;
00199 
00200 
00201     //! Set of alive literals that shouldn't be garbage-collected
00202     /*! Unfortunately, I have a keep-alive issue.  I think literals
00203         actually have to hang around, so I assert them to a separate
00204         d_litsAlive CDList. */
00205     CDList<Literal> d_litsAlive;
00206 
00207     /*! @brief Mappings of literals to vectors of pointers to the
00208       corresponding watched literals.  */
00209     /*! A pointer is a pair (clause,i), where 'i' in {0,1} is the index
00210       of the watch pointer in the clause.
00211     */
00212     // ExprHashMap<std::vector<std::pair<Clause, int> > > d_wp;
00213 
00214     std::vector<Circuit*> d_circuits;
00215     ExprHashMap<std::vector<Circuit*> > d_circuitsByExpr;
00216 
00217     //! The scope of the last conflict
00218     /*! This is the true scope of the conflict, not necessarily the
00219       scope where the conflict was detected. */
00220     int d_lastConflictScope;
00221     //! The last conflict clause (for checkSAT()).  May be Null.
00222     /*! It records which conflict clause must be processed by BCP after
00223       backtracking from a conflict.  A conflict may generate several
00224       conflict clauses, but only one of them will cause a unit
00225       propagation.
00226     */
00227     Clause d_lastConflictClause;
00228     //! Theorem(FALSE) which generated a conflict
00229     Theorem d_conflictTheorem;
00230 
00231     /*! @brief Return a ref to the vector of watched literals.  If no
00232       such vector exists, create it. */
00233     std::vector<std::pair<Clause, int> >& wp(const Literal& literal);
00234 
00235     /*! @brief \return true if SAT, false otherwise.
00236      *
00237      * When false is returned, proof is saved in d_lastConflictTheorem */
00238     QueryResult checkSAT();
00239 
00240     //! Choose a splitter.
00241     /*! Preconditions: The current context is consistent.
00242      *
00243      * \return true if splitter available, and it asserts it through
00244      * newIntAssumption() after first pushing a new context.
00245      *
00246      * \return false if no splitters are available, which means the
00247      * context is SAT.
00248      *
00249      * Postconditions: A literal has been asserted through
00250      * newIntAssumption().
00251      */
00252     bool split();
00253 
00254     // Moved from the decision engine:
00255     //! Returns a splitter
00256     Expr findSplitter();
00257     //! Position of a literal with max score in d_litsByScores
00258     unsigned d_litsMaxScorePos;
00259     //! Vector of literals sorted by score
00260     std::vector<Literal> d_litsByScores;
00261     /*
00262     //! Mapping of literals to scores
00263     ExprHashMap<unsigned> d_litScores;
00264     //! Mapping of literals to their counters
00265     ExprHashMap<unsigned> d_litCounts;
00266     //! Mapping of literals to previous counters (what's that, anyway?)
00267     ExprHashMap<unsigned> d_litCountPrev;
00268     */
00269     //! Internal splitter counter for delaying updateLitScores()
00270     int d_splitterCount;
00271     //! Internal (decrementing) count of added splitters, to sort d_litByScores
00272     int d_litSortCount;
00273 
00274     //! Flag to switch on/off the berkmin heuristic
00275     const bool d_berkminFlag;
00276 
00277     //! Clear the list of asserted literals (d_literals)
00278     void clearLiterals();
00279 
00280     void updateLitScores(bool firstTime);
00281     //! Add the literals of a new clause to d_litsByScores
00282     void updateLitCounts(const Clause& c);
00283 
00284 
00285     //! Boolean constraint propagation.
00286     /*! Preconditions: On every run besides the first, the CNF clause
00287      *  database must not have any unit or unsat clauses, and there
00288      *  must be a literal queued up for processing.  The current
00289      *  context must be consistent.  Any and all assertions and
00290      *  assignments must actually be made within the bcp loop.  Other
00291      *  parts of the solver may queue new facts with addLiteralFact()
00292      *  and addNonLiteralFact().  bcp() will either process them, or
00293      *  it will find a conflict, in which case they will no longer be
00294      *  valid and will be dumped.  Any nonLiterals must already be
00295      *  simplified.
00296      *
00297      *  Description: BCP will systematically work through all the
00298      *  literals and nonliterals, using boolean constraint propagation
00299      *  by detecting unit clauses and using addLiteralFact() on the
00300      *  unit literal while also marking the clause as SAT.  Any
00301      *  clauses marked SAT are guaranteed to be SAT, but clauses not
00302      *  marked SAT are not guaranteed to be unsat.
00303      *
00304      * \return false if a conflict is found, true otherwise.
00305      *
00306      *  Postconditions: False indicates conflict.  If the conflict was
00307      *  discovered in CNF, we call the proof rule, then store that
00308      *  clause pointer so fixConflict() can skip over it during the
00309      *  search (when we finally change dependency tracking).
00310      *
00311      *  True indicates success.  All literals and nonLiterals have
00312      *  been processed without causing a conflict.  Processing
00313      *  nonliterals implies running simplify on them, immediately
00314      *  asserting any simplifications back to the core, and marking
00315      *  the original nonLiteral as simplified, to be ignored by all
00316      *  future (this context or deeper) splitters and bcp runs.
00317      *  Therefore, there will be no unsimplified nonliterals
00318      *  remaining.
00319      */
00320     bool bcp();
00321 
00322     //! Determines backtracking level and adds conflict clauses.
00323     /*! Preconditions: The current context is inconsistent.  If it
00324      *  resulted from a conflictRule() application, then the theorem
00325      *  is stored inside d_lastConflictTheorem.
00326      *
00327      *  If this was caused from bcp, we obtain the conflictRule()
00328      *  theorem from the d_lastConflictTheorem instance variable.
00329      *  From here we build conflict clauses and determine the correct
00330      *  backtracking level, at which point we actually backtrack
00331      *  there.  Finally, we also call addLiteralFact() on the "failure
00332      *  driven assertion" literal so that bcp has some place to begin
00333      *  (and it satisfies the bcp preconditions)
00334      *
00335      *  Postconditions: If True is returned: The current context is
00336      *  consistent, and a literal is queued up for bcp to process.  If
00337      *  False is returned: The context cannot be made consistent
00338      *  without backtracking past the original one, so the formula is
00339      *  unsat.
00340      */
00341     bool fixConflict();
00342     //! FIXME: document this
00343     void assertAssumptions();
00344     //! Queue up a fact to assert to the DPs later
00345     void enqueueFact(const Theorem& thm);
00346     //! Set the context inconsistent.  Takes Theorem(FALSE).
00347     void setInconsistent(const Theorem& thm);
00348     //! Commit all the enqueued facts to the DPs
00349     void commitFacts();
00350     //! Clear the local fact queue
00351     void clearFacts();
00352 
00353     /*! @name Processing a Conflict */
00354     //@{
00355     /*! @brief Take a conflict in the form of Literal, or
00356         Theorem, and generate all the necessary conflict clauses. */
00357     Theorem processConflict(const Literal& l);
00358     Theorem processConflict(const Theorem& thm);
00359     //@}
00360 
00361     //! Auxiliary function for unit propagation
00362     bool propagate(const Clause &c, int idx, bool& wpUpdated);
00363     //! Do the unit propagation for the clause
00364     void unitPropagation(const Clause &c, unsigned idx);
00365     //! Analyse the conflict, find the UIPs, etc.
00366     void analyzeUIPs(const Theorem &falseThm, int conflictScope);
00367 
00368     /////////////////////////////
00369     // New convenience methods //
00370     /////////////////////////////
00371 
00372     //! Go through all the clauses and check the watch pointers (for debugging)
00373     IF_DEBUG(void fullCheck();)
00374     //! Set up the watch pointers for the new clause
00375     void addNewClause(Clause &c);
00376     //! Process a new derived fact (auxiliary function)
00377     void recordFact(const Theorem& thm);
00378 
00379     //! First pass in conflict analysis; takes a theorem of FALSE
00380     void traceConflict(const Theorem& conflictThm);
00381     //! Private helper function for checkValid and restart
00382     QueryResult checkValidMain(const Expr& e2);
00383 
00384   public:
00385     //! The main Constructor
00386     SearchEngineFast(TheoryCore* core);
00387     //! Destructor
00388     virtual ~SearchEngineFast();
00389 
00390     const std::string& getName() { return d_name; }
00391     //! Implementation of the API call
00392     virtual QueryResult checkValidInternal(const Expr& e);
00393     virtual QueryResult restartInternal(const Expr& e);
00394     //! Redefine the counterexample generation.
00395     virtual void getCounterExample(std::vector<Expr>& assertions);
00396     //! Notify the search engine about a new literal fact.
00397     void addLiteralFact(const Theorem& thm);
00398     //! Notify the search engine about a new non-literal fact.
00399     void addNonLiteralFact(const Theorem& thm);
00400     /*! @brief Redefine newIntAssumption(): we need to add the new theorem
00401       to the appropriate Literal */
00402     virtual Theorem newIntAssumption(const Expr& e);
00403     virtual bool isAssumption(const Expr& e);
00404     void addSplitter(const Expr& e, int priority);
00405 
00406   /*! @} */ // end of addtogroup SE_Fast
00407 
00408     //! Return next clause whose satisfiability is unknown
00409     //virtual Clause nextClause();
00410     //! Return next non-clause which does not reduce to false
00411     //virtual Expr nextNonClause();
00412   };
00413 /*! @} */ // end of SE_Fast
00414 }
00415 
00416 
00417 #endif

Generated on Wed Nov 18 16:13:30 2009 for CVC3 by  doxygen 1.5.2