source: vis_dev/zchaff/SAT.h @ 77

Last change on this file since 77 was 10, checked in by cecile, 13 years ago

Zchaff

File size: 17.5 KB
Line 
1// /*********************************************************************
2// Copyright 2000-2004, Princeton University.  All rights reserved.
3// By using this software the USER indicates that he or she has read,
4// understood and will comply with the following:
5//
6// --- Princeton University hereby grants USER nonexclusive permission
7// to use, copy and/or modify this software for internal, noncommercial,
8// research purposes only. Any distribution, including commercial sale
9// or license, of this software, copies of the software, its associated
10// documentation and/or modifications of either is strictly prohibited
11// without the prior consent of Princeton University.  Title to copyright
12// to this software and its associated documentation shall at all times
13// remain with Princeton University.  Appropriate copyright notice shall
14// be placed on all software copies, and a complete copy of this notice
15// shall be included in all copies of the associated documentation.
16// No right is  granted to use in advertising, publicity or otherwise
17// any trademark,  service mark, or the name of Princeton University.
18//
19//
20// --- This software and any associated documentation is provided "as is"
21//
22// PRINCETON UNIVERSITY MAKES NO REPRESENTATIONS OR WARRANTIES, EXPRESS
23// OR IMPLIED, INCLUDING THOSE OF MERCHANTABILITY OR FITNESS FOR A
24// PARTICULAR PURPOSE, OR THAT  USE OF THE SOFTWARE, MODIFICATIONS, OR
25// ASSOCIATED DOCUMENTATION WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS,
26// TRADEMARKS OR OTHER INTELLECTUAL PROPERTY RIGHTS OF A THIRD PARTY.
27//
28// Princeton University shall not be liable under any circumstances for
29// any direct, indirect, special, incidental, or consequential damages
30// with respect to any claim by USER or any third party on account of
31// or arising from the use, or inability to use, this software or its
32// associated documentation, even if Princeton University has been advised
33// of the possibility of those damages.
34// *********************************************************************/
35
36#ifndef __SAT_HEADER__
37#define __SAT_HEADER__
38
39#define SAT_Manager void *
40
41typedef long long long64;  // this is for 32 bit unix machines
42// typedef long long64;     // this is for Windows or 64 bit unix machines
43
44
45#ifndef _SAT_STATUS_
46#define _SAT_STATUS_
47enum SAT_StatusT {
48    UNDETERMINED,
49    UNSATISFIABLE,
50    SATISFIABLE,
51    TIME_OUT,
52    MEM_OUT,
53    ABORTED
54};
55#endif
56
57#ifndef _CLS_STATUS_
58#define _CLS_STATUS_
59enum CLAUSE_STATUS {
60    ORIGINAL_CL,
61    CONFLICT_CL,
62    DELETED_CL,
63};
64#endif
65
66#ifndef UNKNOWN
67#define UNKNOWN         2
68#endif
69
70// /*============================================================
71//
72// This is the header for using the sat solver. A typical flow is
73//
74// 1. calling SAT_InitManager to get a new manager. You can pre-set
75//    the number of variables upfront, or you can add it later by
76//    SAT_AddVariable.
77//    Variables are indexed from 1, NOT 0.
78//
79// 2. add clauses by calling SAT_AddClause. Clause is represented by
80//    an array of integers. Each literal is represented by
81//    2 * VarIndex + Sign. The Sign is 0 for positive phased literals,
82//    and 1 for negative phased literals.
83//    For example, a clause (3 -5 11 -4 ) should be represented by
84//    { 6, 11, 22, 9 }
85//    Note: Each variable can occure no more than once in a clause.
86//    if a variable occures in both phase, the clause is automatically
87//    satisfied. If more than one occurance with same phase, they
88//    should be combined. IT IS YOUR RESPONSIBILITY TO KEEP EACH
89//    CLAUSE NON-REDUNDENT, or the solver will not function correctly.
90//
91// 3. zchaff support incremental SAT solving. Clauses can be added
92//    or deleted from the database after each run. To accomplish
93//    this, a clause is associated with a "Group ID". Each clause
94//    has one Group ID. The group of clauses with the same GID can
95//    be deleted from the database by calling SAT_DeleteClauseGroup
96//    after each run. You need to call SAT_Reset to reset the state
97//    of the solver before begining a new run.
98//    As an example, the first 10 clauses are associated with GID 1,
99//    We add another 2 clauses with GID 2. After solving this instance
100//    with 12 clauses, we may want to delete the last 2 clauses and
101//    add another 3 clauses. We call SAT_DeleteClauseGroup with GID
102//    2 and add the three clauses (these three clauses can have any
103//    GID: either 1 if you don't want to delete them in the future,
104//    2 if you want to distinguish them from Group 1). Then you should
105//    call SAT_Reset() to reset the state of the solver, and call
106//    SAT_Solve() again to solve the new instance (a instance with
107//    13 clauses).
108//    You should obtain free GID using SAT_AllocClauseGroupID. When
109//    you call SAT_DeleteClauseGroup, the gid will be freed and can
110//    be re-used when you call SAT_AllocClauseGroupID() again.
111//    You can also merge two group of clauses into 1 by calling
112//    corresponding functions.
113//
114// 4. Optionally, you may set the time limit and memory limit for
115//    the solver, note: time and memory limits are not exact.
116//    Also, you can set other paramenters like clause deletion
117//    etc.
118//
119// 5. You can add hook function to do some extra work after
120//    a certain number of decisions (branchings). A hook function
121//    should accept input of a manager, and has no return value.
122//
123// 6. Calling SAT_Solve to solve the problem. it will return the
124//    status of the solver.
125//
126// 7. If the problem is satisfiable, you can call SAT_GetVarAsgnment
127//    to get a variable assignment which satisfy the problem.
128//
129// 8. You can also get some statistics from the solver, such as
130//    run time, mem usage, etc.
131//
132// 9. Release the manager by calling SAT_ReleaseManager.
133//
134// You need to link the library libsat.a, also, though you can compile
135// your C program with c compiler when using this sat solver, you
136// still need c++ linker to link the library.
137//
138// Have fun.
139//                         The Chaff Team
140//                         (contact zfu@EE.Princeton.EDU
141//                         for any questions or suggestions)
142//                         2004. 3. 10
143// =============================================================*/
144
145
146// Following are the main functions for the flow.
147
148// init a manager
149SAT_Manager SAT_InitManager(void);
150
151// get the version of the solver
152char * SAT_Version(SAT_Manager mng);
153
154// release a manager
155void SAT_ReleaseManager(SAT_Manager mng);
156
157// set the number of variables.
158void SAT_SetNumVariables(SAT_Manager mng,
159                         int num_vars);
160
161// add a variable. it will return the new var's index
162int SAT_AddVariable(SAT_Manager mng);
163
164// the following functions will allow/disallow the variable to be branched
165// user may want to branch only on certain variables (for example, primary
166// inputs of a circuit, if the CNF is generated from circuit).
167// By default, all variables are branchable, usually, if a variable is
168// unbranchable, it's value should be determined by all the branchable variables.
169// if that's not the case, then these variables may not get an assigned
170// value even if the solver says that the problem is satisfiable.
171// Notice, the solver determines if a problem is satisfiable by trying to assign
172// all the branchable variables. If all such variables can be assigned values
173// without causing conflict, then the instance is reported as satisfiable, even
174// if the instance is actually unsatisfiable because of unbranchable
175// variables being not dependent on branchable variables.
176void SAT_EnableVarBranch(SAT_Manager mng, int vid);
177
178void SAT_DisableVarBranch(SAT_Manager mng, int vid);
179// add a clause. a literal is a integer with value 2*V_idx + sign
180// gid is the group ID. by default, gid equals 0 . Note: group 0
181// clauses can't be deleted.
182void SAT_AddClause(SAT_Manager          mng,
183                   int *                clause_lits,
184                   int                  num_lits,
185                   int                  gid = 0);
186
187// delete a clause group and learned clauses depending on them.
188void SAT_DeleteClauseGroup(SAT_Manager          mng,
189                           int                  gid);
190
191// This will reset the solver so it will not keep the implications made before
192void SAT_Reset(SAT_Manager mng);
193
194// merge the clause group gid1 with gid2, return a new group which
195// contain both groups.
196int SAT_MergeClauseGroup(SAT_Manager    mng,
197                         int            gid1,
198                         int            gid2);
199
200// Allocate a free clause group id. will be -1 if no more available.
201// current implementation allow 32 deletable group IDs ranging from
202// 1-32. Group 0 is the permanent group (i.e. can't delete).
203int SAT_AllocClauseGroupID(SAT_Manager mng);
204
205// followings are for clause gid manipulation
206int SAT_IsSetClauseGroupID(SAT_Manager mng, int cl_idx, int id);
207int SAT_SetClauseGroupID(SAT_Manager mng, int cl_idx, int id);
208int SAT_ClearClauseGroupID(SAT_Manager mng, int cl_idx, int id);
209// clauses belong to volatile group will always be deleted when
210// SAT_DeleteClauseGroup is called
211int SAT_GetVolatileGroupID(SAT_Manager mng);
212// clauses belong to global group will never be deleted
213int SAT_GetGlobalGroupID(SAT_Manager mng);
214
215
216void SAT_SetTimeLimit(SAT_Manager       mng,
217                      float             runtime);
218
219// note: memory estimation is very rough, so allow 30% of error
220// in both SetMemLimit and EstimateMemUsage. Also, in the run
221// time, the memory usage could be temporarily 50% larger than
222// the limit (this occours when program reallocate memory because
223// of insufficiency in the initial allocation).
224void SAT_SetMemLimit(SAT_Manager        mng,
225                     int                num_bytes);
226
227
228int SAT_Solve(SAT_Manager mng);
229// enum SAT_StatusT
230// Get a variable's assignment. -1 means UNKNOWN or undicided
231int SAT_GetVarAsgnment(SAT_Manager      mng,
232                       int              v_idx);
233
234// this is used for randomness in decision making
235void SAT_SetRandomness(SAT_Manager      mng,
236                       int              n);
237// if the seed < 0, solver will use the day timer to
238// get a "psuedo real random" seed.
239void SAT_SetRandSeed(SAT_Manager        mng,
240                     int                seed);
241
242// add a hookfunction. This function will be called
243// every "interval" of decisions. You can add more than
244// one such hook functions. i.e. call SAT_AddHookFun more
245// than once.
246void SAT_AddHookFun(SAT_Manager         mng,
247                    void (*fun)(void *),
248                    int                 interval);
249
250// /* =======================================================
251// This function is for users who want to customize their own
252// decision making strategy.
253//
254// What you can do is add a hook function with interval of 1,
255// that function will be called before every decision. Inside
256// this hook function, use SAT_MakeDecision to make decision
257// with variable "vid" and "sign". sign = 1 means value of
258// the variable be 0.
259//
260// If there are no free variable left, problem is satisfied,
261// call SAT_MakeDecision with vid = 0 && sign = 0 will cause
262// solver exit with status "SATISFIABLE".
263//
264// Here is an example:
265//
266// void my_own_decision (SAT_Manager mng)
267// {
268// int n_var = SAT_NumVariables(mng);
269// int i;
270// for (i=1; i<n_var; ++i) {
271//   if (SAT_GetVarAsgnment(mng, i)==UNKNOWN){
272//     SAT_MakeDecision(mng, i, 1); //make decision with value 0;
273//     break;
274//   }
275// }
276// if (i >= n_var) //every var got an assignment, no free var left
277//   SAT_MakeDecision (mng, 0, 0);
278// }
279// ======================================================== */
280void SAT_MakeDecision(SAT_Manager        mng,
281                      int                vid,
282                      int                sign);
283
284// Following are statistics collecting functions
285int SAT_EstimateMemUsage(SAT_Manager mng);
286// time elapsed from last call of GetElapsedCPUTime
287float SAT_GetElapsedCPUTime(SAT_Manager mng);
288// current cpu time
289float SAT_GetCurrentCPUTime(SAT_Manager mng);
290// time spent on the whole solving process
291float SAT_GetCPUTime(SAT_Manager mng);
292
293int SAT_NumLiterals(SAT_Manager mng);
294
295int SAT_NumClauses(SAT_Manager mng);
296
297int SAT_NumVariables(SAT_Manager mng);
298
299int SAT_InitNumLiterals(SAT_Manager mng);
300
301int SAT_InitNumClauses(SAT_Manager mng);
302
303long64 SAT_NumAddedLiterals(SAT_Manager mng);
304
305int SAT_NumAddedClauses(SAT_Manager mng);
306
307int SAT_NumShrinkings(SAT_Manager mng);
308
309int SAT_NumDeletedClauses(SAT_Manager mng);
310
311int SAT_NumDelOrigCls(SAT_Manager mng);
312
313long64 SAT_NumDeletedLiterals(SAT_Manager mng);
314
315int SAT_NumDecisions(SAT_Manager mng);
316int SAT_NumDecisionsStackConf(SAT_Manager mng);
317int SAT_NumDecisionsVsids(SAT_Manager mng);
318int SAT_NumDecisionsShrinking(SAT_Manager mng);
319
320
321int SAT_Random_Seed(SAT_Manager mng);
322
323long64 SAT_NumImplications(SAT_Manager mng);
324
325int SAT_MaxDLevel(SAT_Manager mng);
326
327float SAT_AverageBubbleMove(SAT_Manager mng);
328// Following function will allow you to traverse all the
329// clauses and literals. Clause is represented by a index.
330// The original clauses' indice are not changed during the
331// whole process, while added clauses may get deleted, so
332// a certain index may not always represent the same
333// clause, also, a index may not always be valid.
334int SAT_GetFirstClause(SAT_Manager mng);
335
336// GetClauseType will get the clause's type. it can be
337// ORIGINAL_CL, CONFLICT_CL, PROBE_CL
338int SAT_GetClauseType(SAT_Manager mng, int cl_idx);
339
340// if there are no more clauses left, return value is -1.
341// the organization is like :
342// index 0 ... InitNumClauses - 1 are the original clauses
343// after that, they are added clauses.
344int SAT_GetNextClause(SAT_Manager mng, int cl_idx);
345
346int SAT_GetClauseNumLits(SAT_Manager mng, int cl_idx);
347
348// the lits array should have been pre-allocated enough memory
349// to store all the lits of a clause. Use SAT_GetClauseNumLits to find
350// out before-hand how much memory is required.
351void SAT_GetClauseLits(SAT_Manager mng, int cl_idx,  int * lits);
352
353// Following functions dictate the run time behavior
354// Don't mess with them unless you know what you are doing
355void SAT_EnableConfClsDeletion(SAT_Manager mng);
356void SAT_DisableConfClsDeletion(SAT_Manager mng);
357void SAT_SetClsDeletionInterval(SAT_Manager mng, int freq);
358
359void SAT_SetMaxUnrelevance(SAT_Manager mng, int n);
360void SAT_SetMinClsLenForDelete(SAT_Manager mng, int n);
361void SAT_SetMaxConfClsLenAllowed(SAT_Manager mng, int n);
362
363//  void SAT_AllowMultipleConflicts(SAT_Manager mng);
364//  void SAT_AllowMultipleConfCls(SAT_Manager mng);
365//  void SAT_SetLitPoolCompactRatio(SAT_Manager mng, float ratio);
366//  void SAT_SetLitPoolExpantionRatio(SAT_Manager mng, float ration);
367
368// this function cleans all learned clauses in the database.
369// it can be called if you incrementally solving many instances and
370// the learned clauses occupy too much memory. By calling
371// this function, it essentially equal to a fresh restart, i.e. throw
372// away the learned clauses obtained so far.
373void SAT_CleanUpDatabase(SAT_Manager mng);
374
375// Followings are functions to facilitate the translation from
376// Circuit to a CNF representation. It will automatically generate
377// the necessary clauses to represent the gates.
378// Note: The input convension are the same as in AddClause,
379//      e.g. 2 * Vid + Sign
380// NOTE: You need to make sure that the signals (a, b, c, o etc) are
381// distinctive. I.e. the two inputs to a AND2 gate are different
382// signals. Otherwise, the solver may behave incorrectly. Don't
383// add a gate that has signal a and a' as inputs. You should do
384// these kinds of special case simplifications by yourself.
385
386
387void SAT_GenClsAnd2(SAT_Manager         mng,
388                    int                 a,
389                    int                 b,
390                    int                 o,
391                    int                 gid = 0);
392
393void SAT_GenClsAndN(SAT_Manager         mng,
394                    int *               inputs,
395                    int                 num_inputs,
396                    int                 o,
397                    int                 gid = 0);
398
399void SAT_GenClsOr2(SAT_Manager          mng,
400                   int                  a,
401                   int                  b,
402                   int                  o,
403                   int                  gid = 0);
404
405void SAT_GenClsOrN(SAT_Manager          mng,
406                   int *                inputs,
407                   int                  num_inputs,
408                   int                  o,
409                   int                  gid = 0);
410
411void SAT_GenClsNand2(SAT_Manager        mng,
412                     int                a,
413                     int                b,
414                     int                o,
415                     int                gid = 0);
416
417void SAT_GenClsNandN(SAT_Manager        mng,
418                     int *              inputs,
419                     int                num_inputs,
420                     int                o,
421                     int                gid = 0);
422
423void SAT_GenClsNor2(SAT_Manager         mng,
424                    int                 a,
425                    int                 b,
426                    int                 o,
427                    int                 gid = 0);
428
429void SAT_GenClsNorN(SAT_Manager         mng,
430                   int *                inputs,
431                   int                  num_inputs,
432                   int                  o,
433                   int                  gid = 0);
434
435void SAT_GenClsXor(SAT_Manager          mng,
436                   int                  a,
437                   int                  b,
438                   int                  o,
439                   int                  gid = 0);
440
441void SAT_GenClsNot(SAT_Manager          mng,
442                   int                  a,
443                   int                  o,
444                   int                  gid = 0);
445
446#endif
Note: See TracBrowser for help on using the repository browser.