CVC3
sat_api.h
Go to the documentation of this file.
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 {
32  } SATStatus;
33 
34  // Constructor and Destructor
35  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;
54  Var() : id(-1) {}
55  bool IsNull() { return id == -1; }
56  void Reset() { id = -1; }
57  };
58 
59  union Lit {
60  long id;
61  void *vptr;
62  Lit() : id(-1) {}
63  bool IsNull() { return id == -1; }
64  void Reset() { id = -1; }
65  };
66 
67  union Clause {
68  long id;
69  void *vptr;
70  Clause() : id(-1) {}
71  bool IsNull() { return id == -1; }
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
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.
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.
218  virtual bool SetBudget(int budget) { return false; }
219 
220  // Set memory limit in bytes.
221  virtual bool SetMemLimit(int mem_limit) { return false; }
222 
223  // Set parameters controlling randomness. Implementation defines what this
224  // means.
225  virtual bool SetRandomness(int n) { return false; }
226  virtual bool SetRandSeed(int seed) { return false; }
227 
228  // Enable or disable deletion of conflict clauses to help control memory.
229  virtual bool EnableClauseDeletion() { return false; }
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
243  virtual int GetBudgetUsed() { return -1; }
244 
245  // Return the amount of memory in use
246  virtual int GetMemUsed() { return -1; }
247 
248  // Return the number of decisions made so far
249  virtual int GetNumDecisions() { return -1; }
250 
251  // Return the number of conflicts (equal to the number of backtracks)
252  virtual int GetNumConflicts() { return -1; }
253 
254  // Return the number of conflicts generated by the registered external
255  // conflict generator
256  virtual int GetNumExtConflicts() { return -1; }
257 
258  // Return the elapsed CPU time (in seconds) since the call to Satisfiable()
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)
263  virtual float GetSATTime() { return -1; }
264 
265  // Return the total number of literals in all clauses
266  virtual int GetNumLiterals() { return -1; }
267 
268  // Return the number of clauses that were deleted
269  virtual int GetNumDeletedClauses() { return -1; }
270 
271  // Return the total number of literals in all deleted clauses
272  virtual int GetNumDeletedLiterals() { return -1; }
273 
274  // Return the number of unit propagations
275  virtual int GetNumImplications() { return -1; }
276 
277  // Return the maximum decision level reached
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