sat_api.h

Go to the documentation of this file.
00001 ///////////////////////////////////////////////////////////////////////////////
00002 //                                                                           //
00003 // File: sat_api.h                       //
00004 // Author: Clark Barrett                                                     //
00005 // Created: Tue Oct 22 11:30:54 2002               //
00006 // Description: Generic enhanced SAT API                                     //
00007 //                                                                           //
00008 ///////////////////////////////////////////////////////////////////////////////
00009 
00010 #ifndef _SAT_API_H_
00011 #define _SAT_API_H_
00012 
00013 #include <vector>
00014 #include <iostream>
00015 
00016 ///////////////////////////////////////////////////////////////////////////////
00017 //                                                                           //
00018 // Class: SAT                      //
00019 // Author: Clark Barrett                                                     //
00020 // Created: Tue Oct 22 12:02:53 2002               //
00021 // Description: API for generic SAT solver with enhanced interface features. //
00022 //                                                                           //
00023 ///////////////////////////////////////////////////////////////////////////////
00024 class SatSolver {
00025 public:
00026   typedef enum SATStatus {
00027     UNKNOWN,
00028     UNSATISFIABLE,
00029     SATISFIABLE,
00030     BUDGET_EXCEEDED,
00031     OUT_OF_MEMORY
00032   } SATStatus;
00033 
00034   // Constructor and Destructor
00035   SatSolver() {}
00036   virtual ~SatSolver() {}
00037 
00038   // Implementation must provide this function
00039   static SatSolver *Create();
00040 
00041   /////////////////////////////////////////////////////////////////////////////
00042   // Variables, Literals, and Clauses                                        //
00043   /////////////////////////////////////////////////////////////////////////////
00044 
00045   // Variables, literals and clauses are all simple union classes.  This makes
00046   // it easy to use integers or pointers to some more complex data structure
00047   // for the implementation while at the same time increasing safety by
00048   // imposing strict type requirements on users of the API.
00049   // The value -1 is reserved to represent an empty or NULL value
00050 
00051   union Var {
00052     long id;
00053     void *vptr;
00054     Var() : id(-1) {}
00055     bool IsNull() { return id == -1; }
00056     void Reset() { id = -1; }
00057   };
00058 
00059   union Lit {
00060     long id;
00061     void *vptr;
00062     Lit() : id(-1) {}
00063     bool IsNull() { return id == -1; }
00064     void Reset() { id = -1; }
00065   };
00066 
00067   union Clause {
00068     long id;
00069     void *vptr;
00070     Clause() : id(-1) {}
00071     bool IsNull() { return id == -1; }
00072     void Reset() { id = -1; }
00073   };
00074 
00075   // Return total number of variables
00076   virtual int NumVariables()=0;
00077 
00078   // Returns the first of nvar new variables.
00079   virtual Var AddVariables(int nvars)=0;
00080 
00081   // Return a new variable
00082   Var AddVariable() { return AddVariables(1); }
00083 
00084   // Get the varIndexth variable.  varIndex must be between 1 and
00085   // NumVariables() inclusive.
00086   virtual Var GetVar(int varIndex)=0;
00087 
00088   // Return the index (between 1 and NumVariables()) of v.
00089   virtual int GetVarIndex(Var v)=0;
00090 
00091   // Get the first variable.  Returns a NULL Var if there are no variables.
00092   virtual Var GetFirstVar()=0;
00093 
00094   // Get the next variable after var.  Returns a NULL Var if var is the last
00095   // variable.
00096   virtual Var GetNextVar(Var var)=0;
00097 
00098   // Return a literal made from the given var and phase (0 is positive phase, 1
00099   // is negative phase).
00100   virtual Lit MakeLit(Var var, int phase)=0;
00101 
00102   // Get var from literal.
00103   virtual Var GetVarFromLit(Lit lit)=0;
00104 
00105   // Get phase from literal ID.
00106   virtual int GetPhaseFromLit(Lit lit)=0;
00107 
00108   // Return total number of clauses
00109   virtual int NumClauses()=0;
00110 
00111   // Add a new clause.  Lits is a vector of literal ID's.  Note that this
00112   // function can be called at any time, even after the search for solution has
00113   // started.  A clause ID is returned which can be used to refer to this
00114   // clause in the future.
00115   virtual Clause AddClause(std::vector<Lit>& lits)=0;
00116 
00117   // Delete a clause.  This can only be done if the clause has unassigned
00118   // literals and it must delete not only the clause in question, but
00119   // any learned clauses which depend on it.  Since this may be difficult to
00120   // implement, implementing this function is not currently required.
00121   // DeleteClause returns true if the clause was successfully deleted, and
00122   // false otherwise.
00123   virtual bool DeleteClause(Clause clause) { return false; }
00124 
00125   // Get the clauseIndexth clause.  clauseIndex must be between 0 and
00126   // NumClauses()-1 inclusive.
00127   virtual Clause GetClause(int clauseIndex)=0;
00128 
00129   // Get the first clause.  Returns a NULL Clause if there are no clauses.
00130   virtual Clause GetFirstClause()=0;
00131 
00132   // Get the next clause after clause.  Returns a NULL Clause if clause is
00133   // the last clause.
00134   virtual Clause GetNextClause(Clause clause)=0;
00135 
00136   // Returns in lits the literals that make up clause.  lits is assumed to be
00137   // empty when the function is called.
00138   virtual void GetClauseLits(Clause clause, std::vector<Lit>* lits)=0;
00139 
00140 
00141   /////////////////////////////////////////////////////////////////////////////
00142   // Checking Satisfiability and Retrieving Solutions                        //
00143   /////////////////////////////////////////////////////////////////////////////
00144 
00145 
00146   // Main check for satisfiability.  The parameter allowNewClauses tells the
00147   // solver whether to expect additional clauses to be added by the API during
00148   // the search for a solution.  The default is that no new clauses will be
00149   // added.  If new clauses can be added, then certain optimizations such as
00150   // the pure literal rule must be disabled.
00151   virtual SATStatus Satisfiable(bool allowNewClauses=false)=0;
00152 
00153   // Get current value of variable. -1=unassigned, 0=false, 1=true
00154   virtual int GetVarAssignment(Var var)=0;
00155 
00156   // After Satisfiable has returned with a SATISFIABLE result, this function
00157   // may be called to search for the next satisfying assignment.  If one is
00158   // found then SATISFIABLE is returned.  If there are no more satisfying
00159   // assignments then UNSATISFIABLE is returned.
00160   virtual SATStatus Continue()=0;
00161 
00162   // Pop all decision levels and remove all assignments, but do not delete any
00163   // clauses
00164   virtual void Restart()=0;
00165 
00166   // Pop all decision levels, remove all assignments, and delete all clauses.
00167   virtual void Reset()=0;
00168 
00169 
00170   /////////////////////////////////////////////////////////////////////////////
00171   // Advanced Features                                                       //
00172   /////////////////////////////////////////////////////////////////////////////
00173 
00174 
00175   // The following four methods allow callback functions to be registered.
00176   // Each function that is registered may optionally provide a cookie (void *)
00177   // which will be passed back to that function whenever it is called.
00178 
00179   // Register a function f which is called every time the decision level
00180   // increases or decreases (i.e. every time the stack is pushed or popped).
00181   // The argument to f is the change in decision level.  For example, +1 is a
00182   // Push, -1 is a Pop.
00183   virtual void RegisterDLevelHook(void (*f)(void *, int), void *cookie)=0;
00184 
00185   // Register a function to replace the built-in decision heuristics.  Every
00186   // time a new decision needs to be made, the solver will call this function.
00187   // The function should return a literal which should be set to true.  If the
00188   // bool pointer is returned with the value false, then a literal was
00189   // successfully chosen.  If the value is true, this signals the solver to
00190   // exit with a satisfiable result.  If the bool value is false and the
00191   // literal is NULL, then this signals the solver to use its own internal
00192   // method for making the next decision.
00193   virtual void RegisterDecisionHook(Lit (*f)(void *, bool *), void *cookie)=0;
00194 
00195   // Register a function which is called every time the value of a variable is
00196   // changed (i.e. assigned or unassigned).  The first parameter is the
00197   // variable ID which has changed.  The second is the new value: -1=unassigned,
00198   // 0=false, 1=true
00199   virtual void RegisterAssignmentHook(void (*f)(void *, Var, int),
00200               void *cookie)=0;
00201 
00202   // Register a function which will be called after Boolean propagation and
00203   // before making a new decision.  Note that the hook function may add new
00204   // clauses and this should be handled correctly.
00205   virtual void RegisterDeductionHook(void (*f)(void *), void *cookie)=0;
00206 
00207 
00208   /////////////////////////////////////////////////////////////////////////////
00209   // Setting Parameters                                                      //
00210   /////////////////////////////////////////////////////////////////////////////
00211 
00212 
00213   // Implementations are not required to implement any of these
00214   // parameter-adjusting routines.  Each function will return true if the request
00215   // is successful and false otherwise.
00216 
00217   // Implementation will define budget.  An example budget would be time.
00218   virtual bool SetBudget(int budget)      { return false; }
00219 
00220   // Set memory limit in bytes.
00221   virtual bool SetMemLimit(int mem_limit) { return false; }
00222 
00223   // Set parameters controlling randomness.  Implementation defines what this
00224   // means.
00225   virtual bool SetRandomness(int n)       { return false; }
00226   virtual bool SetRandSeed(int seed)      { return false; }
00227 
00228   // Enable or disable deletion of conflict clauses to help control memory.
00229   virtual bool EnableClauseDeletion()     { return false; }
00230   virtual bool DisableClauseDeletion()    { return false; }
00231 
00232 
00233   ///////////////////////////////////////////////////////////////////////////////
00234   // Statistics                                                                //
00235   ///////////////////////////////////////////////////////////////////////////////
00236 
00237 
00238   // As with the parameter functions, the statistics-gathering functions may or
00239   // may not be implemented.  They return -1 if not implemented, and the
00240   // correct value otherwise.
00241 
00242   // Return the amount of the budget (set by SetBudget) which has been used
00243   virtual int GetBudgetUsed()         { return -1; }
00244 
00245   // Return the amount of memory in use
00246   virtual int GetMemUsed()            { return -1; }
00247 
00248   // Return the number of decisions made so far
00249   virtual int GetNumDecisions()       { return -1; }
00250 
00251   // Return the number of conflicts (equal to the number of backtracks)
00252   virtual int GetNumConflicts()       { return -1; }
00253 
00254   // Return the number of conflicts generated by the registered external
00255   // conflict generator
00256   virtual int GetNumExtConflicts()    { return -1; }
00257 
00258   // Return the elapsed CPU time (in seconds) since the call to Satisfiable()
00259   virtual float GetTotalTime()        { return -1; }
00260 
00261   // Return the CPU time spent (in seconds) inside the SAT solver
00262   // (as opposed to in the registered hook functions)
00263   virtual float GetSATTime()          { return -1; }
00264 
00265   // Return the total number of literals in all clauses
00266   virtual int GetNumLiterals()        { return -1; }
00267 
00268   // Return the number of clauses that were deleted
00269   virtual int GetNumDeletedClauses()  { return -1; }
00270 
00271   // Return the total number of literals in all deleted clauses
00272   virtual int GetNumDeletedLiterals() { return -1; }
00273 
00274   // Return the number of unit propagations
00275   virtual int GetNumImplications()    { return -1; }
00276 
00277   // Return the maximum decision level reached
00278   virtual int GetMaxDLevel()          { return -1; }
00279 
00280   // Print all implemented statistics
00281   void PrintStatistics(std::ostream & os = std::cout);
00282 
00283 };
00284 
00285 #endif

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