1 /////////////////////////////////////////////////////////////////////////////// 2 // // 3 // File: sat_api.h // 4 // Author: Clark Barrett // 5 // Created: Tue Oct 22 11:30:54 2002 // 6 // Description: Generic enhanced SAT API // 7 // // 8 /////////////////////////////////////////////////////////////////////////////// 9 10 #ifndef _SAT_API_H_ 11 #define _SAT_API_H_ 12 13 #include <vector> 14 #include <iostream> 15 16 /////////////////////////////////////////////////////////////////////////////// 17 // // 18 // Class: SAT // 19 // Author: Clark Barrett // 20 // Created: Tue Oct 22 12:02:53 2002 // 21 // Description: API for generic SAT solver with enhanced interface features. // 22 // // 23 /////////////////////////////////////////////////////////////////////////////// 24 class SatSolver { 25 public: 26 typedef enum SATStatus { 27 UNKNOWN, 28 UNSATISFIABLE, 29 SATISFIABLE, 30 BUDGET_EXCEEDED, 31 OUT_OF_MEMORY 32 } SATStatus; 33 34 // Constructor and Destructor SatSolver()35 SatSolver() {} ~SatSolver()36 virtual ~SatSolver() {} 37 38 // Implementation must provide this function 39 static SatSolver *Create(); 40 41 ///////////////////////////////////////////////////////////////////////////// 42 // Variables, Literals, and Clauses // 43 ///////////////////////////////////////////////////////////////////////////// 44 45 // Variables, literals and clauses are all simple union classes. This makes 46 // it easy to use integers or pointers to some more complex data structure 47 // for the implementation while at the same time increasing safety by 48 // imposing strict type requirements on users of the API. 49 // The value -1 is reserved to represent an empty or NULL value 50 51 union Var { 52 long id; 53 void *vptr; Var()54 Var() : id(-1) {} IsNull()55 bool IsNull() { return id == -1; } Reset()56 void Reset() { id = -1; } 57 }; 58 59 union Lit { 60 long id; 61 void *vptr; Lit()62 Lit() : id(-1) {} IsNull()63 bool IsNull() { return id == -1; } Reset()64 void Reset() { id = -1; } 65 }; 66 67 union Clause { 68 long id; 69 void *vptr; Clause()70 Clause() : id(-1) {} IsNull()71 bool IsNull() { return id == -1; } Reset()72 void Reset() { id = -1; } 73 }; 74 75 // Return total number of variables 76 virtual int NumVariables()=0; 77 78 // Returns the first of nvar new variables. 79 virtual Var AddVariables(int nvars)=0; 80 81 // Return a new variable AddVariable()82 Var AddVariable() { return AddVariables(1); } 83 84 // Get the varIndexth variable. varIndex must be between 1 and 85 // NumVariables() inclusive. 86 virtual Var GetVar(int varIndex)=0; 87 88 // Return the index (between 1 and NumVariables()) of v. 89 virtual int GetVarIndex(Var v)=0; 90 91 // Get the first variable. Returns a NULL Var if there are no variables. 92 virtual Var GetFirstVar()=0; 93 94 // Get the next variable after var. Returns a NULL Var if var is the last 95 // variable. 96 virtual Var GetNextVar(Var var)=0; 97 98 // Return a literal made from the given var and phase (0 is positive phase, 1 99 // is negative phase). 100 virtual Lit MakeLit(Var var, int phase)=0; 101 102 // Get var from literal. 103 virtual Var GetVarFromLit(Lit lit)=0; 104 105 // Get phase from literal ID. 106 virtual int GetPhaseFromLit(Lit lit)=0; 107 108 // Return total number of clauses 109 virtual int NumClauses()=0; 110 111 // Add a new clause. Lits is a vector of literal ID's. Note that this 112 // function can be called at any time, even after the search for solution has 113 // started. A clause ID is returned which can be used to refer to this 114 // clause in the future. 115 virtual Clause AddClause(std::vector<Lit>& lits)=0; 116 117 // Delete a clause. This can only be done if the clause has unassigned 118 // literals and it must delete not only the clause in question, but 119 // any learned clauses which depend on it. Since this may be difficult to 120 // implement, implementing this function is not currently required. 121 // DeleteClause returns true if the clause was successfully deleted, and 122 // false otherwise. DeleteClause(Clause clause)123 virtual bool DeleteClause(Clause clause) { return false; } 124 125 // Get the clauseIndexth clause. clauseIndex must be between 0 and 126 // NumClauses()-1 inclusive. 127 virtual Clause GetClause(int clauseIndex)=0; 128 129 // Get the first clause. Returns a NULL Clause if there are no clauses. 130 virtual Clause GetFirstClause()=0; 131 132 // Get the next clause after clause. Returns a NULL Clause if clause is 133 // the last clause. 134 virtual Clause GetNextClause(Clause clause)=0; 135 136 // Returns in lits the literals that make up clause. lits is assumed to be 137 // empty when the function is called. 138 virtual void GetClauseLits(Clause clause, std::vector<Lit>* lits)=0; 139 140 141 ///////////////////////////////////////////////////////////////////////////// 142 // Checking Satisfiability and Retrieving Solutions // 143 ///////////////////////////////////////////////////////////////////////////// 144 145 146 // Main check for satisfiability. The parameter allowNewClauses tells the 147 // solver whether to expect additional clauses to be added by the API during 148 // the search for a solution. The default is that no new clauses will be 149 // added. If new clauses can be added, then certain optimizations such as 150 // the pure literal rule must be disabled. 151 virtual SATStatus Satisfiable(bool allowNewClauses=false)=0; 152 153 // Get current value of variable. -1=unassigned, 0=false, 1=true 154 virtual int GetVarAssignment(Var var)=0; 155 156 // After Satisfiable has returned with a SATISFIABLE result, this function 157 // may be called to search for the next satisfying assignment. If one is 158 // found then SATISFIABLE is returned. If there are no more satisfying 159 // assignments then UNSATISFIABLE is returned. 160 virtual SATStatus Continue()=0; 161 162 // Pop all decision levels and remove all assignments, but do not delete any 163 // clauses 164 virtual void Restart()=0; 165 166 // Pop all decision levels, remove all assignments, and delete all clauses. 167 virtual void Reset()=0; 168 169 170 ///////////////////////////////////////////////////////////////////////////// 171 // Advanced Features // 172 ///////////////////////////////////////////////////////////////////////////// 173 174 175 // The following four methods allow callback functions to be registered. 176 // Each function that is registered may optionally provide a cookie (void *) 177 // which will be passed back to that function whenever it is called. 178 179 // Register a function f which is called every time the decision level 180 // increases or decreases (i.e. every time the stack is pushed or popped). 181 // The argument to f is the change in decision level. For example, +1 is a 182 // Push, -1 is a Pop. 183 virtual void RegisterDLevelHook(void (*f)(void *, int), void *cookie)=0; 184 185 // Register a function to replace the built-in decision heuristics. Every 186 // time a new decision needs to be made, the solver will call this function. 187 // The function should return a literal which should be set to true. If the 188 // bool pointer is returned with the value false, then a literal was 189 // successfully chosen. If the value is true, this signals the solver to 190 // exit with a satisfiable result. If the bool value is false and the 191 // literal is NULL, then this signals the solver to use its own internal 192 // method for making the next decision. 193 virtual void RegisterDecisionHook(Lit (*f)(void *, bool *), void *cookie)=0; 194 195 // Register a function which is called every time the value of a variable is 196 // changed (i.e. assigned or unassigned). The first parameter is the 197 // variable ID which has changed. The second is the new value: -1=unassigned, 198 // 0=false, 1=true 199 virtual void RegisterAssignmentHook(void (*f)(void *, Var, int), 200 void *cookie)=0; 201 202 // Register a function which will be called after Boolean propagation and 203 // before making a new decision. Note that the hook function may add new 204 // clauses and this should be handled correctly. 205 virtual void RegisterDeductionHook(void (*f)(void *), void *cookie)=0; 206 207 208 ///////////////////////////////////////////////////////////////////////////// 209 // Setting Parameters // 210 ///////////////////////////////////////////////////////////////////////////// 211 212 213 // Implementations are not required to implement any of these 214 // parameter-adjusting routines. Each function will return true if the request 215 // is successful and false otherwise. 216 217 // Implementation will define budget. An example budget would be time. SetBudget(int budget)218 virtual bool SetBudget(int budget) { return false; } 219 220 // Set memory limit in bytes. SetMemLimit(int mem_limit)221 virtual bool SetMemLimit(int mem_limit) { return false; } 222 223 // Set parameters controlling randomness. Implementation defines what this 224 // means. SetRandomness(int n)225 virtual bool SetRandomness(int n) { return false; } SetRandSeed(int seed)226 virtual bool SetRandSeed(int seed) { return false; } 227 228 // Enable or disable deletion of conflict clauses to help control memory. EnableClauseDeletion()229 virtual bool EnableClauseDeletion() { return false; } DisableClauseDeletion()230 virtual bool DisableClauseDeletion() { return false; } 231 232 233 /////////////////////////////////////////////////////////////////////////////// 234 // Statistics // 235 /////////////////////////////////////////////////////////////////////////////// 236 237 238 // As with the parameter functions, the statistics-gathering functions may or 239 // may not be implemented. They return -1 if not implemented, and the 240 // correct value otherwise. 241 242 // Return the amount of the budget (set by SetBudget) which has been used GetBudgetUsed()243 virtual int GetBudgetUsed() { return -1; } 244 245 // Return the amount of memory in use GetMemUsed()246 virtual int GetMemUsed() { return -1; } 247 248 // Return the number of decisions made so far GetNumDecisions()249 virtual int GetNumDecisions() { return -1; } 250 251 // Return the number of conflicts (equal to the number of backtracks) GetNumConflicts()252 virtual int GetNumConflicts() { return -1; } 253 254 // Return the number of conflicts generated by the registered external 255 // conflict generator GetNumExtConflicts()256 virtual int GetNumExtConflicts() { return -1; } 257 258 // Return the elapsed CPU time (in seconds) since the call to Satisfiable() GetTotalTime()259 virtual float GetTotalTime() { return -1; } 260 261 // Return the CPU time spent (in seconds) inside the SAT solver 262 // (as opposed to in the registered hook functions) GetSATTime()263 virtual float GetSATTime() { return -1; } 264 265 // Return the total number of literals in all clauses GetNumLiterals()266 virtual int GetNumLiterals() { return -1; } 267 268 // Return the number of clauses that were deleted GetNumDeletedClauses()269 virtual int GetNumDeletedClauses() { return -1; } 270 271 // Return the total number of literals in all deleted clauses GetNumDeletedLiterals()272 virtual int GetNumDeletedLiterals() { return -1; } 273 274 // Return the number of unit propagations GetNumImplications()275 virtual int GetNumImplications() { return -1; } 276 277 // Return the maximum decision level reached GetMaxDLevel()278 virtual int GetMaxDLevel() { return -1; } 279 280 // Print all implemented statistics 281 void PrintStatistics(std::ostream & os = std::cout); 282 283 }; 284 285 #endif 286