1 /**************************************************************************************************
2 MiniSat -- Copyright (c) 2005, Niklas Sorensson
3 http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
4
5 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
6 associated documentation files (the "Software"), to deal in the Software without restriction,
7 including without limitation the rights to use, copy, modify, merge, publish, distribute,
8 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
10
11 The above copyright notice and this permission notice shall be included in all copies or
12 substantial portions of the Software.
13
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
15 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
16 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
17 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
18 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
19 **************************************************************************************************/
20 // Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
21
22 #ifndef ABC__sat__bsat__satSolver2_h
23 #define ABC__sat__bsat__satSolver2_h
24
25
26 #include <stdio.h>
27 #include <stdlib.h>
28 #include <string.h>
29 #include <assert.h>
30
31 #include "satVec.h"
32 #include "satClause.h"
33 #include "misc/vec/vecSet.h"
34 #include "satProof2.h"
35
36 ABC_NAMESPACE_HEADER_START
37
38 //#define USE_FLOAT_ACTIVITY2
39
40 //=================================================================================================
41 // Public interface:
42
43 struct sat_solver2_t;
44 typedef struct sat_solver2_t sat_solver2;
45 typedef struct Int2_Man_t_ Int2_Man_t;
46
47 extern sat_solver2* sat_solver2_new(void);
48 extern void sat_solver2_delete(sat_solver2* s);
49
50 extern int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end, int Id);
51 extern int sat_solver2_simplify(sat_solver2* s);
52 extern int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
53 extern void sat_solver2_rollback(sat_solver2* s);
54 extern void sat_solver2_reducedb(sat_solver2* s);
55 extern double sat_solver2_memory( sat_solver2* s, int fAll );
56 extern double sat_solver2_memory_proof( sat_solver2* s );
57
58 extern void sat_solver2_setnvars(sat_solver2* s,int n);
59
60 extern void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
61 extern void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * p );
62 extern int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars );
63 extern void Sat_Solver2DoubleClauses( sat_solver2 * p, int iVar );
64
65 // global variables
66 extern int var_is_assigned(sat_solver2* s, int v);
67 extern int var_is_partA (sat_solver2* s, int v);
68 extern void var_set_partA (sat_solver2* s, int v, int partA);
69
70 // proof-based APIs
71 extern void * Sat_ProofCore( sat_solver2 * s );
72 extern void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars );
73 extern word * Sat_ProofInterpolantTruth( sat_solver2 * s, void * pGloVars );
74 extern void Sat_ProofCheck( sat_solver2 * s );
75
76 // interpolation APIs
77 extern Int2_Man_t * Int2_ManStart( sat_solver2 * pSat, int * pGloVars, int nGloVars );
78 extern void Int2_ManStop( Int2_Man_t * p );
79 extern int Int2_ManChainStart( Int2_Man_t * p, clause * c );
80 extern int Int2_ManChainResolve( Int2_Man_t * p, clause * c, int iLit, int varA );
81 extern void * Int2_ManReadInterpolant( sat_solver2 * s );
82
83
84 //=================================================================================================
85 // Solver representation:
86
87 struct varinfo_t;
88 typedef struct varinfo2_t varinfo2;
89
90 struct sat_solver2_t
91 {
92 int size; // nof variables
93 int cap; // size of varmaps
94 int qhead; // Head index of queue.
95 int qtail; // Tail index of queue.
96
97 int root_level; // Level of first proper decision.
98 double random_seed;
99 double progress_estimate;
100 int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything // activities
101
102 #ifdef USE_FLOAT_ACTIVITY2
103 double var_inc; // Amount to bump next variable with.
104 double var_decay; // INVERSE decay factor for variable activity: stores 1/decay.
105 float cla_inc; // Amount to bump next clause with.
106 float cla_decay; // INVERSE decay factor for clause activity: stores 1/decay.
107 double* activity; // A heuristic measurement of the activity of a variable.
108 #else
109 int var_inc; // Amount to bump next variable with.
110 int var_inc2; // Amount to bump next variable with.
111 int cla_inc; // Amount to bump next clause with.
112 unsigned* activity; // A heuristic measurement of the activity of a variable
113 unsigned* activity2; // backup variable activity
114 #endif
115
116 int nUnits; // the total number of unit clauses
117 int nof_learnts; // the number of clauses to trigger reduceDB
118 int nLearntMax; // enables using reduce DB method
119 int nLearntStart; // starting learned clause limit
120 int nLearntDelta; // delta of learned clause limit
121 int nLearntRatio; // ratio percentage of learned clauses
122 int nDBreduces; // number of DB reductions
123 int fNotUseRandom; // do not allow random decisions with a fixed probability
124 int fSkipSimplify; // set to one to skip simplification of the clause database
125 int fProofLogging; // enable proof-logging
126 int fVerbose;
127
128 // clauses
129 Sat_Mem_t Mem;
130 veci* wlists; // watcher lists (for each literal)
131 veci act_clas; // clause activities
132 veci claProofs; // clause proofs
133
134 // rollback
135 int iVarPivot; // the pivot for variables
136 int iTrailPivot; // the pivot for trail
137 int hProofPivot; // the pivot for proof records
138
139 // internal state
140 varinfo2 * vi; // variable information
141 int* levels; //
142 char* assigns; //
143 lit* trail; // sequence of assignment and implications
144 int* orderpos; // Index in variable order.
145 cla* reasons; // reason clauses
146 cla* units; // unit clauses
147 int* model; // If problem is solved, this vector contains the model (contains: lbool).
148
149 veci tagged; // (contains: var)
150 veci stack; // (contains: var)
151 veci order; // Variable order. (heap) (contains: var)
152 veci trail_lim; // Separator indices for different decision levels in 'trail'. (contains: int)
153 veci temp_clause; // temporary storage for a CNF clause
154 veci conf_final; // If problem is unsatisfiable (possibly under assumptions),
155 // this vector represent the final conflict clause expressed in the assumptions.
156 veci mark_levels; // temporary storage for labeled levels
157 veci min_lit_order; // ordering of removable literals
158 veci min_step_order; // ordering of resolution steps
159 veci learnt_live; // remaining clauses after reduce DB
160
161 // proof logging
162 Vec_Set_t * pPrf1; // sequence of proof records
163 veci temp_proof; // temporary place to store proofs
164 int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
165 int hProofLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
166 Prf_Man_t * pPrf2; // another proof manager
167 double dPrfMemory; // memory used by the proof-logger
168 Int2_Man_t * pInt2; // interpolation manager
169 int tempInter; // temporary storage for the interpolant
170
171 // statistics
172 stats_t stats;
173 ABC_INT64_T nConfLimit; // external limit on the number of conflicts
174 ABC_INT64_T nInsLimit; // external limit on the number of implications
175 abctime nRuntimeLimit; // external limit on runtime
176 };
177
clause2_read(sat_solver2 * s,cla h)178 static inline clause * clause2_read( sat_solver2 * s, cla h ) { return Sat_MemClauseHand( &s->Mem, h ); }
clause2_proofid(sat_solver2 * s,clause * c,int varA)179 static inline int clause2_proofid(sat_solver2* s, clause* c, int varA) { return c->lrn ? (veci_begin(&s->claProofs)[clause_id(c)]<<2) | (varA<<1) : (clause_id(c)<<2) | (varA<<1) | 1; }
180
181 // these two only work after creating a clause before the solver is called
clause2_is_partA(sat_solver2 * s,int h)182 static inline int clause2_is_partA (sat_solver2* s, int h) { return clause2_read(s, h)->partA; }
clause2_set_partA(sat_solver2 * s,int h,int partA)183 static inline void clause2_set_partA(sat_solver2* s, int h, int partA) { clause2_read(s, h)->partA = partA; }
clause2_id(sat_solver2 * s,int h)184 static inline int clause2_id(sat_solver2* s, int h) { return clause_id(clause2_read(s, h)); }
clause2_set_id(sat_solver2 * s,int h,int id)185 static inline void clause2_set_id(sat_solver2* s, int h, int id) { clause_set_id(clause2_read(s, h), id); }
186
187 //=================================================================================================
188 // Public APIs:
189
sat_solver2_nvars(sat_solver2 * s)190 static inline int sat_solver2_nvars(sat_solver2* s)
191 {
192 return s->size;
193 }
194
sat_solver2_nclauses(sat_solver2 * s)195 static inline int sat_solver2_nclauses(sat_solver2* s)
196 {
197 return (int)s->stats.clauses;
198 }
199
sat_solver2_nlearnts(sat_solver2 * s)200 static inline int sat_solver2_nlearnts(sat_solver2* s)
201 {
202 return (int)s->stats.learnts;
203 }
204
sat_solver2_nconflicts(sat_solver2 * s)205 static inline int sat_solver2_nconflicts(sat_solver2* s)
206 {
207 return (int)s->stats.conflicts;
208 }
209
sat_solver2_var_value(sat_solver2 * s,int v)210 static inline int sat_solver2_var_value( sat_solver2* s, int v )
211 {
212 assert( v >= 0 && v < s->size );
213 return (int)(s->model[v] == l_True);
214 }
sat_solver2_var_literal(sat_solver2 * s,int v)215 static inline int sat_solver2_var_literal( sat_solver2* s, int v )
216 {
217 assert( v >= 0 && v < s->size );
218 return toLitCond( v, s->model[v] != l_True );
219 }
sat_solver2_act_var_clear(sat_solver2 * s)220 static inline void sat_solver2_act_var_clear(sat_solver2* s)
221 {
222 int i;
223 for (i = 0; i < s->size; i++)
224 s->activity[i] = 0;//.0;
225 s->var_inc = 1.0;
226 }
227
sat_solver2_final(sat_solver2 * s,int ** ppArray)228 static inline int sat_solver2_final(sat_solver2* s, int ** ppArray)
229 {
230 *ppArray = s->conf_final.ptr;
231 return s->conf_final.size;
232 }
233
sat_solver2_set_runtime_limit(sat_solver2 * s,abctime Limit)234 static inline abctime sat_solver2_set_runtime_limit(sat_solver2* s, abctime Limit)
235 {
236 abctime temp = s->nRuntimeLimit;
237 s->nRuntimeLimit = Limit;
238 return temp;
239 }
240
sat_solver2_set_learntmax(sat_solver2 * s,int nLearntMax)241 static inline int sat_solver2_set_learntmax(sat_solver2* s, int nLearntMax)
242 {
243 int temp = s->nLearntMax;
244 s->nLearntMax = nLearntMax;
245 return temp;
246 }
247
sat_solver2_bookmark(sat_solver2 * s)248 static inline void sat_solver2_bookmark(sat_solver2* s)
249 {
250 assert( s->qhead == s->qtail );
251 s->iVarPivot = s->size;
252 s->iTrailPivot = s->qhead;
253 if ( s->pPrf1 )
254 s->hProofPivot = Vec_SetHandCurrent(s->pPrf1);
255 Sat_MemBookMark( &s->Mem );
256 if ( s->activity2 )
257 {
258 s->var_inc2 = s->var_inc;
259 memcpy( s->activity2, s->activity, sizeof(unsigned) * s->iVarPivot );
260 }
261 }
262
sat_solver2_add_const(sat_solver2 * pSat,int iVar,int fCompl,int fMark,int Id)263 static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark, int Id )
264 {
265 lit Lits[1];
266 int Cid;
267 assert( iVar >= 0 );
268
269 Lits[0] = toLitCond( iVar, fCompl );
270 Cid = sat_solver2_addclause( pSat, Lits, Lits + 1, Id );
271 if ( fMark )
272 clause2_set_partA( pSat, Cid, 1 );
273 return 1;
274 }
sat_solver2_add_buffer(sat_solver2 * pSat,int iVarA,int iVarB,int fCompl,int fMark,int Id)275 static inline int sat_solver2_add_buffer( sat_solver2 * pSat, int iVarA, int iVarB, int fCompl, int fMark, int Id )
276 {
277 lit Lits[2];
278 int Cid;
279 assert( iVarA >= 0 && iVarB >= 0 );
280
281 Lits[0] = toLitCond( iVarA, 0 );
282 Lits[1] = toLitCond( iVarB, !fCompl );
283 Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id );
284 if ( fMark )
285 clause2_set_partA( pSat, Cid, 1 );
286
287 Lits[0] = toLitCond( iVarA, 1 );
288 Lits[1] = toLitCond( iVarB, fCompl );
289 Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id );
290 if ( fMark )
291 clause2_set_partA( pSat, Cid, 1 );
292 return 2;
293 }
sat_solver2_add_and(sat_solver2 * pSat,int iVar,int iVar0,int iVar1,int fCompl0,int fCompl1,int fMark,int Id)294 static inline int sat_solver2_add_and( sat_solver2 * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fMark, int Id )
295 {
296 lit Lits[3];
297 int Cid;
298
299 Lits[0] = toLitCond( iVar, 1 );
300 Lits[1] = toLitCond( iVar0, fCompl0 );
301 Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id );
302 if ( fMark )
303 clause2_set_partA( pSat, Cid, 1 );
304
305 Lits[0] = toLitCond( iVar, 1 );
306 Lits[1] = toLitCond( iVar1, fCompl1 );
307 Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id );
308 if ( fMark )
309 clause2_set_partA( pSat, Cid, 1 );
310
311 Lits[0] = toLitCond( iVar, 0 );
312 Lits[1] = toLitCond( iVar0, !fCompl0 );
313 Lits[2] = toLitCond( iVar1, !fCompl1 );
314 Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id );
315 if ( fMark )
316 clause2_set_partA( pSat, Cid, 1 );
317 return 3;
318 }
sat_solver2_add_xor(sat_solver2 * pSat,int iVarA,int iVarB,int iVarC,int fCompl,int fMark,int Id)319 static inline int sat_solver2_add_xor( sat_solver2 * pSat, int iVarA, int iVarB, int iVarC, int fCompl, int fMark, int Id )
320 {
321 lit Lits[3];
322 int Cid;
323 assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
324
325 Lits[0] = toLitCond( iVarA, !fCompl );
326 Lits[1] = toLitCond( iVarB, 1 );
327 Lits[2] = toLitCond( iVarC, 1 );
328 Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id );
329 if ( fMark )
330 clause2_set_partA( pSat, Cid, 1 );
331
332 Lits[0] = toLitCond( iVarA, !fCompl );
333 Lits[1] = toLitCond( iVarB, 0 );
334 Lits[2] = toLitCond( iVarC, 0 );
335 Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id );
336 if ( fMark )
337 clause2_set_partA( pSat, Cid, 1 );
338
339 Lits[0] = toLitCond( iVarA, fCompl );
340 Lits[1] = toLitCond( iVarB, 1 );
341 Lits[2] = toLitCond( iVarC, 0 );
342 Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id );
343 if ( fMark )
344 clause2_set_partA( pSat, Cid, 1 );
345
346 Lits[0] = toLitCond( iVarA, fCompl );
347 Lits[1] = toLitCond( iVarB, 0 );
348 Lits[2] = toLitCond( iVarC, 1 );
349 Cid = sat_solver2_addclause( pSat, Lits, Lits + 3, Id );
350 if ( fMark )
351 clause2_set_partA( pSat, Cid, 1 );
352 return 4;
353 }
sat_solver2_add_constraint(sat_solver2 * pSat,int iVar,int iVar2,int fCompl,int fMark,int Id)354 static inline int sat_solver2_add_constraint( sat_solver2 * pSat, int iVar, int iVar2, int fCompl, int fMark, int Id )
355 {
356 lit Lits[2];
357 int Cid;
358 assert( iVar >= 0 );
359
360 Lits[0] = toLitCond( iVar, fCompl );
361 Lits[1] = toLitCond( iVar2, 0 );
362 Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id );
363 if ( fMark )
364 clause2_set_partA( pSat, Cid, 1 );
365
366 Lits[0] = toLitCond( iVar, fCompl );
367 Lits[1] = toLitCond( iVar2, 1 );
368 Cid = sat_solver2_addclause( pSat, Lits, Lits + 2, Id );
369 if ( fMark )
370 clause2_set_partA( pSat, Cid, 1 );
371 return 2;
372 }
373
374
375 ABC_NAMESPACE_HEADER_END
376
377 #endif
378