1 /***************************************************************************
2 Copyright (c) 2009, Armin Biere, Johannes Kepler University.
4 Permission is hereby granted, free of charge, to any person obtaining a copy
5 of this software and associated documentation files (the "Software"), to
6 deal in the Software without restriction, including without limitation the
7 rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
8 sell copies of the Software, and to permit persons to whom the Software is
9 furnished to do so, subject to the following conditions:
11 The above copyright notice and this permission notice shall be included in
12 all copies or substantial portions of the Software.
14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
19 FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
21 ****************************************************************************/
23 #include "precosat.hh"
24 #include "precobnr.hh"
33 #include <sys/resource.h>
34 #include <sys/unistd.h>
42 do { std::cout << prfx << "LOG " << code << std::endl; } while (false)
44 #define LOG(code) do { } while (false)
50 do { std::cout << prfx << "COVER " << __FUNCTION__ << ' ' \
51 << __LINE__ << ' ' << code << std::endl; } while (false)
53 #define COVER(code) do { } while (false)
58 #warning "PRECOCHECK enabled"
62 #define INC(s) do { stats.s++; } while (0)
64 #define INC(s) do { } while (0)
69 template<class T
> inline static void swap (T
& a
, T
& b
)
70 { T tmp
= a
; a
= b
; b
= tmp
; }
72 template<class T
> inline static const T
min (const T a
, const T b
)
73 { return a
< b
? a
: b
; }
75 template<class T
> inline static const T
max (const T a
, const T b
)
76 { return a
> b
? a
: b
; }
78 template<class T
> inline static void fix (T
* & p
, long moved
)
79 { char * q
= (char*) p
; q
+= moved
; p
= (T
*) q
; }
81 inline static int logsize (int size
) { return (128 >> size
) + 1; }
83 static inline Val
lit2val (int lit
) { return (lit
& 1) ? -1 : 1; }
85 static inline Cls
* lit2conflict (Cls
& bins
, int a
, int b
) {
88 assert (!bins
.lits
[2]);
92 static inline unsigned ggt (unsigned a
, unsigned b
)
93 { while (b
) { unsigned r
= a
% b
; a
= b
, b
= r
; } return a
; }
95 inline static unsigned minuscap (unsigned a
, unsigned b
)
96 { return (a
<= b
) ? 0 : (a
- b
); }
98 static inline double mb (size_t bytes
)
99 { return bytes
/ (double) (1<<20); }
101 static inline bool sigsubs (unsigned s
, unsigned t
)
104 static inline unsigned listig (int lit
)
105 { return (1u << (31u & (unsigned)(lit
/2))); }
107 static inline double average (double a
, double b
) { return b
? a
/b
: 0; }
109 static inline double percent (double a
, double b
) { return 100*average(a
,b
); }
111 static bool parity (unsigned x
)
112 { bool res
= false; while (x
) res
= !res
, x
&= x
-1; return res
; }
115 using namespace PrecoSat
;
117 inline unsigned RNG::next () {
118 unsigned res
= state
;
120 state
+= 1013904223u;
124 inline bool RNG::oneoutof (unsigned spread
) {
125 return spread
? !(next () % spread
) : true;
128 inline size_t Cls::bytes (int n
) {
129 return sizeof (Cls
) + (n
- 3 + 1) * sizeof (int);
132 inline size_t Cls::bytes () const { return bytes (size
); }
134 inline Anchor
<Cls
> & Solver::anchor (Cls
* c
) {
135 if (c
->binary
) return binary
;
136 if (!c
->lnd
) return original
;
137 if (c
->fresh
) return fresh
;
138 return learned
[c
->glue
];
141 inline int Cls::minlit () const {
142 int res
= INT_MAX
, other
;
143 for (const int * p
= lits
; (other
= *p
); p
++)
144 if (other
< res
) res
= other
;
148 inline bool Cls::contains (int lit
) const {
149 if (!(sig
& listig (lit
))) return false;
150 for (const int * p
= lits
; *p
; p
++)
151 if (*p
== lit
) return true;
155 inline void Solver::setsig (Cls
* cls
) {
156 int except
= cls
->minlit (), lit
;
157 unsigned fwsig
= 0, bwsig
= 0;
158 for (const int * p
= cls
->lits
; (lit
= *p
); p
++) {
159 unsigned sig
= listig (lit
);
161 if (lit
!= except
) fwsig
|= sig
;
164 for (const int * p
= cls
->lits
; (lit
= *p
); p
++)
165 bwsigs
[lit
] |= bwsig
;
167 fwsigs
[except
] |= fwsig
;
170 inline unsigned Solver::litsig () {
172 for (int i
= 0; i
< lits
; i
++)
173 res
|= listig (lits
[i
]);
177 inline bool Solver::clt (int a
, int b
) const {
178 Var
& u
= vars
[a
/2], &v
= vars
[b
/2];
179 int l
= u
.dlevel
, k
= v
.dlevel
;
180 if (l
< 0) return false;
181 if (k
< 0) return true;
182 if (l
< k
) return true;
183 if (l
> k
) return false;
184 Val r
= vals
[a
], s
= vals
[b
];
185 if (r
< s
) return true;
189 inline void Solver::connect (Cls
* c
) {
190 for (int i
= 0; i
<= 1; i
++) {
191 int lit
, * r
= c
->lits
+ i
, * q
= r
, best
= *q
;
192 for (int * p
= q
+ 1; (lit
= *p
); p
++)
193 if (clt (best
, lit
)) q
= p
, best
= lit
;
196 assert (c
->lits
[0] && c
->lits
[1]);
197 Anchor
<Cls
> & a
= anchor (c
);
198 if (!connected (a
, c
)) push (a
, c
);
200 for (int i
= 0; i
<= 1; i
++)
201 occs
[c
->lits
[i
]].bins
.push (mem
, c
->lits
[!i
]);
203 for (int i
= 0; i
<= 1; i
++)
204 occs
[c
->lits
[i
]].large
.push (mem
, Occ (c
->lits
[!i
], c
));
207 for (const int * p
= c
->lits
; *p
; p
++)
208 orgs
[*p
].push (mem
, c
);
209 if (fwds
) fwds
[c
->minlit ()].push (mem
, c
);
213 inline void Solver::disconnect (Cls
* c
) {
214 assert (!c
->locked
&& !c
->dirty
&& !c
->trash
);
215 int l0
= c
->lits
[0], l1
= c
->lits
[1];
217 Anchor
<Cls
> & a
= anchor (c
);
218 if (connected (a
, c
)) dequeue (a
, c
);
220 occs
[l0
].bins
.remove(l1
);
221 occs
[l1
].bins
.remove(l0
);
223 occs
[l0
].large
.remove(Occ(0,c
));
224 occs
[l1
].large
.remove(Occ(0,c
));
226 if (fwds
) fwds
[c
->minlit ()].remove (c
);
227 if (!orgs
|| c
->lnd
) return;
228 for (const int * p
= c
->lits
; *p
; p
++)
232 inline Rnk
* Solver::prb (const Rnk
* r
) { return prbs
+ (r
- rnks
); }
233 inline Rnk
* Solver::rnk (const Var
* v
) { return rnks
+ (v
- vars
); }
234 inline Var
* Solver::var (const Rnk
* r
) { return vars
+ (r
- rnks
); }
236 inline Val
Solver::fixed (int lit
) const {
237 return vars
[lit
/2].dlevel
? 0 : vals
[lit
];
240 inline void Solver::collect (Cls
* cls
) {
241 assert (!cls
->locked
&& !cls
->dirty
&& !cls
->trash
&& !cls
->gate
);
242 if (cls
->binary
) assert (stats
.clauses
.bin
), stats
.clauses
.bin
--;
243 else if (cls
->lnd
) assert (stats
.clauses
.lnd
), stats
.clauses
.lnd
--;
244 else assert (stats
.clauses
.orig
), stats
.clauses
.orig
--;
245 if (!cls
->lnd
) assert (stats
.clauses
.irr
), stats
.clauses
.irr
--;
246 size_t bytes
= cls
->bytes ();
249 for (const int * p
= cls
->lits
; *p
; p
++)
250 check
.push (mem
, *p
);
255 dbgprint ("LOG recycle clause ", cls
);
257 mem
.deallocate (cls
, bytes
);
258 stats
.collected
+= bytes
;
262 void Solver::touchblkd (int lit
) {
264 int idx
= lit
/2, notlit
= lit
^1;
265 Var
* v
= vars
+ idx
;
266 if (v
->type
!= FREE
) return;
267 assert (!val (lit
) && !repr
[lit
]);
268 Rnk
* r
= blks
+ notlit
;
270 int nh
= -orgs
[lit
], oh
= r
->heat
; r
->heat
= nh
;
271 if (oh
== nh
&& schedule
.block
.contains (r
)) return;
272 if (oh
== nh
) LOG ("touchblkd " << notlit
<< " again " << nh
);
273 else LOG ("touchblkd " << notlit
<< " from " << oh
<< " to " << nh
);
274 if (!schedule
.block
.contains (r
)) schedule
.block
.push (mem
, r
);
275 else if (nh
> oh
) schedule
.block
.up (r
);
276 else if (nh
< oh
) schedule
.block
.down (r
);
279 void Solver::touchelim (int lit
) {
283 Var
* v
= vars
+ idx
;
284 if (v
->type
!= FREE
) return;
285 assert (!val (lit
) && !repr
[lit
]);
286 if (idx
== elimvar
) return;
287 Rnk
* r
= elms
+ idx
;
290 int neg
= orgs
[1^lit
];
291 long long tmp
= -(((long long)pos
) * (long long) neg
);
292 int nh
= (tmp
>= INT_MIN
) ? (int) tmp
: INT_MIN
;
293 int oh
= r
->heat
; r
->heat
= nh
;
294 if (oh
== nh
&& schedule
.elim
.contains (r
)) return;
295 if (oh
== nh
) LOG ("touchelim " << lit
<< " again " << nh
);
296 else LOG ("touchelim " << lit
<< " from " << oh
<< " to " << nh
);
297 if (pos
> 1 && neg
> 1 && nh
<= opts
.elimin
) {
298 if (schedule
.elim
.contains (r
)) {
299 schedule
.elim
.remove (r
);
301 } else if (!schedule
.elim
.contains (r
)) schedule
.elim
.push (mem
, r
);
302 else if (nh
> oh
) schedule
.elim
.up (r
);
303 else if (nh
< oh
) schedule
.elim
.down (r
);
306 void Solver::touchpure (int lit
) {
309 Var
* v
= vars
+ idx
;
310 if (v
->onplits
) return;
311 LOG ("touchpure " << lit
);
313 plits
.push (mem
, idx
);
316 void Solver::touch (int lit
) {
317 assert (elimode
+ blkmode
== 1);
318 if (elimode
) touchelim (lit
);
319 else touchblkd (lit
);
320 if (puremode
) touchpure (lit
);
323 void Solver::touch (Cls
* c
) {
324 assert (asymode
|| !c
->lnd
);
325 assert (elimode
|| blkmode
);
326 for (int * p
= c
->lits
; *p
; p
++)
330 inline void Solver::recycle (Cls
* c
) {
333 if (c
->trash
) trash
.remove (c
);
334 if (c
->gate
) cleangate ();
335 if (c
->str
) strnd
.remove (c
);
336 if (elimode
|| blkmode
) touch (c
);
340 inline void Solver::dump (Cls
* c
) {
342 if (c
->trash
) return;
347 inline void Solver::cleantrash () {
349 int old
= stats
.clauses
.orig
;
351 Cls
* cls
= trash
.pop ();
359 inline void Solver::gcls (Cls
* c
) {
365 inline void Solver::strcls (Cls
* c
) {
371 inline void Solver::cleangate () {
373 Cls
* cls
= gate
.pop ();
374 assert (cls
->gate
); cls
->gate
= false;
381 inline void Solver::recycle (int lit
) {
382 LOG ("recycle literal " << lit
);
385 Var
* v
= vars
+ (lit
/2); Vrt t
= v
->type
;
386 assert (t
== FIXED
|| t
== PURE
|| t
== ZOMBIE
|| t
== ELIM
);
389 while (int size
= orgs
[lit
]) recycle (orgs
[lit
][size
- 1]);
390 orgs
[lit
].release (mem
);
391 occs
[lit
].bins
.release (mem
);
392 occs
[lit
].large
.release (mem
);
395 Opt::Opt (const char * n
, int v
, int * vp
, int mi
, int ma
) :
396 name (n
), valptr (vp
), min (mi
), max (ma
)
403 bool Opts::set (const char * opt
, int val
) {
404 for (Opt
* o
= opts
.begin (); o
< opts
.end (); o
++)
405 if (!strcmp (o
->name
, opt
)) {
406 if (val
< o
->min
) return false;
407 if (val
> o
->max
) return false;
414 bool Opts::set (const char * opt
, const char * val
) {
415 if (strcmp (opt
, "output")) return false;
420 void Opts::add (Mem
& mem
, const char * n
, int v
, int * vp
, int mi
, int ma
) {
421 opts
.push (mem
, Opt (n
, v
, vp
, mi
, ma
));
424 void Opts::printoptions (FILE * file
, const char * prfx
) const {
426 int lenprfx
= strlen (prfx
);
427 fputs (prfx
, file
); int pos
= 0;
428 const Opt
* o
= opts
.begin ();
429 while (o
< opts
.end ()) {
431 sprintf (line
, " --%s=%d", o
->name
, *o
->valptr
);
432 int len
= strlen (line
); assert (len
< 80);
433 if (len
+ pos
>= 77 - lenprfx
) {
434 fprintf (file
, "\n%s", prfx
);
444 fprintf (file
, "%s\n%s --output=%s\n", prfx
, prfx
, output
);
447 void Solver::initbwsigs () {
449 size_t bytes
= 2 * size
* sizeof *bwsigs
;
450 bwsigs
= (unsigned*) mem
.callocate (bytes
);
453 void Solver::rszbwsigs (int newsize
) {
455 size_t old_bytes
= 2 * size
* sizeof *bwsigs
;
456 size_t new_bytes
= 2 * newsize
* sizeof *bwsigs
;
457 bwsigs
= (unsigned*) mem
.recallocate (bwsigs
, old_bytes
, new_bytes
);
460 void Solver::clrbwsigs () {
461 size_t bytes
= 2 * size
* sizeof *bwsigs
;
462 memset (bwsigs
, 0, bytes
);
465 void Solver::delbwsigs () {
466 size_t bytes
= 2 * size
* sizeof *bwsigs
;
467 mem
.deallocate (bwsigs
, bytes
);
471 void Solver::initorgs () {
472 size_t bytes
= 2 * (maxvar
+ 1) * sizeof *orgs
;
473 orgs
= (Orgs
*) mem
.callocate (bytes
);
476 void Solver::delorgs () {
477 for (int lit
= 2; lit
<= 2*maxvar
+1; lit
++) orgs
[lit
].release (mem
);
478 size_t bytes
= 2 * (maxvar
+ 1) * sizeof *orgs
;
479 mem
.deallocate (orgs
, bytes
);
483 void Solver::initfwds () {
484 size_t bytes
= 2 * (maxvar
+ 1) * sizeof *fwds
;
485 fwds
= (Fwds
*) mem
.callocate (bytes
);
488 void Solver::delfwds () {
489 for (int lit
= 2; lit
<= 2*maxvar
+1; lit
++) fwds
[lit
].release (mem
);
490 size_t bytes
= 2 * (maxvar
+ 1) * sizeof *fwds
;
491 mem
.deallocate (fwds
, bytes
);
495 void Solver::initfwsigs () {
497 size_t bytes
= 2 * (maxvar
+ 1) * sizeof *fwsigs
;
498 fwsigs
= (unsigned*) mem
.callocate (bytes
);
501 void Solver::delfwsigs () {
502 size_t bytes
= 2 * (maxvar
+ 1) * sizeof *fwsigs
;
503 mem
.deallocate (fwsigs
, bytes
);
507 void Solver::initprfx (const char * newprfx
) {
508 prfx
= (char*) mem
.allocate (strlen (newprfx
) + 1);
509 strcpy (prfx
, newprfx
);
512 void Solver::delprfx () {
514 mem
.deallocate (prfx
, strlen (prfx
) + 1);
517 #define OPT(n,v,mi,ma) \
518 do { opts.add (mem, # n, v, &opts.n, mi, ma); } while (0)
520 void Solver::initerm (void) {
521 terminal
= (out
== stdout
) && isatty(1);
524 void Solver::init (int initialmaxvar
)
526 maxvar
= initialmaxvar
;
528 while (maxvar
>= size
)
547 assert (!initialized
);
549 vars
= (Var
*) mem
.callocate (size
* sizeof *vars
);
550 for (int i
= 1; i
<= maxvar
; i
++)
555 blks
= (Rnk
*) mem
.allocate (2 * size
* sizeof *blks
);
556 elms
= (Rnk
*) mem
.allocate (size
* sizeof *elms
);
557 jwhs
= (int*) mem
.callocate (2 * size
* sizeof *jwhs
);
558 occs
= (Occs
*) mem
.callocate (2 * size
* sizeof *occs
);
559 prbs
= (Rnk
*) mem
.allocate (size
* sizeof *prbs
);
560 repr
= (int*) mem
.callocate (2 * size
* sizeof *repr
);
561 rnks
= (Rnk
*) mem
.allocate (size
* sizeof *rnks
);
562 vals
= (Val
*) mem
.callocate (2 * size
* sizeof *vals
);
564 for (Rnk
* p
= rnks
+ maxvar
; p
> rnks
; p
--)
565 p
->heat
= 0, p
->pos
= -1, schedule
.decide
.push (mem
, p
);
567 for (Rnk
* p
= prbs
+ maxvar
; p
> prbs
; p
--) p
->heat
= 0, p
->pos
= -1;
568 for (Rnk
* p
= elms
+ maxvar
; p
> elms
; p
--) p
->heat
= 0, p
->pos
= -1;
569 for (Rnk
* p
= blks
+ 2*maxvar
+1; p
> blks
+1; p
--) p
->heat
= 0, p
->pos
= -1;
578 frames
.push (mem
, Frame (trail
));
583 int m
= INT_MIN
, M
= INT_MAX
;
591 OPT (simprd
,20,0,M
); OPT (simpinc
,26,0,100); OPT (simprtc
,0,0,2);
593 OPT (dominate
,1,0,1);
594 OPT (maxdoms
,5*1000*1000,0,M
);
597 OPT (blockrtc
,0,0,2); OPT (blockimpl
,1,0,1);
598 OPT (blockprd
,10,1,M
); OPT (blockint
,300*1000,0,M
);
599 OPT (blockotfs
,1,0,1);
600 OPT (blockreward
,100,0,10000);
601 OPT (blockboost
,3,0,100);
602 OPT (heatinc
,10,0,100);
604 OPT (restart
,1,0,1); OPT (restartint
,100,1,M
);
605 OPT (restartinner
,10,0,1000); OPT (restartouter
,10,0,1000);
606 OPT (rebias
,1,0,1); OPT (rebiasint
,1000,1,M
);
608 OPT (probeint
,100*1000,1000,M
); OPT (probeprd
,10,1,M
);
609 OPT (probertc
,0,0,2); OPT (probereward
,2000,0,10000);
610 OPT (probeboost
,5,0,10000);
611 OPT (decompose
,1,0,1);
612 OPT (inverse
,0,0,1); OPT (inveager
,0,0,1);
613 OPT (mtfall
,0,0,1); OPT (mtfrev
,1,0,1);
615 OPT (bumpsort
,1,0,1); OPT (bumprev
,1,0,1);
616 OPT (bumpturbo
,0,0,1); OPT (bumpbulk
,0,0,1);
617 OPT (fresh
,50,0,100);
618 OPT (glue
,Cls::MAXGLUE
,0,Cls::MAXGLUE
);
619 OPT (slim
,1,0,1); OPT (sticky
,1,0,Cls::MAXGLUE
);
621 OPT (minimize
,4,0,4); OPT (maxdepth
,1000,2,10000); OPT (strength
,100,0,M
);
623 OPT (elimgain
,0,m
/2,M
/2);
624 OPT (elimint
,300*1000,0,M
); OPT (elimprd
,20,1,M
);
626 OPT (elimin
,-10000,-m
,M
);
627 OPT (elimclim
,20,0,M
);
628 OPT (elimboost
,1,0,100);
629 OPT (elimreward
,100,0,10000);
630 OPT (elimasym
,2,1,100);
631 OPT (elimasymint
,100000,100,M
);
632 OPT (elimasymreward
,1000,0,M
);
633 OPT (fwmaxlen
,100,0,M
);OPT (bwmaxlen
,1000,0,M
); OPT (reslim
,20,0,M
);
634 OPT (blkmaxlen
,1000,0,M
);
635 OPT (subst
,1,0,1); OPT (ands
,1,0,1); OPT (xors
,1,0,1); OPT (ites
,1,0,1);
636 OPT (minlimit
,500,10,10000); OPT (maxlimit
,3*1000*1000,100,M
);
637 OPT (dynred
,4,-1,100000);
638 OPT (liminitmode
,1,0,1);
639 OPT (limincmode
,0,0,1);
640 OPT (liminitconst
,2000,0,1000*1000);
641 OPT (liminitmax
,20000,0,10*1000*1000);
642 OPT (liminitpercent
,10,0,1000);
643 OPT (liminconst1
,2000,0,100*1000);
644 OPT (liminconst2
,1000,0,100*1000);
645 OPT (limincpercent
,10,0,1000);
646 OPT (enlinc
,20,0,1000);
647 OPT (shrink
,2,0,2); OPT (shrinkfactor
,100,1,1000);
648 OPT (random
,1,0,1); OPT (spread
,2000,0,M
); OPT (seed
,0,0,M
);
650 opts
.set ("output", (const char*) 0);
656 void Solver::initiirfs () {
657 if (opts
.order
< 2) return;
658 size_t bytes
= size
* (opts
.order
- 1) * sizeof *iirfs
;
659 iirfs
= (int *) mem
.allocate (bytes
);
660 for (Var
* v
= vars
+ 1; v
<= vars
+ maxvar
; v
++)
661 for (int i
= 1; i
< opts
.order
; i
++)
665 void Solver::rsziirfs (int newsize
) {
666 if (opts
.order
< 2) return;
667 size_t old_bytes
= size
* (opts
.order
- 1) * sizeof *iirfs
;
668 size_t new_bytes
= newsize
* (opts
.order
- 1) * sizeof *iirfs
;
669 iirfs
= (int *) mem
.reallocate (iirfs
, old_bytes
, new_bytes
);
672 void Solver::deliirfs () {
674 assert (opts
.order
>= 2);
675 size_t bytes
= size
* (opts
.order
- 1) * sizeof *iirfs
;
676 mem
.deallocate (iirfs
, bytes
);
680 void Solver::delclauses (Anchor
<Cls
> & anchor
) {
682 for (Cls
* p
= anchor
.head
; p
; p
= prev
) {
683 p
->bytes (); prev
= p
->prev
; mem
.deallocate (p
, p
->bytes ());
685 anchor
.head
= anchor
.tail
= 0;
688 void Solver::reset () {
689 assert (initialized
);
694 for (int lit
= 2; lit
<= 2 * maxvar
+ 1; lit
++) occs
[lit
].bins
.release (mem
);
695 for (int lit
= 2; lit
<= 2 * maxvar
+ 1; lit
++) occs
[lit
].large
.release (mem
);
696 bytes
= 2 * size
* sizeof *occs
; mem
.deallocate (occs
, bytes
);
697 bytes
= 2 * size
* sizeof *vals
; mem
.deallocate (vals
, bytes
);
698 bytes
= 2 * size
* sizeof *repr
; mem
.deallocate (repr
, bytes
);
699 bytes
= 2 * size
* sizeof *jwhs
; mem
.deallocate (jwhs
, bytes
);
700 bytes
= 2 * size
* sizeof *blks
; mem
.deallocate (blks
, bytes
);
701 bytes
= size
* sizeof *vars
; mem
.deallocate (vars
, bytes
);
702 bytes
= size
* sizeof *prbs
; mem
.deallocate (prbs
, bytes
);
703 bytes
= size
* sizeof *rnks
; mem
.deallocate (rnks
, bytes
);
704 bytes
= size
* sizeof *elms
; mem
.deallocate (elms
, bytes
);
705 delclauses (original
);
707 for (int glue
= 0; glue
<= opts
.glue
; glue
++)
708 delclauses (learned
[glue
]);
710 if (iirfs
) deliirfs ();
711 if (orgs
) delorgs ();
712 if (fwds
) delfwds ();
713 if (bwsigs
) delbwsigs ();
714 if (fwsigs
) delfwsigs ();
715 schedule
.block
.release (mem
);
716 schedule
.elim
.release (mem
);
717 schedule
.decide
.release (mem
);
718 schedule
.probe
.release (mem
);
719 opts
.opts
.release (mem
);
721 frames
.release (mem
);
722 levels
.release (mem
);
739 void Solver::fxopts () {
740 assert (!opts
.fixed
);
743 if (!opts
.plain
) return;
755 void Solver::propts () {
757 opts
.printoptions (out
, prfx
);
761 void Solver::prstats () {
762 double overalltime
= stats
.seconds ();
763 fprintf (out
, "%s%d conflicts, %d decisions, %d random\n", prfx
,
764 stats
.conflicts
, stats
.decisions
, stats
.random
);
765 fprintf (out
, "%s%d iterations, %d restarts, %d skipped\n", prfx
,
766 stats
.iter
, stats
.restart
.count
, stats
.restart
.skipped
);
767 fprintf (out
, "%s%d enlarged, %d shrunken, %d rescored, %d rebiased\n", prfx
,
768 stats
.enlarged
, stats
.shrunken
, stats
.rescored
, stats
.rebias
.count
);
769 fprintf (out
, "%s%d simplifications, %d reductions\n", prfx
,
770 stats
.simps
, stats
.reductions
);
771 fprintf (out
, "%s\n", prfx
);
772 fprintf (out
, "%svars: %d fixed, %d equiv, %d elim, %d pure, %d zombies\n",
774 stats
.vars
.fixed
, stats
.vars
.equiv
,
775 stats
.vars
.elim
, stats
.vars
.pure
, stats
.vars
.zombies
);
776 fprintf (out
, "%selim: %lld resolutions, %d phases, %d rounds\n", prfx
,
777 stats
.elim
.resolutions
, stats
.elim
.phases
, stats
.elim
.rounds
);
778 fprintf (out
, "%sextd: %d forced, %d assumed, %d flipped\n", prfx
,
779 stats
.extend
.forced
, stats
.extend
.assumed
, stats
.extend
.flipped
);
780 fprintf (out
, "%ssbst: %.0f%% subst, "
781 "%.1f%% nots, %.1f%% ands, %.1f%% xors, %.1f%% ites\n", prfx
,
782 percent (stats
.vars
.subst
,stats
.vars
.elim
),
783 percent (stats
.subst
.nots
.count
,stats
.vars
.subst
),
784 percent (stats
.subst
.ands
.count
,stats
.vars
.subst
),
785 percent (stats
.subst
.xors
.count
,stats
.vars
.subst
),
786 percent (stats
.subst
.ites
.count
,stats
.vars
.subst
));
787 fprintf (out
, "%sarty: %.2f ands %.2f xors average arity\n", prfx
,
788 average (stats
.subst
.ands
.len
, stats
.subst
.ands
.count
),
789 average (stats
.subst
.xors
.len
, stats
.subst
.xors
.count
));
790 fprintf (out
, "%sprbe: %d probed, %d phases, %d rounds\n", prfx
,
791 stats
.probe
.variables
, stats
.probe
.phases
, stats
.probe
.rounds
);
792 fprintf (out
, "%sprbe: %d failed, %d lifted, %d merged\n", prfx
,
793 stats
.probe
.failed
, stats
.probe
.lifted
, stats
.probe
.merged
);
794 fprintf (out
, "%ssccs: %d non trivial, %d fixed, %d merged\n", prfx
,
795 stats
.sccs
.nontriv
, stats
.sccs
.fixed
, stats
.sccs
.merged
);
797 long long l1s
= stats
.sigs
.bw
.l1
.srch
+ stats
.sigs
.fw
.l1
.srch
;
798 long long l1h
= stats
.sigs
.bw
.l1
.hits
+ stats
.sigs
.fw
.l1
.hits
;
799 long long l2s
= stats
.sigs
.bw
.l2
.srch
+ stats
.sigs
.fw
.l2
.srch
;
800 long long l2h
= stats
.sigs
.bw
.l2
.hits
+ stats
.sigs
.fw
.l2
.hits
;
801 long long bws
= stats
.sigs
.bw
.l1
.srch
+ stats
.sigs
.bw
.l2
.srch
;
802 long long bwh
= stats
.sigs
.bw
.l1
.hits
+ stats
.sigs
.bw
.l2
.hits
;
803 long long fws
= stats
.sigs
.fw
.l1
.srch
+ stats
.sigs
.fw
.l2
.srch
;
804 long long fwh
= stats
.sigs
.fw
.l1
.hits
+ stats
.sigs
.fw
.l2
.hits
;
805 long long hits
= bwh
+ fwh
, srch
= bws
+ fws
;
806 if (opts
.verbose
> 1) {
807 fprintf (out
, "%ssigs: %13lld srch %3.0f%% hits, %3.0f%% L1, %3.0f%% L2\n",
809 srch
, percent (hits
,srch
), percent (l1h
,l1s
), percent(l2h
,l2s
));
811 "%s fw: %13lld %3.0f%% %3.0f%% hits, %3.0f%% L1, %3.0f%% L2\n",
813 fws
, percent (fws
,srch
), percent (fwh
,fws
),
814 percent (stats
.sigs
.fw
.l1
.hits
, stats
.sigs
.fw
.l1
.srch
),
815 percent (stats
.sigs
.fw
.l2
.hits
, stats
.sigs
.fw
.l2
.srch
));
817 "%s bw: %13lld %3.0f%% %3.0f%% hits, %3.0f%% L1, %3.0f%% L2\n",
819 bws
, percent (bws
,srch
), percent (bwh
,bws
),
820 percent (stats
.sigs
.bw
.l1
.hits
, stats
.sigs
.bw
.l1
.srch
),
821 percent (stats
.sigs
.bw
.l2
.hits
, stats
.sigs
.bw
.l2
.srch
));
824 "%ssigs: %lld searched, %.0f%% hits, %.0f%% L1, %.0f%% L2\n",
826 srch
, percent (hits
,srch
), percent (l1h
,l1s
), percent(l2h
,l2s
));
828 long long alllits
= stats
.lits
.added
+ stats
.mins
.deleted
;
830 "%smins: %lld lrnd, %.0f%% del, %lld strng, %lld inv, %d dpth\n",
833 percent (stats
.mins
.deleted
, alllits
),
834 stats
.mins
.strong
, stats
.mins
.inverse
, stats
.mins
.depth
);
836 "%ssubs: %d fw, %d bw, %d dynamic, %d org, %d doms, %d gc\n",
838 stats
.subs
.fw
, stats
.subs
.bw
,
839 stats
.subs
.dyn
, stats
.subs
.org
,
840 stats
.subs
.doms
, stats
.subs
.red
);
842 "%sblkd: %lld resolutions, %d phases, %d rounds\n",
844 stats
.blkd
.resolutions
,
845 stats
.blkd
.phases
, stats
.blkd
.rounds
);
847 "%sblkd: %d = %d implicit + %d explicit\n",
849 stats
.blkd
.impl
+ stats
.blkd
.expl
,
850 stats
.blkd
.impl
, stats
.blkd
.expl
);
851 assert (stats
.vars
.pure
==
852 stats
.pure
.elim
+ stats
.pure
.blkd
+ stats
.pure
.expl
);
853 fprintf (out
, "%spure: %d = %d explicit + %d elim + %d blkd\n",
856 stats
.pure
.expl
, stats
.pure
.elim
, stats
.pure
.blkd
);
857 assert (stats
.vars
.zombies
==
858 stats
.zombies
.elim
+ stats
.zombies
.blkd
+ stats
.zombies
.expl
);
859 fprintf (out
, "%szmbs: %d = %d explicit + %d elim + %d blkd\n",
862 stats
.zombies
.expl
, stats
.zombies
.elim
, stats
.zombies
.blkd
);
864 "%sstrs: %d forward, %d backward, %d dynamic, %d org, %d asym\n",
866 stats
.str
.fw
, stats
.str
.bw
, stats
.str
.dyn
,
867 stats
.str
.org
, stats
.str
.asym
);
868 fprintf (out
, "%sotfs: dynamic %d = %d bin + %d trn + %d large\n",
870 stats
.otfs
.dyn
.bin
+ stats
.otfs
.dyn
.trn
+ stats
.otfs
.dyn
.large
,
871 stats
.otfs
.dyn
.bin
, stats
.otfs
.dyn
.trn
, stats
.otfs
.dyn
.large
);
872 fprintf (out
, "%sotfs: static %d = %d bin + %d trn + %d large\n",
874 stats
.otfs
.stat
.bin
+ stats
.otfs
.stat
.trn
+ stats
.otfs
.stat
.large
,
875 stats
.otfs
.stat
.bin
, stats
.otfs
.stat
.trn
, stats
.otfs
.stat
.large
);
877 "%sglue: %.2f avg, %lld slimmed = %.2f per conflict\n",
879 average (stats
.glue
.sum
, stats
.glue
.count
),
881 average (stats
.glue
.slimmed
, stats
.conflicts
));
882 assert (stats
.doms
.count
>= stats
.doms
.level1
);
883 assert (stats
.doms
.level1
>= stats
.doms
.probing
);
884 fprintf (out
, "%sdoms: %d dominators, %d high, %d low\n", prfx
,
886 stats
.doms
.count
- stats
.doms
.level1
,
887 stats
.doms
.level1
- stats
.doms
.probing
);
888 long long props
= stats
.props
.srch
+ stats
.props
.simp
;
889 fprintf (out
, "%svsts: %lld visits, %.2f per prop, %.0f%% blkd",
891 stats
.visits
, average (stats
.visits
, props
),
892 percent (stats
.blocked
, stats
.visits
));
894 fprintf (out
, ", %.0f%% trn",
895 percent (stats
.ternaryvisits
, stats
.visits
));
898 double othrtime
= overalltime
- stats
.simptime
- stats
.srchtime
;
899 fprintf (out
, "%stime: "
901 "%.1f srch (%.0f%%) + "
902 "%.1f simp (%.0f%%) + "
903 "%.1f othr (%.0f%%)\n",
906 stats
.srchtime
, percent (stats
.srchtime
, overalltime
),
907 stats
.simptime
, percent (stats
.simptime
, overalltime
),
908 othrtime
, percent (othrtime
, overalltime
));
909 fprintf (out
, "%sprps: %lld srch props, %.2f megaprops per second\n",
910 prfx
, stats
.props
.srch
,
911 (stats
.srchtime
>0) ? stats
.props
.srch
/1e6
/stats
.srchtime
: 0);
912 fprintf (out
, "%sclss: %d recycled\n", prfx
,
914 fprintf (out
, "%s\n", prfx
);
915 fprintf (out
, "%s%.1f seconds, %.0f MB max, %.0f MB recycled\n", prfx
,
916 overalltime
, mb (mem
.getMax ()), mb (stats
.collected
));
920 inline void Solver::assign (int lit
) {
921 assert (!vals
[lit
]);
922 vals
[lit
] = 1; vals
[lit
^1] = -1;
923 Var
& v
= vars
[lit
/2];
924 assert ((v
.type
== ELIM
) == extending
);
925 if (!(v
.dlevel
= level
)) {
926 if (v
.type
== EQUIV
) {
928 assert (stats
.vars
.equiv
);
934 if (v
.type
== FREE
) {
937 } else assert (v
.type
== ZOMBIE
|| v
.type
== PURE
);
942 Val val
= lit2val (lit
);
943 agility
-= agility
/10000;
944 if (v
.phase
&& v
.phase
!= val
) agility
+= 1000;
948 trail
.push (mem
, lit
);
950 printf ("%sLOG assign %d at level %d <=", prfx
, lit
, level
);
951 if (v
.binary
) printf (" %d %d\n", lit
, v
.reason
.lit
);
952 else if (v
.reason
.cls
)
953 printf (" %d %d %d%s\n",
954 v
.reason
.cls
->lits
[0],
955 v
.reason
.cls
->lits
[1],
956 v
.reason
.cls
->lits
[2],
957 v
.reason
.cls
->size
> 3 ? " ..." : "");
958 else if (!level
) printf (" top level\n");
959 else printf (" decision\n");
963 inline void Solver::assume (int lit
, bool inclevel
) {
965 frames
.push (mem
, Frame (trail
));
967 LOG ("assume new level " << level
);
968 assert (level
+ 1 == frames
);
969 LOG ("assuming " << lit
);
972 LOG ("permanently assume " << lit
<< " on top level");
974 Var
& v
= vars
[lit
/2]; v
.binary
= false; v
.reason
.cls
= 0;
979 inline void Solver::imply (int lit
, int reason
) {
980 assert (lit
/2 != reason
/2);
981 assert (vals
[reason
] < 0);
982 assert (vars
[reason
/2].dlevel
== level
);
983 Var
& v
= vars
[lit
/2];
984 if (level
) v
.binary
= true, v
.reason
.lit
= reason
;
985 else v
.binary
= false, v
.reason
.lit
= 0;
986 if (level
) v
.dominator
= vars
[reason
/2].dominator
;
990 inline int Solver::dominator (int lit
, Cls
* reason
, bool & contained
) {
991 if (!opts
.dominate
) return 0;
992 if (asymode
) return 0;
993 if (opts
.maxdoms
<= stats
.doms
.count
) return 0;
996 int vdom
= 0, other
, oldvdom
;
998 for (const int * p
= reason
->lits
; vdom
>= 0 && (other
= *p
); p
++) {
999 if (other
== lit
) continue;
1000 u
= vars
+ (other
/2);
1001 if (!u
->dlevel
) continue;
1002 if (u
->dlevel
< level
) { vdom
= -1; break; }
1003 int udom
= u
->dominator
;
1007 if (udom
!= vdom
) vdom
= -1;
1011 if (vdom
<= 0) return vdom
;
1012 assert (vals
[vdom
] > 0);
1013 LOG (vdom
<< " dominates " << lit
);
1014 for (const int * p
= reason
->lits
; !contained
&& (other
= *p
); p
++)
1015 contained
= (other
^1) == vdom
;
1016 if (contained
) goto DONE
;
1017 oldvdom
= vdom
; vdom
= 0;
1018 for (const int * p
= reason
->lits
; (other
= *p
); p
++) {
1019 if (other
== lit
) continue;
1020 assert (vals
[other
] < 0);
1022 if (!u
->dlevel
) continue;
1023 assert (u
->dlevel
== level
);
1024 assert (u
->dominator
== oldvdom
);
1026 assert (other
!= oldvdom
);
1027 if (other
== vdom
) continue;
1030 (other
= (assert (u
->binary
), 1^u
->reason
.lit
)) != oldvdom
&&
1032 assert (vals
[other
] > 0);
1034 assert (u
->dlevel
== level
);
1035 assert (u
->dominator
== oldvdom
);
1037 while (vdom
!= other
) {
1038 u
= vars
+ (vdom
/2);
1042 vdom
= 1^u
->reason
.lit
;
1044 if (vdom
== oldvdom
) break;
1046 vdom
= 1^u
->reason
.lit
;
1047 if (vdom
== oldvdom
) break;
1048 assert (vals
[vdom
] > 0);
1052 assert (u
->dlevel
== level
);
1053 assert (u
->dominator
== oldvdom
);
1057 other
= 1^u
->reason
.lit
;
1058 assert (vals
[other
] > 0);
1059 } while (other
!= oldvdom
);
1063 while (other
!= oldvdom
) {
1065 assert (u
->dlevel
== level
);
1066 assert (u
->dominator
== oldvdom
);
1070 other
= 1^u
->reason
.lit
;
1071 assert (vals
[other
] > 0);
1074 if (vdom
== oldvdom
) goto DONE
;
1077 LOG (vdom
<< " also dominates " << lit
);
1078 assert (!contained
);
1079 for (const int * p
= reason
->lits
; !contained
&& (other
= *p
); p
++)
1080 contained
= (other
^1) == vdom
;
1084 if (level
== 1) stats
.doms
.level1
++;
1085 if (!measure
) { assert (level
== 1); stats
.doms
.probing
++; }
1087 reason
->garbage
= true;
1089 LOG ("dominator clause is subsuming");
1095 inline void Solver::unit (int lit
) {
1097 Val val
= vals
[lit
];
1100 LOG ("conflict after adding unit"); conflict
= &empty
; return;
1104 v
->binary
= false, v
->reason
.cls
= 0;
1107 int other
= find (lit
);
1108 if (other
== lit
) return;
1111 LOG ("conflict after adding unit"); conflict
= &empty
; return;
1114 v
= vars
+ (other
/2);
1115 v
->binary
= false, v
->reason
.cls
= 0;
1119 inline unsigned Solver::gluelits () {
1120 const int * eol
= lits
.end ();
1124 for (const int * p
= lits
.begin (); p
< eol
; p
++) {
1126 assert (val (lit
) < 0);
1127 Var
* v
= vars
+ (lit
/2);
1128 int dlevel
= v
->dlevel
;
1129 if (dlevel
== level
) { assert (!found
); found
= lit
; continue; }
1130 assert (dlevel
> 0);
1131 Frame
* f
= &frames
[dlevel
];
1132 if (f
->contained
) continue;
1133 f
->contained
= true;
1136 assert (found
== uip
);
1137 for (const int * p
= lits
.begin (); p
< eol
; p
++)
1138 frames
[vars
[*p
/2].dlevel
].contained
= false;
1142 inline void Solver::slim (Cls
* cls
) {
1143 if (!opts
.slim
) return;
1146 if (!cls
->lnd
) return;
1147 assert (!cls
->binary
);
1148 unsigned oldglue
= cls
->glue
;
1149 if (!oldglue
) return;
1150 const int * p
= cls
->lits
;
1151 unsigned newglue
= 0;
1152 int lit
, nonfalse
= 0;
1153 while ((lit
= *p
++)) {
1154 Val val
= vals
[lit
];
1155 if (val
>= 0 && nonfalse
++) { newglue
= oldglue
; break; }
1156 Var
* v
= vars
+ (lit
/2);
1157 int dlevel
= v
->dlevel
;
1158 if (dlevel
<= 0) continue;
1159 assert (dlevel
< frames
);
1160 Frame
* f
= &frames
[dlevel
];
1161 if (f
->contained
) continue;
1162 if (++newglue
>= oldglue
) break;
1163 f
->contained
= true;
1165 while (p
> cls
->lits
) {
1168 Var
* v
= vars
+ (lit
/2);
1169 int dlevel
= v
->dlevel
;
1170 if (dlevel
<= 0) continue;
1171 assert (dlevel
< frames
);
1172 Frame
* f
= &frames
[dlevel
];
1173 f
->contained
= false;
1176 assert (oldglue
>= newglue
);
1177 if (oldglue
== newglue
) return;
1178 assert (newglue
>= 1);
1179 LOG ("slimmed glue from " << oldglue
<< " to " << newglue
);
1180 } else LOG ("new glue " << newglue
);
1181 assert (newglue
<= (unsigned) opts
.glue
);
1182 if (!cls
->fresh
) dequeue (anchor (cls
), cls
);
1183 cls
->glue
= newglue
;
1184 if (!cls
->fresh
) push (anchor (cls
), cls
);
1185 if (cls
->glued
) stats
.glue
.slimmed
++;
1187 stats
.glue
.sum
+= newglue
;
1191 inline void Solver::force (int lit
, Cls
* reason
) {
1193 assert (!reason
->binary
);
1194 Val val
= vals
[lit
];
1195 if (val
< 0) { LOG ("conflict forcing literal"); conflict
= reason
; }
1198 for (const int * p
= reason
->lits
; *p
; p
++)
1199 if (*p
!= lit
) assert (vals
[*p
] < 0);
1201 Var
* v
= vars
+ (lit
/2);
1205 v
->binary
= false, v
->reason
.cls
= 0;
1206 } else if (!lits
&& (vdom
= dominator (lit
, reason
, sub
)) > 0) {
1207 v
->dominator
= vdom
;
1208 assert (vals
[vdom
] > 0);
1210 LOG ("dominating learned clause " << vdom
<< ' ' << lit
);
1212 lits
.push (mem
, vdom
);
1213 lits
.push (mem
, lit
);
1214 bool lnd
= reason
->lnd
|| !sub
;
1216 v
->binary
= true, v
->reason
.lit
= vdom
;
1218 v
->binary
= false, v
->reason
.cls
= reason
;
1219 reason
->locked
= true;
1220 if (reason
->lnd
) stats
.clauses
.lckd
++;
1226 inline void Solver::jwh (Cls
* cls
) {
1227 //if (cls->lnd) return; // TODO better not ?
1229 for (p
= cls
->lits
; *p
; p
++)
1231 int size
= p
- cls
->lits
;
1232 int inc
= logsize (size
);
1233 while (p
> cls
->lits
) {
1236 if (jwhs
[l
] < 0) die ("maximum large JWH score exceeded");
1240 int Solver::find (int a
) {
1241 assert (2 <= a
&& a
<= 2 * maxvar
+ 1);
1243 for (res
= a
; (tmp
= repr
[res
]); res
= tmp
)
1245 for (int fix
= a
; (tmp
= repr
[fix
]) && tmp
!= res
; fix
= tmp
)
1246 repr
[fix
] = res
, repr
[fix
^1] = res
^1;
1250 inline void Solver::merge (int l
, int k
, int & merged
) {
1252 if (!opts
.merge
) return;
1255 if ((a
= find (l
)) == (b
= find (k
))) return;
1256 assert (a
/2 != b
/2);
1259 LOG ("merge " << l
<< " and " << k
<< " to " << m
);
1260 if (k
!= m
) LOG ("learned clause " << k
<< ' ' << (m
^1));
1261 if (k
!= m
) LOG ("learned clause " << (k
^1) << ' ' << m
);
1262 if (l
!= m
) LOG ("learned clause " << l
<< ' ' << (m
^1));
1263 if (l
!= m
) LOG ("learned clause " << (l
^1) << ' ' << m
);
1265 if (a
< b
) repr
[k
] = repr
[b
] = a
, repr
[k
^1] = repr
[b
^1] = a
^1;
1266 else repr
[l
] = repr
[a
] = b
, repr
[l
^1] = repr
[a
^1] = b
^1;
1267 assert (vars
[a
/2].type
== FREE
&& vars
[b
/2].type
== FREE
);
1268 vars
[max (a
,b
)/2].type
= EQUIV
;
1269 stats
.vars
.merged
++;
1275 Cls
* Solver::clause (bool lnd
, unsigned glue
) {
1276 assert (asymode
|| !elimode
|| !lnd
);
1277 assert (lnd
|| !glue
);
1280 std::cout
<< prfx
<< "LOG " << (lnd
? "learned" : "original") << " clause";
1281 for (const int * p
= lits
.begin (); p
< lits
.end (); p
++)
1282 std::cout
<< ' ' << *p
;
1283 std::cout
<< std::endl
;
1286 for (int i
= 0; i
< lits
; i
++)
1287 assert (vars
[lits
[i
]/2].type
!= ELIM
);
1290 LOG ("conflict after added empty clause");
1292 } else if (lits
== 1) {
1295 if ((val
= vals
[lit
]) < 0) {
1296 LOG ("conflict after adding falsified unit clause");
1298 } else if (!val
) unit (lit
);
1300 if (lits
>= (int)Cls::MAXSZ
) die ("maximal clause size exceeded");
1301 size_t bytes
= Cls::bytes (lits
);
1302 res
= (Cls
*) mem
.callocate (bytes
);
1304 if (!lnd
) stats
.clauses
.irr
++;
1306 int * q
= res
->lits
, * eol
= lits
.end ();
1307 for (const int * p
= lits
.begin (); p
< eol
; p
++)
1310 if (lits
== 2) res
->binary
= true, stats
.clauses
.bin
++;
1312 res
->glue
= min ((unsigned)opts
.glue
,glue
);
1313 res
->fresh
= res
->lnd
;
1314 if (lnd
) stats
.clauses
.lnd
++;
1315 else stats
.clauses
.orig
++;
1324 inline void Solver::marklits () {
1325 for (const int * p
= lits
.begin (); p
< lits
.end (); p
++)
1326 vars
[*p
/2].mark
= lit2val (*p
);
1329 inline void Solver::unmarklits () {
1330 for (const int * p
= lits
.begin (); p
< lits
.end (); p
++)
1331 vars
[*p
/2].mark
= 0;
1334 inline bool Solver::bwsub (unsigned sig
, Cls
* c
) {
1335 assert (!c
->trash
&& !c
->dirty
&& !c
->garbage
);
1336 limit
.budget
.bw
.sub
--;
1338 if (c
->size
< (unsigned) count
) return false;
1339 INC (sigs
.bw
.l1
.srch
);
1340 if (!sigsubs (sig
, c
->sig
)) { INC (sigs
.bw
.l1
.hits
); return false; }
1342 for (int * p
= c
->lits
; count
&& (lit
= *p
); p
++) {
1343 Val u
= lit2val (lit
), v
= vars
[lit
/2].mark
;
1344 if (u
== v
) count
--;
1349 int Solver::bwstr (unsigned sig
, Cls
* c
) {
1350 assert (!c
->trash
&& !c
->dirty
&& !c
->garbage
);
1351 limit
.budget
.bw
.str
--;
1353 if (c
->size
< (unsigned) count
) return 0;
1354 INC (sigs
.bw
.l1
.srch
);
1355 if (!sigsubs (sig
, c
->sig
)) { INC (sigs
.bw
.l1
.hits
); return 0; }
1357 for (int * p
= c
->lits
; count
&& (lit
= *p
); p
++) {
1358 Val u
= lit2val (lit
), v
= vars
[lit
/2].mark
;
1359 if (abs (u
) != abs (v
)) continue;
1360 if (u
== -v
) { if (res
) return 0; res
= lit
; }
1363 assert (count
>= 0);
1364 res
= count
? 0 : res
;
1369 void Solver::remove (int del
, Cls
* c
) {
1370 assert (!c
->trash
&& !c
->garbage
&& !c
->dirty
&& !c
->gate
);
1371 assert (c
->lits
[0] && c
->lits
[1]);
1373 int pos
= (c
->lits
[1] == del
);
1374 assert (c
->lits
[pos
] == del
);
1375 LOG ("will not remove " << del
<< " but will simply produce unit instead");
1376 unit (c
->lits
[!pos
]);
1379 int * p
= c
->lits
, lit
;
1380 while ((lit
= *p
) != del
) assert (lit
), p
++;
1381 while ((lit
= *++p
)) p
[-1] = lit
;
1383 assert (p
- c
->lits
>= 3);
1384 if (p
- c
->lits
== 3) {
1386 assert (stats
.clauses
.lnd
> 0);
1387 stats
.clauses
.lnd
--;
1389 assert (stats
.clauses
.orig
> 0);
1390 stats
.clauses
.orig
--;
1393 stats
.clauses
.bin
++;
1397 if (elimode
|| blkmode
) touch (del
);
1400 LOG ("removed " << del
<< " and got");
1401 dbgprint ("LOG learned clause ", c
);
1406 void Solver::bworgs () {
1407 if (lits
<= 1) return;
1408 limit
.budget
.bw
.str
+= 2;
1409 limit
.budget
.bw
.sub
+= 4;
1412 int minlen
= INT_MAX
;
1413 for (int i
= 0; i
< lits
; i
++) {
1414 int other
= lits
[i
];
1415 int len
= orgs
[other
];
1416 if (len
< minlen
) first
= other
, minlen
= len
;
1418 unsigned sig
= litsig ();
1420 INC (sigs
.bw
.l2
.srch
);
1421 if (!sigsubs (sig
, bwsigs
[first
])) INC (sigs
.bw
.l2
.hits
);
1422 else if (orgs
[first
] <= opts
.bwmaxlen
)
1423 for (int i
= 0; limit
.budget
.bw
.sub
>= 0 && i
< orgs
[first
]; i
++) {
1424 Cls
* other
= orgs
[first
][i
];
1425 assert (!other
->locked
);
1426 if (other
->trash
|| other
->dirty
|| other
->garbage
) continue;
1427 if (!bwsub (sig
, other
)) continue;
1429 dbgprint ("LOG static backward subsumed clause ", other
);
1432 limit
.budget
.bw
.sub
+= 12;
1437 for (int i
= 0; i
< lits
; i
++) {
1438 int other
= lits
[i
];
1439 if (other
== first
) continue;
1440 int len
= orgs
[other
];
1441 if (len
< minlen
) second
= other
, minlen
= len
;
1444 if (orgs
[first
^1] < minlen
) second
= (first
^1);
1445 for (int round
= 0; round
<= 1; round
++) {
1446 int start
= round
? second
: first
;
1447 INC (sigs
.bw
.l2
.srch
);
1448 if (!sigsubs (sig
, bwsigs
[start
])) { INC (sigs
.bw
.l2
.hits
); continue; }
1449 Orgs
& org
= orgs
[start
];
1450 if (org
> opts
.bwmaxlen
) continue;
1451 for (int i
= 0; limit
.budget
.bw
.str
>= 0 && i
< org
; i
++) {
1452 Cls
* other
= org
[i
];
1453 assert (!other
->locked
);
1454 if (other
->trash
|| other
->dirty
|| other
->garbage
) continue;
1455 int del
= bwstr (sig
, other
);
1457 LOG ("static backward strengthened clause by removing " << del
);
1459 limit
.budget
.bw
.str
+= 10;
1460 remove (del
, other
);
1461 assert (litsig () == sig
);
1467 void Solver::bwoccs (bool & lnd
) {
1468 if (lits
<= 1) return;
1469 limit
.budget
.bw
.sub
+= lnd
? 30 : 10;
1470 limit
.budget
.bw
.str
+= lnd
? 20 : 8;
1472 unsigned sig
= litsig ();
1473 for (int i
= 0; i
< lits
; i
++) {
1474 int first
= lits
[i
];
1475 if (limit
.budget
.bw
.sub
>= 0) {
1476 INC (sigs
.bw
.l2
.srch
);
1477 if (!sigsubs (sig
, bwsigs
[first
])) INC (sigs
.bw
.l2
.hits
);
1478 else if (occs
[first
].large
<= opts
.bwmaxlen
) {
1480 limit
.budget
.bw
.sub
>= 0 && i
< occs
[first
].large
; i
++) {
1481 Cls
* other
= occs
[first
].large
[i
].cls
;
1482 assert (!other
->dirty
&& !other
->trash
);
1483 if (other
->garbage
) continue;
1484 if (!bwsub (sig
, other
)) continue;
1485 if (!other
->lnd
&& lnd
) lnd
= false;
1486 LOG ((level
? "dynamic" : "static")
1487 << " backward subsumed "
1488 << (other
->lnd
? "learned" : "original")
1492 std::cout
<< prfx
<< "LOG subsumed clause";
1493 for (const int * p
= other
->lits
; *p
; p
++)
1494 std::cout
<< ' ' << *p
;
1495 std::cout
<< std::endl
;
1500 if (!other
->lnd
) stats
.subs
.org
++;
1501 } else stats
.subs
.bw
++;
1502 limit
.budget
.bw
.sub
+= 20;
1503 if (other
->locked
) other
->garbage
= true; else recycle (other
);
1507 if (limit
.budget
.bw
.str
>= 0) {
1508 INC (sigs
.bw
.l2
.srch
);
1509 if (!sigsubs (sig
, bwsigs
[first
])) INC (sigs
.bw
.l2
.hits
);
1510 else if (occs
[first
].large
<= opts
.bwmaxlen
) {
1512 limit
.budget
.bw
.sub
>= 0 && i
< occs
[first
].large
;
1514 Cls
* other
= occs
[first
].large
[i
].cls
;
1515 assert (!other
->dirty
&& !other
->trash
);
1516 if (other
->locked
|| other
->garbage
) continue;
1517 int del
= bwstr (sig
, other
);
1519 LOG ((level
? "dynamic" : "static")
1520 << " backward strengthened "
1521 << (other
->lnd
? "learned" : "original")
1522 << " clause by removing "
1526 std::cout
<< prfx
<< "LOG strengthened clause";
1527 for (const int * p
= other
->lits
; *p
; p
++)
1528 std::cout
<< ' ' << *p
;
1529 std::cout
<< std::endl
;
1534 if (!other
->lnd
) stats
.str
.org
++;
1535 } else stats
.str
.bw
++;
1536 limit
.budget
.bw
.str
+= 15;
1537 remove (del
, other
);
1538 if (level
) strcls (other
);
1546 inline bool Solver::fwsub (unsigned sig
, Cls
* c
) {
1547 assert (!c
->trash
&& !c
->dirty
&& !c
->garbage
);
1548 limit
.budget
.fw
.sub
--;
1549 INC (sigs
.fw
.l1
.srch
);
1550 if (!sigsubs (c
->sig
, sig
)) { INC (sigs
.fw
.l1
.hits
); return false; }
1552 for (const int * p
= c
->lits
; (lit
= *p
); p
++) {
1553 Val u
= lit2val (lit
), v
= vars
[lit
/2].mark
;
1554 if (u
!= v
) return false;
1559 inline int Solver::fwstr (unsigned sig
, Cls
* c
) {
1560 assert (!c
->trash
&& !c
->dirty
&& !c
->garbage
);
1561 limit
.budget
.fw
.str
--;
1562 INC (sigs
.fw
.l1
.srch
);
1563 if (!sigsubs (c
->sig
, sig
)) { INC (sigs
.fw
.l1
.hits
); return 0; }
1565 for (const int * p
= c
->lits
; (lit
= *p
); p
++) {
1566 Val u
= lit2val (lit
), v
= vars
[lit
/2].mark
;
1567 if (u
== v
) continue;
1568 if (u
!= -v
) return 0;
1575 bool Solver::fworgs () {
1576 if (lits
<= 1) return false;
1577 limit
.budget
.fw
.str
+= 3;
1578 limit
.budget
.fw
.sub
+= 5;
1581 unsigned sig
= litsig ();
1584 for (int i
= 0; !res
&& limit
.budget
.fw
.sub
>= 0 && i
< lits
; i
++) {
1586 INC (sigs
.fw
.l2
.srch
);
1587 if (!(fwsigs
[lit
] & sig
)) { INC (sigs
.fw
.l2
.hits
); continue; }
1588 Fwds
& f
= fwds
[lit
];
1589 if (f
> opts
.fwmaxlen
) continue;
1590 for (int j
= 0; !res
&& limit
.budget
.fw
.sub
>= 0 && j
< f
; j
++) {
1592 if (c
->trash
|| c
->dirty
|| c
->garbage
) continue;
1593 res
= fwsub (sig
, c
);
1597 LOG ("new clause is subsumed");
1599 limit
.budget
.fw
.sub
+= 5;
1603 for (int sign
= 0; sign
<= 1; sign
++)
1604 for (int i
= 0; limit
.budget
.fw
.str
>= 0 && i
< lits
; i
++) {
1606 INC (sigs
.fw
.l2
.srch
);
1607 if (!(fwsigs
[lit
] & sig
)) { INC (sigs
.fw
.l2
.hits
); continue; }
1609 Fwds
& f
= fwds
[lit
];
1610 if (f
> opts
.fwmaxlen
) continue;
1612 for (int j
= 0; !del
&& limit
.budget
.fw
.str
>= 0 && j
< f
; j
++) {
1614 if (c
->trash
|| c
->dirty
|| c
->garbage
) continue;
1615 del
= fwstr (sig
, c
);
1618 assert (sign
|| del
/2 != lit
/2);
1619 LOG ("strengthen new clause by removing " << del
);
1621 limit
.budget
.fw
.str
+= 8;
1622 assert (vars
[del
/2].mark
== lit2val (del
));
1623 vars
[del
/2].mark
= 0;
1632 void Solver::resize (int newmaxvar
) {
1633 assert (maxvar
< size
);
1634 assert (newmaxvar
> maxvar
);
1636 while (newsize
<= newmaxvar
)
1638 if (newsize
> size
) {
1641 o
= size
* sizeof * vars
;
1642 n
= newsize
* sizeof * vars
;
1643 vars
= (Var
*) mem
.recallocate (vars
, o
, n
);
1645 o
= 2 * size
* sizeof *repr
;
1646 n
= 2 * newsize
* sizeof *repr
;
1647 repr
= (int*) mem
.recallocate (repr
, o
, n
);
1649 o
= 2 * size
* sizeof *jwhs
;
1650 n
= 2 * newsize
* sizeof *jwhs
;
1651 jwhs
= (int*) mem
.recallocate (jwhs
, o
, n
);
1653 o
= 2 * size
* sizeof *vals
;
1654 n
= 2 * newsize
* sizeof *vals
;
1655 vals
= (Val
*) mem
.recallocate (vals
, o
, n
);
1657 o
= 2 * size
* sizeof *occs
;
1658 n
= 2 * newsize
* sizeof *occs
;
1659 occs
= (Occs
*) mem
.recallocate (occs
, o
, n
);
1664 o
= size
* sizeof *rnks
;
1665 n
= newsize
* sizeof *rnks
;
1667 rnks
= (Rnk
*) mem
.reallocate (rnks
, o
, n
);
1668 diff
= c
- (char *) rnks
;
1669 schedule
.decide
.fix (diff
);
1671 o
= size
* sizeof *prbs
;
1672 n
= newsize
* sizeof *prbs
;
1674 prbs
= (Rnk
*) mem
.reallocate (prbs
, o
, n
);
1675 diff
= c
- (char *) prbs
;
1676 schedule
.probe
.fix (diff
);
1678 o
= size
* sizeof *elms
;
1679 n
= newsize
* sizeof *elms
;
1681 elms
= (Rnk
*) mem
.reallocate (elms
, o
, n
);
1682 diff
= c
- (char *) elms
;
1683 schedule
.elim
.fix (diff
);
1685 o
= 2 * size
* sizeof *elms
;
1686 n
= 2 * newsize
* sizeof *elms
;
1688 blks
= (Rnk
*) mem
.reallocate (blks
, o
, n
);
1689 diff
= c
- (char *) blks
;
1690 schedule
.block
.fix (diff
);
1692 rszbwsigs (newsize
);
1696 assert (newmaxvar
< size
);
1697 while (maxvar
< newmaxvar
) {
1698 Var
* v
= vars
+ ++maxvar
;
1701 for (int i
= 1; i
< opts
.order
; i
++)
1704 Rnk
* r
= rnks
+ maxvar
;
1705 r
->heat
= 0, r
->pos
= -1, schedule
.decide
.push (mem
, r
);
1707 Rnk
* p
= prbs
+ maxvar
;
1708 p
->heat
= 0, p
->pos
= -1;
1710 Rnk
* e
= elms
+ maxvar
;
1711 e
->heat
= 0, e
->pos
= -1;
1713 Rnk
* b
= blks
+ 2*maxvar
;
1714 b
[0].heat
= b
[1].heat
= 0;
1715 b
[0].pos
= b
[1].pos
= -1;
1717 assert (maxvar
< size
);
1720 void Solver::import () {
1721 bool trivial
= false;
1722 int * q
= lits
.begin ();
1723 const int * p
, * eol
= lits
.end ();
1724 for (p
= lits
.begin (); !trivial
&& p
< eol
; p
++) {
1725 int lit
= *p
, v
= lit
/2;
1727 if (v
> maxvar
) resize (v
);
1728 Val tmp
= vals
[lit
];
1730 int prev
= vars
[v
].mark
;
1731 int val
= lit2val (lit
);
1733 if (val
== prev
) continue;
1734 assert (val
== -prev
);
1744 while (p
> lits
.begin ()) vars
[*--p
/2].mark
= 0;
1756 inline bool Solver::satisfied (const Cls
* c
) {
1758 for (const int * p
= c
->lits
; (lit
= *p
); p
++)
1759 if (val (lit
) > 0) return true;
1763 inline bool Solver::satisfied (Anchor
<Cls
> & anchor
) {
1764 for (const Cls
* p
= anchor
.head
; p
; p
= p
->prev
)
1765 if (!satisfied (p
)) return false;
1769 bool Solver::satisfied () {
1770 if (!satisfied (binary
)) return false;
1771 if (!satisfied (original
)) return false;
1773 for (int glue
= 0; glue
<= opts
.glue
; glue
++)
1774 if (!satisfied (learned
[glue
])) return false;
1775 if (!satisfied (fresh
)) return false;
1778 for (const int * p
= check
.begin (); p
< check
.end (); p
++) {
1781 while ((lit
= *p
)) {
1782 if (val (lit
) > 0) found
= true;
1785 if (!found
) return false;
1791 inline void Solver::prop2 (int lit
) {
1792 assert (vals
[lit
] < 0);
1793 LOG ("prop2 " << lit
);
1794 const Stack
<int> & os
= occs
[lit
].bins
;
1795 const int * eos
= os
.end ();
1796 for (const int * p
= os
.begin (); p
< eos
; p
++) {
1798 Val val
= vals
[other
];
1799 if (val
> 0) continue;
1800 if (!val
) { imply (other
, lit
); continue; }
1801 LOG ("conflict in binary clause while propagating " << (1^lit
));
1802 conflict
= lit2conflict (dummy
, lit
, other
);
1803 LOG ("conflicting clause " << lit
<< ' ' << other
);
1807 inline void Solver::propl (int lit
) {
1808 assert (vals
[lit
] < 0);
1809 LOG ("propl " << lit
);
1810 Stack
<Occ
> & os
= occs
[lit
].large
;
1811 Occ
* a
= os
.begin (), * t
= os
.end (), * p
= a
, * q
= a
;
1812 CONTINUE_OUTER_LOOP
:
1815 Cls
* cls
= p
++->cls
;
1816 *q
++ = Occ (blit
, cls
);
1818 Val val
= vals
[blit
];
1819 if (val
> 0) { stats
.blocked
++; continue; }
1821 if (cls
->lits
[2] && !*(cls
->lits
+ 3)) INC (ternaryvisits
);
1823 int sum
= cls
->lits
[0]^cls
->lits
[1];
1824 int other
= sum
^lit
;
1827 if (val
> 0) continue;
1828 int prev
= lit
, next
, *l
, *lits2
= cls
->lits
+2;
1829 for (l
= lits2
; (next
= *l
); l
++) {
1830 *l
= prev
; prev
= next
;
1831 if (vals
[next
] < 0) continue;
1832 occs
[next
].large
.push (mem
, Occ (other
, cls
));
1833 int pos
= (cls
->lits
[1] == lit
);
1834 cls
->lits
[pos
] = next
;
1835 q
--; goto CONTINUE_OUTER_LOOP
;
1837 while (l
> lits2
) { next
= *--l
; *l
= prev
; prev
= next
; }
1840 LOG ("conflict in large clause while propagating " << (1^lit
));
1843 dbgprint ("LOG conflicting clause ", cls
);
1848 long moved
= ((char*)os
.begin ()) - (char*)a
;
1849 if (moved
) fix (p
,moved
), fix (q
,moved
), fix (t
,moved
), a
= os
.begin ();
1851 while (p
< t
) *q
++ = *p
++;
1855 bool Solver::bcp () {
1856 if (conflict
) return false;
1857 if (!level
&& units
) flushunits ();
1858 if (conflict
) return false;
1861 if (queue2
< trail
) {
1863 lit
= 1^trail
[queue2
++];
1865 if (!measure
&& conflict
) break;
1866 } else if (queue
< trail
) {
1867 if (conflict
) break;
1868 lit
= 1^trail
[queue
++];
1870 if (conflict
) break;
1874 if (measure
) stats
.props
.srch
+= props
;
1875 else stats
.props
.simp
+= props
;
1879 inline bool Solver::needtoflush () const {
1880 return queue2
< trail
;
1883 bool Solver::flush () {
1886 if (!bcp ()) return false;
1887 while (fixed
< trail
) {
1888 int lit
= trail
[fixed
++];
1895 inline int Solver::phase (Var
* v
) {
1896 int lit
= 2 * (v
- vars
) + 1;
1898 (!v
->phase
&& (jwhs
[lit
^1] > jwhs
[lit
]))) lit
^= 1;
1902 void Solver::extend () {
1907 int unblock
= elits
[--n
];
1908 int lit
= elits
[--n
];
1910 LOG ("unblocking " << lit
);
1911 Val valit
= val (lit
);
1913 bool forced
= (valit
< 0);
1915 while ((other
= elits
[--n
])) {
1916 if (!forced
) continue;
1917 other
= find (other
);
1918 Val v
= val (other
);
1922 if (!forced
) continue;
1923 // TODO make this in an assertion ...
1924 // We have 'in principle' a proof that this can not happen.
1925 if (repr
[lit
]) die ("internal error extending assignment");
1926 LOG ("assign " << (1^lit
) << " at level " << level
<< " <= unblock");
1927 vals
[lit
] = 1, vals
[lit
^1] = -1;
1928 assert (trail
[vars
[lit
/2].tlevel
] == (1^lit
));
1929 trail
[vars
[lit
/2].tlevel
] = lit
;
1930 stats
.extend
.flipped
++;
1932 LOG ("extending " << lit
);
1933 assert (!repr
[lit
]);
1934 while (elits
[n
-1]) {
1937 while ((other
= elits
[--n
])) {
1938 if (!forced
) continue;
1939 other
= find (other
);
1940 if (other
== lit
) continue;
1941 if (other
== (lit
^1)) { forced
= false; continue; }
1942 Val v
= val (other
);
1943 if (v
> 0) forced
= false;
1945 if (!forced
) continue;
1947 if (v
) assert (v
> 0);
1948 else { assume (lit
); stats
.extend
.forced
++; }
1950 if (!val (lit
)) { assume (lit
^1); stats
.extend
.assumed
++; }
1955 for (int lit
= 2; lit
<= 2 * maxvar
+ 1; lit
+= 2)
1961 bool Solver::decide () {
1964 if (!schedule
.decide
) { extend (); return false; }
1965 r
= schedule
.decide
.max ();
1968 if (vars
[idx
].type
== FREE
&& !vals
[lit
]) break;
1969 (void) schedule
.decide
.pop ();
1973 stats
.sumheight
+= level
;
1974 if (opts
.random
&& agility
<= 10 * 100000 && rng
.oneoutof (opts
.spread
)) {
1976 unsigned n
= schedule
.decide
; assert (n
);
1977 unsigned s
= rng
.next () % n
, d
= rng
.next () % n
;
1978 while (ggt (n
, d
) != 1) {
1979 d
++; if (d
>= n
) d
= 1;
1982 r
= schedule
.decide
[s
];
1983 int lit
= 2 * (r
- rnks
);
1984 if (vars
[lit
/2].type
== FREE
&& !vals
[lit
]) break;
1985 s
+= d
; if (s
>= n
) s
-= n
;
1988 int lit
= phase (var (r
));
1989 assert (!vals
[lit
]);
1990 LOG ("decision " << lit
);
1996 inline bool Solver::min2 (int lit
, int other
, int depth
) {
1997 assert (lit
!= other
&& vals
[lit
] > 0);
1998 if (vals
[other
] >= 0) return false;
1999 Var
* v
= vars
+ (lit
/2);
2000 if (v
->binary
&& v
->reason
.lit
== other
) {
2001 Var
* d
= vars
+ (v
->dominator
/2);
2004 if (d
->removable
) return true;
2005 if (d
->mark
) return true;
2007 Var
* u
= vars
+ (other
/2);
2008 assert (opts
.minimize
> Opts::RECUR
|| u
->tlevel
< v
->tlevel
);
2009 if (u
->tlevel
> v
->tlevel
) return false;
2010 if (u
->mark
) return true;
2011 if (u
->removable
) return true;
2012 if (u
->poison
) return false;
2013 return minimize (u
, depth
);
2016 inline bool Solver::minl (int lit
, Cls
* cls
, int depth
) {
2017 assert (vals
[lit
] > 0);
2018 assert (cls
->locked
|| cls
->lits
[0] == lit
|| cls
->lits
[1] == lit
);
2019 Var
* v
= vars
+ (lit
/2);
2021 for (const int * p
= cls
->lits
; (other
= *p
); p
++) {
2022 if (other
== lit
) continue;
2023 if (vals
[other
] >= 0) return false;
2024 Var
* u
= vars
+ (other
/2);
2025 assert (opts
.minimize
> Opts::RECUR
|| u
->tlevel
< v
->tlevel
);
2026 if (u
->tlevel
> v
->tlevel
) {
2027 if (!opts
.inveager
) return false;
2028 if (u
!= vars
+ uip
/2 && (u
->binary
|| u
->reason
.cls
))
2031 if (u
->mark
) continue;
2032 if (u
->removable
) continue;
2033 if (u
->poison
) return false;
2036 if (!frames
[l
].pulled
) return false;
2039 for (const int * p
= cls
->lits
; (other
= *p
); p
++) {
2040 if (other
== lit
) continue;
2041 Var
* u
= vars
+ other
/2;
2042 if (u
->mark
) continue;
2043 if (u
->removable
) continue;
2044 if (u
->poison
) return false;
2047 if (!minimize (u
, depth
)) { /*cleanpulled (old); */ return false; }
2052 inline bool Solver::strengthen (int lit
, int depth
) {
2053 assert (vals
[lit
] > 0);
2054 assert (opts
.minimize
>= Opts::STRONG
);
2055 const Stack
<int> & os2
= occs
[lit
].bins
;
2056 const int * eos2
= os2
.end ();
2057 for (const int * o
= os2
.begin (); o
< eos2
&& limit
.strength
-- >= 0; o
++)
2058 if (min2 (lit
, *o
, depth
)) return true;
2059 if (opts
.minimize
< Opts::STRONGER
) return false;
2060 const Stack
<Occ
> & osl
= occs
[lit
].large
;
2061 const Occ
* eosl
= osl
.end ();
2062 for (const Occ
* o
= osl
.begin (); o
< eosl
&& limit
.strength
-- >= 0; o
++)
2063 if (minl (lit
, o
->cls
, depth
)) {
2064 if (opts
.mtfall
&& depth
== 1 && o
->cls
->lnd
)
2065 mtf (anchor (o
->cls
), o
->cls
);
2071 bool Solver::minimize (Var
* v
, int depth
) {
2072 if (!depth
) limit
.strength
= opts
.strength
;
2073 if (depth
> stats
.mins
.depth
) stats
.mins
.depth
= depth
;
2074 assert (v
->dlevel
!= level
);
2075 if (v
->removable
) return true;
2076 if (depth
&& v
->mark
) return true;
2077 if (v
->poison
) return false;
2079 if (!l
) return true;
2080 if (opts
.minimize
== Opts::NONE
) return false;
2081 if (depth
&& opts
.minimize
== Opts::LOCAL
) return false;
2082 if (!v
->binary
&& !v
->reason
.cls
) return false;
2083 if (!frames
[l
].pulled
) return false;
2084 if (depth
++ >= opts
.maxdepth
) return false;
2085 assert (!v
->onstack
);
2088 int lit
= 2 * (v
- vars
);
2089 Val val
= vals
[lit
];
2090 if (val
< 0) lit
^= 1;
2091 assert (vals
[lit
] > 0);
2092 if (v
->binary
) res
= min2 (lit
, v
->reason
.lit
, depth
);
2093 else if ((res
= minl (lit
, v
->reason
.cls
, depth
))) {
2094 if (opts
.mtfall
&& depth
== 1 && v
->reason
.cls
->lnd
)
2095 mtf (anchor (v
->reason
.cls
), v
->reason
.cls
);
2097 if (opts
.minimize
>= Opts::STRONG
&& !res
)
2098 if ((res
= strengthen (lit
, depth
)))
2099 stats
.mins
.strong
++;
2101 if (res
) v
->removable
= true;
2102 else v
->poison
= true;
2107 bool Solver::inverse (int lit
) {
2108 assert (vals
[lit
] > 0);
2109 Var
* v
= vars
+ (lit
/2);
2110 if (v
->dlevel
!= jlevel
) return false;
2111 const Stack
<Occ
> & osl
= occs
[lit
].large
;
2112 const Occ
* eosl
= osl
.end ();
2113 bool foundlit
= false, founduip
= false;
2114 for (const Occ
* o
= osl
.begin (); o
< eosl
; o
++) {
2117 for (const int * p
= c
->lits
; (other
= *p
); p
++) {
2118 if (other
== lit
) { foundlit
= true; continue; }
2119 if (other
== uip
) { founduip
= true; continue; }
2120 if (vals
[other
] >= 0) break;
2121 Var
* u
= vars
+ (other
/2);
2122 if (u
->dlevel
>= jlevel
) break;
2123 if (!u
->mark
) break;
2125 if (other
) continue;
2129 dbgprint ("LOG inverse arc ", c
);
2131 if (opts
.mtfall
&& c
->lnd
) mtf (anchor (c
), c
);
2137 void Solver::undo (int newlevel
, bool save
) {
2138 LOG ("undo " << newlevel
);
2139 assert (newlevel
<= level
);
2140 if (newlevel
== level
) return;
2141 if (save
) saved
.shrink ();
2142 int tlevel
= frames
[newlevel
+1].tlevel
;
2143 while (tlevel
< trail
) {
2144 int lit
= trail
.pop ();
2145 assert (vals
[lit
] > 0);
2146 vals
[lit
] = vals
[lit
^1] = 0;
2147 LOG("unassign " << lit
);
2149 if (save
) saved
.push (mem
, lit
);
2150 Rnk
& r
= rnks
[lit
/2];
2151 if (!schedule
.decide
.contains (&r
)) schedule
.decide
.push (mem
, &r
);
2154 Var
& v
= vars
[idx
];
2156 if (v
.binary
) continue;
2157 Cls
* c
= v
.reason
.cls
;
2160 if (!c
->lnd
) continue;
2161 assert (stats
.clauses
.lckd
> 0);
2162 stats
.clauses
.lckd
--;
2164 frames
.shrink (newlevel
+ 1);
2166 queue
= queue2
= trail
;
2168 LOG ("backtrack new level " << newlevel
);
2171 inline int & Solver::iirf (Var
* v
, int t
) {
2172 assert (1 <= t
&& t
< opts
.order
&& 2 <= opts
.order
);
2173 return iirfs
[(opts
.order
- 1) * (v
- vars
) + (t
- 1)];
2176 inline void Solver::rescore () {
2179 for (Rnk
* s
= rnks
+ 1; s
<= rnks
+ maxvar
; s
++) s
->heat
>>= 14;
2180 schedule
.decide
.construct ();
2183 inline void Solver::bump (Var
* v
, int add
) {
2184 assert (stats
.conflicts
> 0);
2186 if (opts
.order
>= 2) {
2188 int w
= inc
, c
= stats
.conflicts
- 1, s
= 512, l
= 9;
2189 for (int i
= 1; i
<= opts
.order
- 1; i
++) {
2191 for (int j
= 1; j
<= opts
.order
- 1; j
++) {
2192 int d
= iirf (v
, j
);
2193 if (d
> c
) continue;
2194 if (d
== c
) inc
+= w
, s
+= (1<<l
);
2199 for (int i
= opts
.order
- 1; i
> 1; i
--)
2200 iirf (v
, i
) = iirf (v
, i
- 1);
2201 iirf (v
, 1) = stats
.conflicts
;
2202 assert ((hinc
>> (opts
.order
-1)) <= inc
&& inc
<= hinc
);
2205 r
->heat
+= inc
+ add
;
2206 LOG ("bump " << 2*(v
- vars
) << " by " << inc
<< " new score " << r
->heat
);
2207 schedule
.decide
.up (r
);
2208 assert (hinc
< (1<<28));
2209 if (r
->heat
>= (1<<24)) {
2210 if (opts
.bumpbulk
) needrescore
= true;
2215 inline void Solver::pull (int lit
) {
2216 Var
* v
= vars
+ (lit
/2);
2217 assert (v
->dlevel
&& !v
->mark
);
2218 LOG ("pulling " << lit
<< " open " << open
);
2221 if (v
->dlevel
== level
) open
++;
2223 lits
.push (mem
, lit
);
2224 if (!frames
[v
->dlevel
].pulled
) {
2225 frames
[v
->dlevel
].pulled
= true;
2226 levels
.push (mem
, v
->dlevel
);
2231 void Solver::cleanlevels () {
2233 int l
= levels
.pop ();
2234 assert (frames
[l
].pulled
);
2235 frames
[l
].pulled
= false;
2239 void Solver::jump () {
2241 int * eolits
= lits
.end ();
2242 for (const int * p
= lits
.begin(); p
< eolits
; p
++) {
2243 Var
* v
= vars
+ (*p
/2);
2244 if (v
->dlevel
< level
&& v
->dlevel
> jlevel
)
2247 LOG ("new jump level " << jlevel
);
2250 void Solver::cleanseen () {
2251 Var
** eos
= seen
.end ();
2252 for (Var
** p
= seen
.begin(); p
< eos
; p
++) {
2253 Var
* v
= *p
; v
->mark
= 0; v
->removable
= v
->poison
= false;
2258 void Solver::bump (Cls
* c
) {
2259 if (c
== &dummy
) return;
2261 if (c
->garbage
) return;
2262 if (!c
->lnd
) return;
2263 assert (!c
->binary
);
2264 mtf (anchor (c
), c
);
2267 for (const int * p
= c
->lits
; (lit
= *p
); p
++)
2268 if (val (lit
) > 0) break;
2271 sprintf (buffer
, "LOG bump %d forcing clause ", lit
);
2272 dbgprint (buffer
, c
);
2273 } else dbgprint ("LOG bump conflicting clause ", c
);
2277 static int revcmptlevel (const void * p
, const void * q
) {
2278 Var
* u
= *(Var
**) p
, * v
= *(Var
**) q
;
2279 return v
->tlevel
- u
->tlevel
;
2282 void Solver::bump () {
2284 Var
** start
, ** end
, ** bos
= seen
.begin (), ** eos
= seen
.end ();
2285 if (opts
.bumpsort
) qsort (bos
, seen
, sizeof *bos
, revcmptlevel
);
2287 for (Var
** p
= bos
; p
< eos
; p
++)
2288 if (p
+1 < eos
) assert (p
[0]->tlevel
> p
[1]->tlevel
);
2290 Var
* uipvar
= vars
+ (uip
/2), * except
= opts
.bumpuip
? 0 : uipvar
;
2292 if (opts
.mtfrev
) start
= bos
, end
= eos
, dir
= 1;
2293 else start
= eos
-1, end
= bos
-1, dir
= -1;
2294 if (opts
.mtfrev
) bump (conflict
);
2295 for (Var
** p
= start
; p
!= end
; p
+= dir
) {
2297 if (v
== uipvar
) continue;
2298 if (v
->dlevel
< level
) continue;
2299 if (v
->binary
) continue;
2300 Cls
* r
= v
->reason
.cls
;
2304 if (!opts
.mtfrev
) bump (conflict
);
2305 // NOTE: this case split is actually redundant since
2306 // we use the variable index order as tie breaker anyhow.
2307 // TODO not really true, since rescore may happen?
2308 if (opts
.bumpbulk
) needrescore
= false;
2309 if (opts
.bumprev
) start
= eos
-1, end
= bos
-1, dir
= -1;
2310 else start
= bos
, end
= eos
, dir
= 1;
2311 int turbo
= opts
.bumpturbo
? eos
- bos
- 1 : 0;
2312 for (Var
** p
= start
; p
!= end
; p
+= dir
) {
2314 if (v
== except
) continue;
2316 if (opts
.bumpturbo
) turbo
--;
2318 if (opts
.bumpbulk
&& needrescore
) rescore ();
2321 bool Solver::analyze () {
2325 if (!level
) return false;
2326 assert (!lits
); assert (!seen
); assert (!levels
);
2329 resolved
= open
= 0;
2333 assert (seen
>= resolved
);
2334 int otf
= seen
- resolved
;
2336 LOG ("resolving " << uip
);
2339 if (!u
|| !u
->binary
) {
2340 Cls
* r
= (u
? u
->reason
.cls
: conflict
); assert (r
);
2341 for (const int * p
= r
->lits
; (lit
= *p
); p
++) {
2342 Var
* v
= vars
+ (lit
/2);
2343 if (!v
->dlevel
) continue;
2344 if (!v
->mark
) { pull (lit
); otf
= INT_MAX
; }
2345 else if (v
->tlevel
<= i
) otf
--;
2348 if (level
> 0 && opts
.otfs
&& otf
<= 0 && r
!= &dummy
) {
2350 printf ("%sLOG on-the-fly strengthened %s clause ",
2351 prfx
, r
->lnd
? "learned" : "original");
2353 printf ("%sLOG on-the-fly strengthening resolvent", prfx
);
2354 for (Var
** p
= seen
.begin (); p
< seen
.end (); p
++)
2355 if ((*p
)->tlevel
<= i
) {
2356 int lit
= 2 * (*p
- vars
);
2357 int val
= vals
[lit
];
2360 printf (" %d", lit
);
2362 fputc ('\n', stdout
);
2367 for (Var
** p
= seen
.begin (); p
< seen
.end (); p
++) {
2370 if (v
->tlevel
> i
) continue;
2371 int idx
= v
- vars
, * q
;
2372 for (q
= r
->lits
; *q
; q
++) if (*q
/2 == idx
) break;
2377 lit
= 2 * (u
- vars
);
2378 int val
= vals
[lit
];
2382 assert (u
->reason
.cls
== r
);
2386 assert (stats
.clauses
.lckd
> 0);
2387 stats
.clauses
.lckd
--;
2390 if (r
->garbage
) r
->garbage
= false;
2393 conflict
= lit2conflict (dummy
, r
->lits
[0], r
->lits
[1]);
2394 stats
.otfs
.dyn
.trn
++;
2398 stats
.otfs
.dyn
.large
++;
2406 assert (u
&& u
->binary
);
2408 lit
= u
->reason
.lit
;
2409 Var
* v
= vars
+ (lit
/2);
2411 if (v
->mark
) { if (v
->tlevel
< i
) otf
--; }
2412 else { pull (lit
); otf
= INT_MAX
; }
2415 if (level
> 0 && opts
.otfs
&& otf
<= 0) {
2416 stats
.otfs
.dyn
.bin
++;
2425 if (!u
->mark
) continue;
2426 assert (u
->dlevel
== level
);
2433 LOG ("uip " << uip
);
2435 lits
.push (mem
, uip
);
2438 printf ("%sLOG 1st uip clause", prfx
);
2439 for (const int * p
= lits
.begin (); p
< lits
.end (); p
++)
2441 fputc ('\n', stdout
);
2445 for (Var
**p
= seen
.begin (); p
< seen
.end (); p
++) {
2446 Var
* v
= *p
; assert (v
->mark
&& !v
->removable
&& !v
->poison
);
2449 int * q
= lits
.begin (), * eolits
= lits
.end ();
2450 for (const int * p
= q
; p
< eolits
; p
++) {
2451 lit
= *p
; Var
* v
= vars
+ (lit
/2);
2452 assert ((v
->dlevel
== level
) == (lit
== uip
));
2453 if (v
->dlevel
< level
&& minimize (v
, 0)) {
2454 LOG ("removing 1st uip literal " << lit
);
2455 stats
.mins
.deleted
++;
2461 eolits
= lits
.end ();
2462 for (const int * p
= lits
.begin(); p
< eolits
; p
++) {
2464 Var
* v
= vars
+ (lit
/2);
2465 if (v
->dlevel
!= jlevel
) continue;
2466 LOG ("literal " << lit
<< " on jump level " << jlevel
);
2470 " variables in minimized 1st UIP clause on jump level " << jlevel
);
2472 if (opts
.inverse
&& cjlevel
== 1) {
2473 q
= lits
.begin (), eolits
= lits
.end ();
2476 for (p
= q
; p
< eolits
; p
++) {
2477 if (inverse (1^*p
)) {
2478 stats
.mins
.inverse
++;
2479 stats
.mins
.deleted
++;
2480 LOG ("literal " << *p
<< " removed due to inverse arc");
2481 assert (cjlevel
> 0);
2490 LOG ("inverse arc decreases jump level");
2497 unsigned glue
= gluelits ();
2502 stats
.lits
.added
+= lits
;
2504 printf ("%sLOG minimized clause", prfx
);
2505 for (const int * p
= lits
.begin (); p
< lits
.end (); p
++)
2507 fputc ('\n', stdout
);
2511 for (const int * p
= lits
.begin (); p
< lits
.end (); p
++)
2512 assert (*p
== uip
|| vars
[*p
/2].dlevel
< level
);
2513 if (unit
) assert (!jlevel
);
2516 if (jlevel
+ 1 < level
) LOG ("backjump to " << jlevel
);
2517 else LOG ("backtrack to " << jlevel
);
2520 if (!jlevel
) iterating
= true;
2525 int strlevel
= jlevel
;
2528 LOG ("analyzing " << strnd
<< " strengthened clauses");
2529 for (Cls
** p
= strnd
.begin (); p
< strnd
.end (); p
++) {
2531 int countnonfalse
= 0, maxlevel
= 0;
2532 for (int * q
= c
->lits
; (lit
= *q
); q
++) {
2533 int val
= vals
[lit
];
2535 if (!val
&& ++countnonfalse
>= 2) break;
2537 if (lit
|| countnonfalse
>= 2) continue;
2538 for (int * q
= c
->lits
; (lit
= *q
); q
++) {
2539 int tmp
= vars
[lit
/2].dlevel
;
2540 if (tmp
> maxlevel
) maxlevel
= tmp
;
2542 int newstrlevel
= 0;
2543 for (int * q
= c
->lits
; (lit
= *q
); q
++) {
2544 int tmp
= vars
[lit
/2].dlevel
;
2545 if (tmp
== maxlevel
) continue;
2546 assert (tmp
< maxlevel
);
2547 if (tmp
> newstrlevel
) newstrlevel
= tmp
;
2549 if (newstrlevel
< strlevel
) strlevel
= newstrlevel
;
2551 if (strlevel
< jlevel
) {
2552 LOG ("strengthened backtrack level " << strlevel
);
2556 unsigned sig
= litsig ();
2557 for (Cls
** p
= strnd
.begin (); !skip
&& p
< strnd
.end (); p
++)
2558 if (fwsub (sig
, *p
)) skip
= true;
2561 LOG ("learned clause subsumed by strengthened clause");
2562 for (Cls
** p
= strnd
.begin (); p
< strnd
.end (); p
++) {
2565 for (int * q
= c
->lits
; (lit
= *q
); q
++) {
2566 Val val
= vals
[lit
];
2567 if (val
< 0) continue;
2574 assert (!c
->garbage
);
2576 int other
= c
->lits
[0] + c
->lits
[1];
2578 imply (unit
, other
);
2579 } else force (unit
, c
);
2582 LOG ("learned clause skipped because of forcing strengthened clause");
2584 for (Cls
** p
= strnd
.begin (); p
< strnd
.end (); p
++)
2585 assert ((*p
)->str
), (*p
)->str
= false;
2588 if (!skip
|| !lnd
) {
2589 for (Frame
* f
= frames
.begin (); f
< frames
.end (); f
++)
2590 assert (!f
->contained
);
2591 Cls
* cls
= clause (lnd
, lnd
? glue
: 0); //TODO: move before if?
2592 if (!vals
[uip
] && strlevel
== jlevel
) {
2595 int other
= cls
->lits
[0] + cls
->lits
[1];
2605 while (fresh
.count
> limit
.reduce
.fresh
&& fresh
.tail
) {
2606 Cls
* f
= fresh
.tail
;
2609 assert (!f
->binary
);
2612 push (anchor (f
), f
);
2614 int count
= opts
.dynred
;
2616 for (int glue
= opts
.glue
;
2617 glue
>= opts
.sticky
&& count
>= 0 && recycling ();
2619 ctc
= learned
[glue
].tail
;
2620 while (ctc
&& count
-- >= 0 && recycling ()) {
2621 Cls
* next
= ctc
->next
;
2622 assert (!ctc
->binary
);
2623 if (ctc
!= cls
&& !ctc
->locked
) recycle (ctc
);
2628 } else lits
.shrink ();
2630 long long tmp
= hinc
;
2631 tmp
*= 100 + opts
.heatinc
; tmp
/= 100;
2632 assert (tmp
<= INT_MAX
);
2638 int Solver::luby (int i
) {
2640 for (k
= 1; k
< 32; k
++)
2641 if (i
== (1 << k
) - 1)
2645 if ((1 << (k
-1)) <= i
&& i
< (1 << k
) - 1)
2646 return luby (i
- (1u << (k
-1)) + 1);
2649 inline double Stats::height () {
2650 return decisions
? sumheight
/ (double) decisions
: 0.0;
2653 void Solver::increp () {
2654 if ((stats
.reports
++ % 19)) return;
2658 " clauses fixed eliminated learned agility"
2661 " seconds variables equivalent conflicts height MB"
2663 "%s .\n", prfx
, prfx
, prfx
, prfx
);
2666 int Solver::remvars () const {
2668 res
-= stats
.vars
.fixed
;
2669 res
-= stats
.vars
.equiv
;
2670 res
-= stats
.vars
.elim
;
2671 res
-= stats
.vars
.pure
;
2672 res
-= stats
.vars
.zombies
;
2677 void Solver::report (int v
, char type
) {
2678 if (opts
.quiet
|| v
> opts
.verbose
) return;
2680 countch
[0] = countch
[1] = ' ';
2681 if (terminal
&& type
== lastype
) {
2683 if (type
!= 'e' && type
!= 'p' && type
!= 'k') {
2684 countch
[0] = '0' + (typecount
% 10);
2685 if (typecount
>= 10) countch
[1] = '0' + (typecount
% 100)/10;
2689 if (terminal
&& lastype
) fputc ('\n', out
);
2692 assert (maxvar
>= stats
.vars
.fixed
+ stats
.vars
.equiv
+ stats
.vars
.elim
);
2693 fprintf (out
, "%s%c%c%c%7.1f %7d %7d %6d %6d %6d %7d %6d %6.1f %2.0f %4.0f",
2695 countch
[1], countch
[0], type
, stats
.seconds (),
2698 stats
.vars
.fixed
, stats
.vars
.equiv
,
2700 type
=='e'?schedule
.elim
:
2701 (type
=='p'?schedule
.probe
:
2702 (type
=='k'?schedule
.block
:stats
.conflicts
)),
2703 (type
=='F'?limit
.reduce
.fresh
:
2704 (type
=='l' || type
=='+' || type
== '-') ?
2705 limit
.reduce
.learned
: stats
.clauses
.lnd
),
2708 mem
/ (double) (1<<20));
2709 if (!terminal
|| type
=='0' || type
=='1' || type
=='?') fputc ('\n', out
);
2710 else fputc ('\r', out
);
2715 void Solver::restart () {
2716 int skip
= agility
>= opts
.skip
* 100000;
2717 if (skip
) stats
.restart
.skipped
++;
2718 else stats
.restart
.count
++;
2719 limit
.restart
.conflicts
= stats
.conflicts
;
2721 if (opts
.luby
) delta
= opts
.restartint
* luby (++limit
.restart
.lcnt
);
2723 if (limit
.restart
.inner
>= limit
.restart
.outer
) {
2724 limit
.restart
.inner
= opts
.restartint
;
2725 limit
.restart
.outer
*= 100 + opts
.restartouter
;
2726 limit
.restart
.outer
/= 100;
2728 limit
.restart
.inner
*= 100 + opts
.restartinner
;
2729 limit
.restart
.inner
/= 100;
2731 delta
= limit
.restart
.inner
;
2733 limit
.restart
.conflicts
+= delta
;
2734 if (!skip
) undo (0);
2735 if (stats
.restart
.maxdelta
< delta
) {
2736 stats
.restart
.maxdelta
= delta
;
2737 report (1, skip
? 'N' : 'R');
2739 report (2, skip
? 'n' :'r');
2742 void Solver::rebias () {
2743 limit
.rebias
.conflicts
= stats
.conflicts
;
2744 int delta
= opts
.rebiasint
* luby (++limit
.rebias
.lcnt
);
2745 limit
.rebias
.conflicts
+= delta
;
2746 if (!opts
.rebias
) return;
2747 stats
.rebias
.count
++;
2748 for (Var
* v
= vars
+ 1; v
<= vars
+ maxvar
; v
++) v
->phase
= 0;
2750 if (stats
.rebias
.maxdelta
>= delta
) report (2, 'b');
2751 else stats
.rebias
.maxdelta
= delta
, report (1, 'B');
2754 inline int Solver::redundant (Cls
* c
) {
2756 assert (!c
->locked
);
2757 assert (!c
->garbage
);
2759 for (const int * p
= c
->lits
; *p
; p
++) {
2760 Var
* v
= vars
+ (*p
/2);
2762 assert (v
->type
!= ELIM
);
2765 int res
= 0, * p
, lit
;
2767 bool shrink
= false;
2768 for (p
= c
->lits
; !res
&& (lit
= *p
); p
++) {
2769 int other
= find (lit
);
2770 Var
* v
= vars
+ (other
/2);
2771 assert ((v
->type
!= ELIM
));
2772 Val val
= vals
[other
];
2773 if (val
> 0 && !v
->dlevel
) res
= 1;
2774 else if (val
< 0 && !v
->dlevel
) shrink
= true;
2776 val
= lit2val (other
);
2777 if (v
->mark
== val
) { shrink
= true; continue; }
2778 else if (v
->mark
== -val
) res
= 1;
2782 while (p
> c
->lits
) vars
[find (*--p
)/2].mark
= 0;
2784 for (p
= c
->lits
; *p
; p
++) assert (!vars
[find (*p
)/2].mark
);
2786 if (shrink
|| res
) {
2787 for (p
= c
->lits
; *p
; p
++) check
.push (mem
, *p
);
2788 check
.push (mem
, 0);
2790 if (res
) return res
;
2792 p
= c
->lits
; int * q
= p
;
2793 while (!res
&& (lit
= *p
)) {
2795 int other
= find (lit
);
2796 if (other
!= lit
) simplified
= true;
2797 Var
* v
= vars
+ (other
/2);
2798 assert (v
->type
!= ELIM
);
2799 Val val
= vals
[other
];
2800 if (val
&& !v
->dlevel
) {
2801 if (val
> 0) res
= 1;
2803 val
= lit2val (other
);
2804 if (v
->mark
== val
) continue;
2805 if (v
->mark
== -val
) res
= 1;
2806 else { assert (!v
->mark
); v
->mark
= val
; *q
++ = other
; }
2811 if (!res
) assert (!*q
&& !*p
);
2813 int newsize
= q
- c
->lits
;
2817 newsize
<= opts
.redsub
&&
2818 (!c
->lnd
|| c
->binary
)) {
2819 limit
.budget
.red
+= 10;
2821 for (p
= c
->lits
; !res
&& (lit
= *p
) && limit
.budget
.red
>= 0; p
++) {
2822 INC (sigs
.fw
.l2
.srch
);
2823 if (!(fwsigs
[lit
] & c
->sig
)) { INC (sigs
.fw
.l2
.hits
); continue; }
2824 if (fwds
[lits
] > opts
.fwmaxlen
) continue;
2825 for (int i
= 0; !res
&& i
< fwds
[lit
] && limit
.budget
.red
>= 0; i
++) {
2827 Cls
* d
= fwds
[lit
][i
];
2829 if (d
->garbage
) continue;
2830 if (d
->size
> (unsigned) newsize
) continue;
2831 if (d
->size
> (unsigned) opts
.redsub
) continue;
2832 if (!c
->lnd
&& d
->lnd
&& !d
->binary
) continue;
2833 INC (sigs
.fw
.l1
.srch
);
2834 if (!sigsubs (d
->sig
, c
->sig
)) { INC (sigs
.fw
.l1
.hits
); continue; };
2836 for (const int * r
= d
->lits
; (other
= *r
); r
++) {
2837 Val u
= lit2val (other
), v
= vars
[other
/2].mark
;
2840 if ((res
= !other
)) {
2842 limit
.budget
.red
+= 20;
2843 if (!c
->lnd
&& d
->lnd
) {
2846 stats
.clauses
.irr
++;
2853 while (q
-- > c
->lits
) {
2854 assert (vars
[*q
/2].mark
); vars
[*q
/2].mark
= 0;
2857 if (res
) return res
;
2859 if (newsize
> 1 && newsize
<= opts
.redsub
&& (!c
->lnd
|| c
->binary
))
2860 fwds
[c
->minlit ()].push (mem
, c
);
2863 if (!newsize
) conflict
= &empty
;
2864 else if (newsize
== 1) {
2865 LOG ("learned clause " << c
->lits
[0]);
2867 } else if (newsize
== 2 && !c
->binary
&& 2 < c
->size
) {
2868 if (c
->lnd
) assert (stats
.clauses
.lnd
), stats
.clauses
.lnd
--;
2869 else assert (stats
.clauses
.orig
), stats
.clauses
.orig
--;
2870 stats
.clauses
.bin
++;
2874 } else assert (!res
);
2879 void Solver::checkvarstats () {
2882 int fixed
= 0, equivalent
= 0, eliminated
= 0, pure
= 0, zombies
= 0;
2883 for (Var
* v
= vars
+ 1; v
<= vars
+ maxvar
; v
++) {
2884 int lit
= 2 * (v
- vars
);
2885 if (v
->type
== ELIM
) eliminated
++;
2886 else if (v
->type
== PURE
) pure
++;
2887 else if (v
->type
== ZOMBIE
) zombies
++;
2888 else if (vals
[lit
]) { assert (v
->type
== FIXED
); fixed
++; }
2889 else if (repr
[lit
]) { assert (v
->type
== EQUIV
); equivalent
++; }
2890 else assert (v
->type
== FREE
);
2892 assert (fixed
== stats
.vars
.fixed
);
2893 assert (eliminated
== stats
.vars
.elim
);
2894 assert (pure
== stats
.vars
.pure
);
2895 assert (zombies
== stats
.vars
.zombies
);
2896 assert (equivalent
== stats
.vars
.equiv
);
2900 void Solver::decompose () {
2902 if (!opts
.decompose
) return;
2905 size_t bytes
= 2 * (maxvar
+ 1) * sizeof (SCC
);
2906 SCC
* sccs
= (SCC
*) mem
.callocate (bytes
);
2910 LOG ("starting scc decomposition");
2911 for (int root
= 2; !conflict
&& root
<= 2*maxvar
+ 1; root
++) {
2912 if (sccs
[root
].idx
) { assert (sccs
[root
].done
); continue; }
2914 work
.push (mem
, root
);
2915 LOG ("new scc root " << root
);
2916 while (!conflict
&& work
) {
2917 int lit
= work
.top ();
2918 if (sccs
[lit
^1].idx
&& !sccs
[lit
^1].done
) {
2919 Val val
= vals
[lit
];
2921 LOG ("conflict while learning unit in scc");
2924 LOG ("learned clause " << lit
);
2930 if (conflict
) break;
2931 Stack
<int> & os
= occs
[1^lit
].bins
;
2933 if (!sccs
[lit
].idx
) {
2934 assert (!sccs
[lit
].done
);
2935 sccs
[lit
].idx
= sccs
[lit
].min
= ++dfsi
;
2936 saved
.push (mem
, lit
);
2938 int other
= os
[--i
];
2939 if (sccs
[other
].idx
) continue;
2940 work
.push (mem
, other
);
2944 if (!sccs
[lit
].done
) {
2946 int other
= os
[--i
];
2947 if (sccs
[other
].done
) continue;
2948 sccs
[lit
].min
= min (sccs
[lit
].min
, sccs
[other
].min
);
2950 SCC
* scc
= sccs
+ lit
;
2951 unsigned min
= scc
->min
;
2952 if (min
!= scc
->idx
) { assert (min
< scc
->idx
); continue; }
2953 n
++; LOG ("new scc " << n
);
2954 int m
= 0, prev
= 0, other
= 0;
2955 while (!conflict
&& other
!= lit
) {
2956 other
= saved
.pop ();
2957 sccs
[other
].done
= true;
2958 LOG ("literal " << other
<< " added to scc " << n
);
2960 int a
= find (prev
), b
= find (other
);
2961 if (a
== b
) continue;
2963 LOG ("conflict while merging scc");
2965 } else if (val (a
) || val (b
)) {
2966 assert (val (a
) == val (b
));
2968 merge (prev
, other
, stats
.sccs
.merged
);
2971 } else prev
= other
;
2973 if (m
) stats
.sccs
.nontriv
++;
2979 LOG ("found " << n
<< " sccs");
2980 assert (conflict
|| dfsi
<= 2 * maxvar
);
2982 mem
.deallocate (sccs
, bytes
);
2990 void Solver::disconnect () {
2991 cleangate (), cleantrash ();
2992 for (int lit
= 2; lit
<= 2*maxvar
+ 1; lit
++)
2993 occs
[lit
].bins
.release (mem
), occs
[lit
].large
.release (mem
);
2994 assert (!orgs
&& !fwds
&& !fwsigs
);
2998 void Solver::connect (Anchor
<Cls
> & anchor
, bool orgonly
) {
2999 for (Cls
* p
= anchor
.tail
; p
; p
= p
->next
) {
3000 assert (&anchor
== &this->anchor (p
));
3001 if (!orgonly
|| !p
->lnd
) connect (p
);
3005 void Solver::gc (Anchor
<Cls
> & anchor
, const char * type
) {
3006 limit
.budget
.red
= 10000;
3007 Cls
* p
= anchor
.tail
;
3009 anchor
.head
= anchor
.tail
= 0;
3012 Cls
* next
= p
->next
;
3014 p
->next
= p
->prev
= 0;
3018 red
= redundant (p
);
3019 if (red
> 0) p
->garbage
= true;
3021 if (p
->garbage
) { collect (p
); collected
++; }
3022 else if (!red
) push (anchor
, p
);
3023 else assert (connected (binary
, p
));
3028 LOG ("collected " << collected
<< ' ' << type
<< " clauses");
3034 inline void Solver::checkclean () {
3037 for (int i
= 0; i
<= 3 + opts
.glue
; i
++) {
3039 if (i
== 0) p
= original
.head
;
3040 if (i
== 1) p
= binary
.head
;
3041 if (i
== 2) p
= fresh
.head
;
3042 if (i
>= 3) p
= learned
[i
-3].head
;
3044 for (int * q
= p
->lits
; *q
; q
++) {
3046 assert (!repr
[lit
]);
3047 assert (!vals
[lit
]);
3048 Var
* v
= vars
+ (lit
/2);
3049 assert (v
->type
== FREE
);
3058 void Solver::gc () {
3060 size_t old
= stats
.collected
;
3067 gc (binary
, "binary");
3068 gc (original
, "original");
3069 gc (fresh
, "fresh");
3070 for (int glue
= 0; glue
<= opts
.glue
; glue
++) {
3072 sprintf (buffer
, "learned[%u]", glue
);
3073 gc (learned
[glue
], buffer
);
3079 for (int glue
= 0; glue
<= opts
.glue
; glue
++)
3080 connect (learned
[glue
]);
3084 size_t bytes
= stats
.collected
- old
;
3085 LOG ("collected " << bytes
<< " bytes");
3093 inline int Solver::recyclelimit () const {
3094 return limit
.reduce
.learned
+ stats
.clauses
.lckd
;
3097 inline bool Solver::recycling () const {
3098 return stats
.clauses
.lnd
>= recyclelimit ();
3101 void Solver::reduce () {
3103 assert (trail
== queue
);
3106 while ((f
= fresh
.tail
)) {
3109 assert (!f
->binary
);
3112 push (anchor (f
), f
);
3114 int goal
= (stats
.clauses
.lnd
- stats
.clauses
.lckd
)/2, count
= 0;
3115 for (int glue
= opts
.glue
; glue
>= opts
.sticky
&& count
< goal
; glue
--) {
3117 for (Cls
* p
= learned
[glue
].tail
; p
&& count
< goal
; p
= next
) {
3119 if (p
->locked
) continue;
3126 if (count
>= goal
/2) report (1, '/');
3127 else report (1, '='), enlarge ();
3130 inline void Solver::checkeliminated () {
3133 for (int i
= 0; i
<= 3 + (int)opts
.glue
; i
++) {
3135 if (i
== 0) p
= original
.head
;
3136 if (i
== 1) p
= binary
.head
;
3137 if (i
== 1) p
= fresh
.head
;
3138 if (i
>= 3) p
= learned
[i
-3].head
;
3140 for (int * q
= p
->lits
; *q
; q
++) {
3142 Var
* v
= vars
+ (lit
/2);
3143 assert (v
->type
!= ELIM
);
3152 void Solver::probe () {
3155 assert (queue2
== trail
);
3157 stats
.probe
.phases
++;
3159 for (const Rnk
* r
= rnks
+ 1; r
<= rnks
+ maxvar
; r
++) {
3161 int lit
= 2 * (r
- rnks
);
3162 int old_heat
= p
->heat
;
3163 int new_heat
= jwhs
[lit
] + jwhs
[lit
^1];
3164 if (new_heat
< 0) new_heat
= INT_MAX
;
3166 if (schedule
.probe
.contains (p
)) {
3167 if (new_heat
> old_heat
) schedule
.probe
.up (p
);
3168 else if (new_heat
< old_heat
) schedule
.probe
.down (p
);
3171 int repcounter
= 111;
3173 if (opts
.rtc
== 2 || opts
.probertc
== 2 ||
3174 ((opts
.rtc
== 1 || opts
.probertc
== 1) && !stats
.probe
.rounds
))
3177 bound
= stats
.props
.simp
+ opts
.probeint
;
3178 for (int i
= stats
.probe
.phases
; i
<= opts
.probeboost
; i
++)
3179 bound
+= opts
.probeint
;
3181 int last
= -1, filled
= 0;
3182 if (!schedule
.probe
) {
3185 for (int idx
= 1; idx
<= maxvar
; idx
++) {
3186 Var
& v
= vars
[idx
];
3187 if (v
.type
!= FREE
&& v
.type
!= EQUIV
) continue;
3189 assert (!vals
[lit
]);
3190 if (repr
[lit
]) continue;
3192 // TODO replace && by '==' for incremental scc computation
3193 if (!occs
[lit
].bins
== !occs
[lit
^1].bins
) continue;
3195 if (!occs
[lit
].bins
&& !occs
[lit
^1].bins
) continue;
3197 Rnk
* p
= prbs
+ idx
;
3198 schedule
.probe
.push (mem
, p
);
3202 while (stats
.props
.simp
< bound
&& !conflict
) {
3203 if (!--repcounter
) {
3204 if (terminal
) report (2, 'p');
3208 if (!schedule
.probe
) {
3209 stats
.probe
.rounds
++;
3210 if (last
== filled
) goto FILL
;
3213 Rnk
* p
= schedule
.probe
.pop ();
3215 Var
& v
= vars
[idx
];
3216 if (v
.type
!= FREE
&& v
.type
!= EQUIV
) continue;
3218 assert (!vals
[lit
]);
3219 if (repr
[lit
]) continue;
3221 long long old
= stats
.props
.simp
;
3222 LOG ("probing " << lit
);
3223 stats
.probe
.variables
++;
3227 if (!ok
) goto FAILEDLIT
;
3229 LOG ("probing " << lit
);
3231 stats
.probe
.variables
++;
3232 if (!bcp ()) { undo (0); goto FAILEDLIT
; }
3234 int * q
= saved
.begin (), * eos
= saved
.end ();
3235 for (const int * p
= q
; p
< eos
; p
++) {
3237 if (other
== (lit
^1)) continue;
3238 if (vals
[other
] < 0) merge (lit
, other
^1, stats
.probe
.merged
);
3239 if (vals
[other
] <= 0) continue;
3243 if (q
== saved
.begin ()) continue;
3245 for (const int * p
= saved
.begin (); p
< q
; p
++) {
3246 stats
.probe
.lifted
++;
3249 LOG ("lifting " << other
);
3250 LOG ("learned clause " << other
);
3254 goto BCPANDINCBOUND
;
3256 stats
.probe
.failed
++;
3258 LOG ("learned clause " << (1^lit
));
3262 if (bound
!= LLONG_MAX
)
3263 bound
+= opts
.probereward
+ (stats
.props
.simp
- old
);
3266 limit
.props
.probe
= opts
.probeprd
;
3267 limit
.props
.probe
*= opts
.probeint
;
3268 limit
.props
.probe
+= stats
.props
.srch
;
3269 limit
.fixed
.probe
= stats
.vars
.fixed
;
3275 bool Solver::andgate (int lit
) {
3277 assert (vars
[lit
/2].type
!= ELIM
);
3278 assert (!gate
&& !gatestats
);
3279 if (!opts
.subst
) return false;
3280 if (!opts
.ands
) return false;
3281 if (!orgs
[lit
] || !orgs
[1^lit
]) return false;
3283 int other
, notlit
= (1^lit
), bound
= 1000;
3284 for (int i
= 0; !b
&& i
< orgs
[lit
] && bound
-- >= 0; i
++) {
3285 Cls
* c
= orgs
[lit
][i
];
3286 if (!sigsubs (c
->sig
, bwsigs
[lit
^1])) continue;
3291 for (const int * p
= c
->lits
; (other
= *p
); p
++) {
3292 if (lit
== other
) { hit
= true; continue; }
3293 assert (!vars
[other
/2].mark
);
3294 vars
[other
/2].mark
= -lit2val (other
);
3299 int count
= gatelen
;
3300 for (int j
= 0; j
< orgs
[notlit
] && bound
-- >= 0; j
++) {
3301 if (orgs
[notlit
] - j
< count
) break;
3302 Cls
* d
= orgs
[notlit
][j
];
3303 if (d
->lits
[2]) continue;
3304 int pos
= (d
->lits
[1] == notlit
);
3305 assert (d
->lits
[pos
] == notlit
);
3307 other
= d
->lits
[!pos
];
3308 if (vars
[other
/2].mark
!= lit2val (other
)) continue;
3309 vars
[other
/2].mark
= 0;
3311 if (!--count
) break;
3313 for (const int * p
= c
->lits
; (other
= *p
); p
++)
3314 vars
[other
/2].mark
= 0;
3315 if (count
) cleangate (); else b
= c
;
3317 if (!b
) { assert (!gate
); return false; }
3318 assert (gate
== gatelen
+ 1);
3319 gatestats
= (gatelen
>= 2) ? &stats
.subst
.ands
: &stats
.subst
.nots
;
3323 printf ("%sLOG %s gate %d = ", prfx
, (gatelen
>= 2) ? "and" : "not", lit
);
3324 for (const int * p
= b
->lits
; (other
= *p
); p
++) {
3325 if (other
== lit
) continue;
3326 printf ("%d", (1^other
));
3327 if (p
[1] && (p
[1] != lit
|| p
[2])) fputs (" & ", stdout
);
3329 fputc ('\n', stdout
);
3335 bool Solver::xorgate (int lit
) {
3337 assert (vars
[lit
/2].type
!= ELIM
);
3338 assert (!gate
&& !gatestats
);
3339 if (!opts
.subst
) return false;
3340 if (!opts
.xors
) return false;
3341 if (orgs
[lit
] < 2 || orgs
[1^lit
] < 2) return false;
3342 if (orgs
[lit
] > orgs
[1^lit
]) lit
^= 1;
3344 int len
= 0, other
, bound
= 600;
3345 for (int i
= 0; i
< orgs
[lit
] && !b
&& bound
-- >= 0; i
++) {
3346 Cls
* c
= orgs
[lit
][i
];
3347 const int maxlen
= 20;
3348 assert (maxlen
< 31);
3349 if (c
->size
> (unsigned) maxlen
) continue;
3350 if (!c
->lits
[2]) continue;
3351 assert (!c
->binary
);
3352 if (!sigsubs (c
->sig
, bwsigs
[lit
^1])) continue;
3354 for (p
= c
->lits
; *p
; p
++)
3358 int required
= (1 << (len
-1));
3359 for (p
= c
->lits
; (other
= *p
); p
++) {
3360 if (other
== lit
) continue;
3361 if (orgs
[other
] < required
) break;
3362 if (orgs
[other
^1] < required
) break;
3363 if (!sigsubs (c
->sig
, bwsigs
[other
])) break;
3364 if (!sigsubs (c
->sig
, bwsigs
[1^other
])) break;
3366 if (other
) continue;
3368 assert (0 < len
&& len
<= maxlen
);
3370 for (signs
= 0; signs
< (1u<<len
) && bound
-- >= 0; signs
++) {
3371 if (parity (signs
)) continue;
3372 int start
= 0, startlen
= INT_MAX
, s
= 0;
3373 for (p
= c
->lits
; (other
= *p
); p
++, s
++) {
3374 if ((signs
& (1u<<s
))) other
^= 1;
3375 int tmp
= orgs
[other
];
3376 if (start
&& tmp
>= startlen
) continue;
3380 assert (s
== len
&& start
&& startlen
< INT_MAX
);
3383 for (j
= 0; !found
&& j
< orgs
[start
] && bound
-- >= 0; j
++) {
3384 Cls
* d
= orgs
[start
][j
];
3385 if (d
->sig
!= c
->sig
) continue;
3386 for (p
= d
->lits
; *p
; p
++)
3388 if (p
- d
->lits
!= len
) continue;
3391 for (p
= c
->lits
; (other
= *p
); p
++, s
++) {
3392 if ((signs
& (1u<<s
))) other
^= 1;
3393 if (other
== start
) { hit
= true; continue; }
3394 if (!d
->contains (other
)) break;
3396 assert (other
|| hit
);
3397 if (!other
) found
= d
;
3399 assert (bound
< 0 || signs
|| found
);
3405 if (signs
== (1u<<len
)) { assert (!required
); b
= c
; }
3408 if (!b
) { assert (!gate
); return false; }
3410 assert (gate
== (1<<(len
-1)));
3412 gatestats
= &stats
.subst
.xors
;
3414 int pos
= -1, neg
= gate
;
3416 while (pos
+1 < neg
&& gate
[pos
+1]->contains (lit
)) pos
++;
3417 assert (pos
>= gate
|| gate
[pos
+1]->contains(1^lit
));
3418 if (pos
+1 == neg
) break;
3419 while (pos
< neg
-1 && gate
[neg
-1]->contains ((1^lit
))) neg
--;
3420 assert (neg
< 0 || gate
[neg
-1]->contains(lit
));
3421 if (pos
+1 == neg
) break;
3423 swap (gate
[++pos
], gate
[--neg
]);
3427 printf ("%sLOG %d-ary xor gate %d = ", prfx
, len
-1, (lit
^1));
3428 for (const int * p
= b
->lits
; (other
= *p
); p
++) {
3429 if (other
== lit
) continue;
3430 printf ("%d", other
);
3431 if (p
[1] && (p
[1] != lit
|| p
[2])) fputs (" ^ ", stdout
);
3433 fputc ('\n', stdout
);
3439 Cls
* Solver::find (int a
, int b
, int c
) {
3440 unsigned sig
= listig (a
) | listig (b
) | listig (c
);
3441 unsigned all
= bwsigs
[a
] & bwsigs
[b
] & bwsigs
[c
];
3442 if (!sigsubs (sig
, all
)) return 0;
3444 if (orgs
[start
] > orgs
[b
]) start
= b
;
3445 if (orgs
[start
] > orgs
[c
]) start
= c
;
3446 for (int i
= 0; i
< orgs
[start
]; i
++) {
3447 Cls
* res
= orgs
[start
][i
];
3448 if (res
->sig
!= sig
) continue;
3449 assert (res
->lits
[0] && res
->lits
[1]);
3450 if (!res
->lits
[2]) continue;
3451 assert (!res
->binary
);
3452 if (res
->lits
[3]) continue;
3453 int l0
= res
->lits
[0], l1
= res
->lits
[1], l2
= res
->lits
[2];
3454 if ((a
== l0
&& b
== l1
&& c
== l2
) ||
3455 (a
== l0
&& b
== l2
&& c
== l1
) ||
3456 (a
== l1
&& b
== l0
&& c
== l2
) ||
3457 (a
== l1
&& b
== l2
&& c
== l0
) ||
3458 (a
== l2
&& b
== l0
&& c
== l1
) ||
3459 (a
== l2
&& b
== l1
&& c
== l2
)) return res
;
3464 int Solver::itegate (int lit
, int cond
, int t
) {
3465 Cls
* c
= find (lit
^1, cond
, t
^1);
3467 int start
= lit
, nc
= (cond
^1), bound
= 200;
3468 if (orgs
[nc
] < orgs
[start
]) start
= nc
;
3469 unsigned sig
= listig (lit
) | listig (nc
);
3470 for (int i
= 0; i
< orgs
[start
] && --bound
>= 0; i
++) {
3471 Cls
* d
= orgs
[start
][i
];
3472 if (!sigsubs (sig
, d
->sig
)) continue;
3473 assert (d
->lits
[0] && d
->lits
[1]);
3474 if (!d
->lits
[2]) continue;
3475 assert (!d
->binary
);
3476 if (d
->lits
[3]) continue;
3477 int l0
= d
->lits
[0], l1
= d
->lits
[1], l2
= d
->lits
[2], res
;
3478 if (l0
== lit
&& l1
== nc
) res
= l2
;
3479 else if (l1
== lit
&& l0
== nc
) res
= l2
;
3480 else if (l0
== lit
&& l2
== nc
) res
= l1
;
3481 else if (l2
== lit
&& l0
== nc
) res
= l1
;
3482 else if (l1
== lit
&& l2
== nc
) res
= l0
;
3483 else if (l2
== lit
&& l1
== nc
) res
= l0
;
3485 Cls
* e
= find (lit
^1, nc
, res
^1);
3495 bool Solver::itegate (int lit
) {
3497 assert (vars
[lit
/2].type
!= ELIM
);
3498 assert (!gate
&& !gatestats
);
3499 if (!opts
.subst
) return false;
3500 if (!opts
.ites
) return false;
3501 if (orgs
[lit
] < 2 || orgs
[1^lit
] < 2) return false;
3502 if (orgs
[lit
] > orgs
[1^lit
]) lit
^= 1;
3504 int cond
= 0, t
= 0, e
= 0;
3505 for (int i
= 0; i
< orgs
[lit
] && !b
; i
++) {
3506 Cls
* c
= orgs
[lit
][i
];
3507 assert (c
->lits
[0] && c
->lits
[1]);
3508 if (!c
->lits
[2]) continue;
3509 assert (!c
->binary
);
3510 if (c
->lits
[3]) continue;
3512 int o0
, o1
, l0
= c
->lits
[0], l1
= c
->lits
[1], l2
= c
->lits
[2];
3513 if (lit
== l0
) o0
= l1
, o1
= l2
;
3514 else if (lit
== l1
) o0
= l0
, o1
= l2
;
3515 else assert (lit
== l2
), o0
= l0
, o1
= l1
;
3518 if ((e
= itegate (lit
, cond
= o0
, t
= o1
)) ||
3519 (e
= itegate (lit
, cond
= o1
, t
= o0
))) b
= c
;
3522 if (!b
) { assert (!gate
); return false; }
3523 assert (cond
&& t
&& e
);
3525 gatestats
= &stats
.subst
.ites
;
3529 LOG ("ite gate " << lit
<< " = " <<
3530 (1^cond
) << " ? " << (1^t
) << " : " << (1^e
));
3536 bool Solver::resolve (Cls
* c
, int pivot
, Cls
* d
, bool tryonly
) {
3537 if (tryonly
) resotfs
= reslimhit
= false;
3538 assert (tryonly
|| (c
->dirty
&& d
->dirty
));
3539 assert (tryonly
!= (vars
[pivot
/2].type
== ELIM
));
3540 assert (!vals
[pivot
] && !repr
[pivot
]);
3541 if (!tryonly
&& gate
&& c
->gate
== d
->gate
) return false;
3542 if (elimode
) stats
.elim
.resolutions
++;
3543 else { assert (blkmode
); stats
.blkd
.resolutions
++; }
3544 int other
, notpivot
= (1^pivot
), clits
= 0, dlits
= 0;
3545 bool found
= false, res
= true;
3548 for (p
= c
->lits
; (other
= *p
); p
++) {
3549 if (other
== pivot
) { found
= true; continue; }
3550 assert (other
!= notpivot
);
3551 assert (find (other
) == other
);
3552 assert (other
!= notpivot
);
3553 if (other
== pivot
) continue;
3554 Val v
= vals
[other
];
3555 if (v
< 0) continue;
3556 if (v
> 0) { res
= false; goto DONE
; }
3557 assert (!vars
[other
/2].mark
);
3558 Val u
= lit2val (other
);
3559 vars
[other
/2].mark
= u
;
3560 lits
.push (mem
, other
);
3565 for (p
= d
->lits
; (other
= *p
); p
++) {
3566 if (other
== notpivot
) { found
= true; continue; }
3567 assert (other
!= pivot
);
3568 assert (find (other
) == other
);
3569 assert (other
!= pivot
);
3570 if (other
== notpivot
) continue;
3571 Val v
= vals
[other
];
3572 if (v
< 0) continue;
3573 if (v
> 0) { res
= false; goto DONE
; }
3575 v
= vars
[other
/2].mark
;
3576 Val u
= lit2val (other
);
3578 vars
[other
/2].mark
= u
;
3579 lits
.push (mem
, other
);
3580 } else if (v
!= u
) { res
= false; goto DONE
; }
3583 if (opts
.otfs
&& tryonly
) {
3585 bool logresolvent
= false;
3587 if (lits
== clits
&& (!blkmode
|| opts
.blockotfs
)) {
3589 dbgprint ("LOG static on-the-fly strengthened clause ", c
);
3590 dbgprint ("LOG static on-the-fly antecedent ", d
);
3591 logresolvent
= true;
3593 if (c
->gate
) cleangate ();
3596 if (clits
== 1) stats
.otfs
.stat
.bin
++;
3597 else if (clits
== 2) stats
.otfs
.stat
.trn
++;
3598 else stats
.otfs
.stat
.large
++;
3600 if (lits
== dlits
&& (!blkmode
|| opts
.blockotfs
)) {
3602 dbgprint ("LOG static on-the-fly strengthened clause ", d
);
3603 dbgprint ("LOG static on-the-fly antecedent ", c
);
3604 logresolvent
= true;
3606 if (d
->gate
) cleangate ();
3607 remove (notpivot
, d
);
3609 if (dlits
== 1) stats
.otfs
.stat
.bin
++;
3610 else if (dlits
== 2) stats
.otfs
.stat
.trn
++;
3611 else stats
.otfs
.stat
.large
++;
3615 printf ("%sLOG static on-the-fly subsuming resolvent", prfx
);
3616 for (p
= lits
.begin (); p
< lits
.end (); p
++) printf (" %d", *p
);
3617 fputc ('\n', stdout
);
3622 for (p
= lits
.begin (); p
< lits
.end (); p
++) {
3623 Var
* u
= vars
+ (*p
/2);
3629 LOG ("conflict in resolving clauses");
3632 } else if (lits
== 1) {
3633 LOG ("learned clause " << lits
[0]);
3636 } else if (!tryonly
) {
3642 if (lits
> opts
.reslim
) reslimhit
= true;
3649 inline void Solver::checkgate () {
3651 for (int i
= 0; i
< posgate
; i
++) assert (gate
[i
]->contains (gatepivot
));
3652 for (int i
= posgate
; i
< gate
; i
++) assert (gate
[i
]->contains (1^gatepivot
));
3653 for (int i
= 0; i
< posgate
; i
++)
3654 for (int j
= posgate
; j
< gate
; j
++)
3655 assert (!resolve (gate
[i
], gatepivot
, gate
[j
], true));
3659 inline void Solver::block (Cls
* c
, int lit
) {
3660 assert (opts
.block
);
3662 dbgprint ("LOG blocked clause ", c
);
3663 LOG ("blocked on literal " << lit
);
3667 if (c
->gate
) cleangate ();
3668 elits
.push (mem
, 0);
3671 for (const int * p
= c
->lits
; (other
= *p
); p
++) {
3672 if (other
== lit
) { found
= true; continue; }
3673 elits
.push (mem
, other
);
3676 elits
.push (mem
, lit
);
3677 elits
.push (mem
, INT_MAX
);
3678 // NOTE: we can not simply turn binary blocked clauses
3679 // into learned clauses, which can be removed without
3680 // any further check in the future, because adding
3681 // resolvents to the CNF (either through learning,
3682 // elimination, dominator clauses etc) may unblock
3683 // clauses. These binary clauses would need to
3684 // be treated differently in all operations that
3685 // remove clauses from the CNF.
3690 bool Solver::trelim (int idx
) {
3693 assert (queue
== trail
);
3694 assert (vars
[idx
].type
== FREE
);
3696 int lit
= 2*idx
, pos
= orgs
[lit
], neg
= orgs
[lit
^1];
3697 if (val (lit
)) return false;
3698 if (opts
.elimgain
<= 1 && (pos
<= 1 || neg
<= 1)) return true;
3699 if (opts
.elimgain
<= 0 && pos
<= 2 && neg
<= 2) return true;
3700 LOG ("trelim " << lit
<< " bound " << elms
[idx
].heat
);
3701 if (gate
) LOG ("actually trelim gate for " << gatepivot
);
3702 for (int sign
= 0; sign
<= 1; sign
++)
3703 for (int i
= 0; i
< orgs
[lit
^sign
]; i
++)
3704 if (orgs
[lit
^sign
][i
]->size
> (unsigned)opts
.elimclim
)
3706 int gain
= pos
+ neg
, l
= opts
.elimgain
, found
, i
, j
;
3709 assert (gatepivot
/2 == lit
/2);
3710 int piv
, s0
, e0
, s1
, e1
;
3712 s0
= 0, e0
= posgate
;
3713 s1
= posgate
, e1
= gate
;
3714 for (i
= s0
; !conflict
&& i
< e0
&& gain
>= l
; i
++) {
3717 for (j
= 0; !conflict
&& gain
>= l
&& j
< orgs
[piv
^1]; j
++) {
3719 if (d
->gate
) continue;
3720 if (resolve (c
, piv
, d
, true)) gain
--, found
++;
3721 if (needtoflush ()) { if (!flush ()) return false; goto RESTART
; }
3722 if (val (piv
)) return false;
3723 if (resotfs
) goto RESTART
;
3724 if (reslimhit
) gain
= INT_MIN
, found
++;
3726 if (opts
.block
&& opts
.blockimpl
&& !found
) { lit
= piv
; goto BLKD
; }
3728 for (i
= s1
; !conflict
&& i
< e1
&& gain
>= l
; i
++) {
3731 for (j
= 0; !conflict
&& gain
>= l
&& j
< orgs
[piv
]; j
++) {
3733 if (d
->gate
) continue;
3734 if (resolve (d
, piv
, c
, true)) gain
--, found
++;
3735 if (needtoflush ()) { if (!flush ()) return false; goto RESTART
; }
3736 if (val (piv
)) return false;
3737 if (resotfs
) goto RESTART
;
3738 if (reslimhit
) gain
= INT_MIN
, found
++;
3740 if (opts
.block
&& opts
.blockimpl
&& !found
) { lit
= 1^piv
; goto BLKD
; }
3743 for (i
= 0; !conflict
&& gain
>= l
&& i
< orgs
[lit
]; i
++) {
3746 for (j
= 0; !conflict
&& gain
>= l
&& j
< orgs
[lit
^1]; j
++) {
3748 if (resolve (c
, lit
, d
, true)) gain
--, found
++;
3749 if (needtoflush ()) { if (!flush ()) return false; goto RESTART
; }
3750 if (val (lit
)) return false;
3751 if (resotfs
) goto RESTART
;
3752 if (reslimhit
) gain
= INT_MIN
, found
++;
3754 if (opts
.block
&& opts
.blockimpl
&& !found
) {
3762 if (conflict
) return false;
3763 LOG ("approximated gain for " << lit
<< " is " << gain
);
3764 if (!val (lit
) && gain
< l
) {
3768 for (int sign
= 0; sign
<= 1; sign
++, lit
^=1) {
3769 if (orgs
[lit
] < 2) goto DONE
;
3770 assert (!val (lit
));
3771 if (orgs
[lit
] <= opts
.elimasym
) {
3772 if (limit
.props
.asym
< 0) goto DONE
;
3773 long long old
= stats
.props
.simp
;
3774 LOG ("trying to eliminate one out of " << orgs
[lit
] <<
3775 " occurences of " << lit
);
3776 for (i
= orgs
[lit
]-1; !conflict
&& i
>= 0; i
--) {
3777 Cls
* c
= orgs
[lit
][i
];
3778 if (c
->gate
) continue;
3780 dbgprint ("LOG trying to eliminate literal from ", c
);
3782 assert (c
->lits
[1]);
3784 bool ok
= bcp (), fl
= true;
3786 for (const int * p
= c
->lits
; ok
&& (other
= *p
); p
++) {
3787 if (val (other
)) continue;
3788 assert (other
!= lit
);
3795 limit
.props
.asym
-= stats
.props
.simp
- old
;
3799 LOG ("asymmetric branching eliminates literal " << lit
);
3800 if (fl
) assign (lit
^1); else remove (lit
, c
);
3801 limit
.props
.asym
+= opts
.elimasymreward
;
3802 if (val (lit
)) goto DONE
;
3803 if (needtoflush ()) {
3804 if (!flush ()) goto DONE
;
3805 if (val (lit
)) goto DONE
;
3808 if (orgs
[lit
] < 2) goto DONE
;
3809 if (orgs
[lit
] == 2 && orgs
[lit
^1] == 2) goto DONE
;
3816 if (conflict
) return false;
3817 if (vals
[lit
]) return false;
3818 if (opts
.elimgain
<= 1 && (orgs
[lit
] <= 1 || orgs
[1^lit
] <= 1))
3820 if (opts
.elimgain
<= 0 && orgs
[lit
] <= 2 && orgs
[1^lit
] <= 2)
3826 void Solver::elim (int idx
) {
3832 assert (queue
== trail
);
3833 assert (vars
[idx
].type
== FREE
);
3834 assert (!vals
[lit
]);
3835 assert (!repr
[lit
]);
3841 LOG ("elim " << lit
);
3842 assert (!vals
[lit
] && !repr
[lit
]);
3845 Cls
** begin
, ** end
;
3849 int neg
= gate
- pos
;
3850 assert (pos
> 0 && neg
> 0);
3851 begin
= gate
.begin ();
3852 if (pos
< neg
) end
= begin
+ posgate
;
3853 else begin
+= posgate
, end
= gate
.end (), slit
^= 1;
3856 int pos
= orgs
[lit
];
3857 int neg
= orgs
[lit
^1];
3858 if (!pos
&& !neg
) zombie (vars
+ idx
);
3859 else if (!pos
) pure (lit
^1);
3860 else if (!neg
) pure (lit
);
3861 if (!pos
|| !neg
) { elimvar
= 0; return; }
3862 if (pos
< neg
) begin
= orgs
[lit
].begin (), end
= orgs
[lit
].end ();
3863 else begin
= orgs
[1^lit
].begin (), end
= orgs
[1^lit
].end (), slit
^= 1;
3865 elits
.push (mem
, 0);
3867 for (Cls
** p
= begin
; p
< end
; p
++) {
3868 elits
.push (mem
, 0);
3872 for (int * p
= c
->lits
; (other
= *p
); p
++) {
3873 if (other
== (slit
)) continue;
3874 assert (other
!= (1^slit
));
3875 elits
.push (mem
, other
);
3876 LOG ("elit " << other
);
3879 elits
.push (mem
, slit
);
3880 LOG ("elit " << slit
);
3881 elits
.push (mem
, 0);
3884 vars
[idx
].type
= ELIM
;
3887 for (int sign
= 0; sign
<= 1; sign
++)
3888 for (int i
= 0; i
< orgs
[lit
^sign
]; i
++) {
3889 Cls
* c
= orgs
[lit
^sign
][i
];
3893 int gatecount
= gate
;
3895 LOG ("actually elim gate for " << gatepivot
);
3896 assert (gatepivot
/2 == lit
/2);
3897 int piv
= gatepivot
;
3898 for (int i
= 0; !conflict
&& i
< posgate
; i
++)
3899 for (int j
= 0; !conflict
&& j
< orgs
[piv
^1]; j
++)
3900 resolve (gate
[i
], piv
, orgs
[piv
^1][j
], false);
3901 for (int i
= posgate
; !conflict
&& i
< gate
; i
++)
3902 for (int j
= 0; !conflict
&& j
< orgs
[piv
]; j
++)
3903 resolve (orgs
[piv
][j
], piv
, gate
[i
], false);
3905 for (int i
= 0; !conflict
&& i
< orgs
[lit
]; i
++)
3906 for (int j
= 0; !conflict
&& j
< orgs
[lit
^1]; j
++)
3907 resolve (orgs
[lit
][i
], lit
, orgs
[lit
^1][j
], false);
3910 for (int sign
= 0; sign
<= 1; sign
++)
3911 for (int i
= 0; i
< orgs
[lit
^sign
]; i
++)
3912 orgs
[lit
^sign
][i
]->dirty
= false;
3914 assert (gate
== gatecount
);
3915 cleangate (), cleantrash ();
3917 for (int sign
= 0; sign
<= 1; sign
++)
3923 inline long long Solver::clauses () const {
3924 return stats
.clauses
.orig
+ stats
.clauses
.lnd
+ stats
.clauses
.bin
;
3927 inline bool Solver::hasgate (int idx
) {
3928 assert (0 < idx
&& idx
<= maxvar
);
3931 if (andgate (lit
)) return true;
3932 if (andgate (1^lit
)) return true;
3933 if (xorgate (lit
)) return true;
3934 if (itegate (lit
)) return true;
3938 void Solver::cleans () {
3940 assert (elimode
|| blkmode
);
3942 for (int i
= 0; i
<= 3 + (int)opts
.glue
; i
++) {
3944 if (i
== 0) p
= binary
.head
;
3945 if (i
== 1) p
= original
.head
;
3946 if (i
== 2) p
= fresh
.head
;
3947 if (i
>= 3) p
= learned
[i
-3].head
;
3949 assert (!p
->locked
); assert (!p
->garbage
);
3950 Cls
* prev
= p
->prev
;
3952 for (int * q
= p
->lits
; (other
= *q
); q
++) {
3953 Var
* v
= vars
+ (other
/2);
3954 if (v
->type
== FREE
) continue;
3955 if (v
->type
== FIXED
) continue;
3958 if (other
) { /*assert (p->lnd);*/ p
->garbage
= true; }
3964 void Solver::elim () {
3965 if (!eliminating ()) return;
3966 stats
.elim
.phases
++;
3975 connect (binary
, true);
3976 connect (original
, true);
3977 if (!flush ()) return;
3978 int repcounter
= 111;
3980 limit
.budget
.bw
.sub
= limit
.budget
.fw
.sub
= opts
.elimint
;
3981 limit
.budget
.bw
.str
= limit
.budget
.fw
.str
= opts
.elimint
;
3982 if (opts
.rtc
== 2 || opts
.elimrtc
== 2 ||
3983 ((opts
.rtc
== 1 || opts
.elimrtc
== 1) && !stats
.elim
.rounds
))
3986 bound
= stats
.elim
.resolutions
+ opts
.elimint
;
3987 for (int i
= stats
.elim
.phases
; i
<= opts
.elimboost
; i
++)
3988 bound
+= opts
.elimint
;
3990 limit
.props
.asym
= opts
.elimasymint
;
3991 if (schedule
.elim
) {
3992 for (int idx
= 1; idx
<= maxvar
; idx
++) {
3993 int lit
= 2*idx
, pos
= orgs
[lit
], neg
= orgs
[lit
^1];
3994 if (pos
<= 2 || neg
<= 2 || schedule
.elim
.contains (elms
+ idx
))
3998 for (int idx
= 1; idx
<= maxvar
; idx
++) touch (2*idx
);
4002 while (!conflict
&& schedule
.elim
) {
4003 Rnk
* e
= schedule
.elim
.max ();
4004 int idx
= e
- elms
, lit
= 2*idx
, pos
= orgs
[lit
], neg
= orgs
[1^lit
];
4005 if (pos
> 1 && neg
> 1 && (pos
> 2 || neg
> 2))
4006 if (stats
.elim
.resolutions
> bound
) break;
4007 if (!--repcounter
) {
4008 if (terminal
) report (2, 'e');
4011 (void) schedule
.elim
.pop ();
4012 Var
* v
= vars
+ idx
;
4013 if (v
->type
!= FREE
) continue;
4014 if (!pos
&& !neg
) zombie (vars
+ idx
);
4015 else if (!pos
) pure (lit
^1);
4016 else if (!neg
) pure (lit
);
4018 if (hasgate (idx
)) assert (gatestats
), checkgate ();
4019 bool eliminate
= trelim (idx
);
4020 if (needtoflush () && !flush ()) break;
4021 if (!eliminate
|| vals
[lit
]) { cleangate (); continue; }
4023 gatestats
->count
+= 1;
4024 gatestats
->len
+= gatelen
;
4028 if (needtoflush () && !flush ()) break;
4029 if (bound
!= LLONG_MAX
) bound
+= opts
.elimreward
;
4036 for (int idx
= 1; !conflict
&& idx
<= maxvar
; idx
++) {
4037 if (vars
[idx
].type
!= FREE
) continue;
4038 if (elms
[idx
].pos
== -1) continue;
4039 int lit
= 2*idx
, pos
= orgs
[lit
], neg
= orgs
[lit
+1];
4042 assert (pos
!= 2 || neg
!= 2);
4046 if (conflict
) return;
4051 if (bound
!= LLONG_MAX
) pure ();
4060 if (!schedule
.elim
) {
4061 stats
.elim
.rounds
++;
4062 limit
.fixed
.elim
= remvars ();
4064 limit
.props
.elim
= opts
.elimprd
;
4065 limit
.props
.elim
*= opts
.elimint
;
4066 limit
.props
.elim
+= stats
.props
.srch
;
4070 void Solver::zombie (Var
* v
) {
4071 assert (elimode
|| blkmode
);
4073 assert (v
->type
== FREE
);
4074 int idx
= v
- vars
, lit
= 2*idx
;
4075 assert (!val (lit
));
4076 assert (!orgs
[lit
]);
4077 assert (!orgs
[lit
^1]);
4078 assert (!repr
[lit
]);
4080 LOG ("explicit zombie literal " << lit
);
4081 stats
.zombies
.expl
++;
4082 } else if (blkmode
) {
4083 LOG ("blocking zombie literal " << lit
);
4084 stats
.zombies
.blkd
++;
4087 LOG ("eliminating zombie literal " << lit
);
4088 stats
.zombies
.elim
++;
4090 stats
.vars
.zombies
++;
4092 assume (lit
, false);
4099 void Solver::pure (int lit
) {
4100 assert (elimode
|| blkmode
);
4102 assert (!val (lit
));
4103 assert (!orgs
[lit
^1]);
4104 assert (!repr
[lit
]);
4105 Var
* v
= vars
+ (lit
/2);
4106 assert (v
->type
== FREE
);
4108 LOG ("explicit pure literal " << lit
);
4110 } else if (blkmode
) {
4111 LOG ("blocking pure literal " << lit
);
4115 LOG ("eliminating pure literal " << lit
);
4120 assume (lit
, false);
4125 void Solver::block () {
4126 if (!blocking ()) return;
4127 stats
.blkd
.phases
++;
4133 connect (binary
, true);
4134 connect (original
, true);
4135 if (!flush ()) return;
4136 int repcounter
= 111;
4138 if (opts
.rtc
== 2 || opts
.blockrtc
== 2 ||
4139 ((opts
.rtc
== 1 || opts
.blockrtc
== 1) && !stats
.blkd
.rounds
)) {
4142 bound
= stats
.blkd
.resolutions
+ opts
.blockint
;
4143 for (int i
= stats
.blkd
.phases
; i
<= opts
.blockboost
; i
++)
4144 bound
+= opts
.blockint
;
4146 if (schedule
.block
) {
4147 for (int lit
= 2; lit
<= 2*maxvar
+1; lit
++)
4148 if (schedule
.block
.contains (blks
+ lit
)) touchblkd (lit
);
4150 for (int lit
= 2; lit
<= 2*maxvar
+1; lit
++) touchblkd (lit
);
4154 while (!conflict
&& schedule
.block
&& stats
.blkd
.resolutions
<= bound
) {
4155 Rnk
* b
= schedule
.block
.pop ();
4157 if (!repcounter
--) {
4158 if (terminal
) report (2, 'k');
4162 Var
* v
= vars
+ (lit
/2);
4163 if (v
->type
!= FREE
) continue;
4164 int pos
= orgs
[lit
], neg
= orgs
[1^lit
];
4165 if (!pos
&& !neg
) zombie (v
);
4166 else if (!pos
) pure (1^lit
);
4167 else if (!neg
) pure (lit
);
4168 else if (orgs
[lit
] <= opts
.blkmaxlen
|| orgs
[1^lit
] <= opts
.blkmaxlen
) {
4169 assert (!val (lit
));
4170 if (orgs
[1^lit
] > opts
.blkmaxlen
) continue;
4171 LOG ("tryblk " << lit
);
4172 for (int i
= orgs
[lit
]-1; !conflict
&& i
>= 0; i
--) {
4173 Cls
* c
= orgs
[lit
][i
];
4174 bool blocked
= true;
4175 for (int j
= 0; !conflict
&& blocked
&& j
< orgs
[lit
^1]; j
++) {
4176 blocked
= !resolve (c
, lit
, orgs
[lit
^1][j
], true);
4177 if (needtoflush ()) { if (!flush ()) goto DONE
; goto RESTART
; }
4178 if (blocked
&& resotfs
) goto RESTART
;
4180 if (!blocked
) continue;
4181 if (conflict
) break;
4182 if (val (lit
)) break;
4185 if (bound
!= LLONG_MAX
) bound
+= opts
.blockreward
;
4191 if (conflict
) return;
4192 assert (schedule
.block
|| stats
.clauses
.irr
!= 1);
4193 if (bound
!= LLONG_MAX
) pure ();
4199 if (!schedule
.block
) {
4200 stats
.blkd
.rounds
++;
4201 limit
.fixed
.block
= remvars ();
4203 limit
.props
.block
= opts
.blockprd
;
4204 limit
.props
.block
*= opts
.blockint
;
4205 limit
.props
.block
+= stats
.props
.srch
;
4209 void Solver::pure () {
4211 assert (blkmode
|| elimode
);
4213 if (!flush ()) return;
4217 for (int idx
= 1; idx
<= maxvar
; idx
++) {
4218 Var
* v
= vars
+ idx
;
4219 assert (!v
->onplits
);
4220 if (v
->type
!= FREE
) continue;
4221 plits
.push (mem
, idx
);
4225 int idx
= plits
.pop (), lit
= 2*idx
;
4226 Var
* v
= vars
+ idx
;
4227 assert (v
->type
== FREE
);
4228 assert (v
->onplits
);
4229 if (!orgs
[lit
] && !orgs
[lit
^1]) zombie (v
);
4230 else if (!orgs
[lit
]) pure (1^lit
);
4231 else if (!orgs
[1^lit
]) pure (lit
);
4238 void Solver::jwh () {
4239 memset (jwhs
, 0, 2 * (maxvar
+ 1) * sizeof *jwhs
);
4240 for (Cls
* p
= original
.head
; p
; p
= p
->prev
) jwh (p
);
4241 for (Cls
* p
= binary
.head
; p
; p
= p
->prev
) jwh (p
);
4242 for (Cls
* p
= fresh
.head
; p
; p
= p
->prev
) jwh (p
);
4243 for (int glue
= 0; glue
<= opts
.glue
; glue
++)
4244 for (Cls
* p
= learned
[glue
].head
; p
; p
= p
->prev
) jwh (p
);
4247 void Solver::initfresh () {
4248 limit
.reduce
.fresh
= (opts
.fresh
* limit
.reduce
.learned
+ 99) / 100;
4252 void Solver::initreduce () {
4254 if (opts
.liminitmode
) l
= (opts
.liminitpercent
*stats
.clauses
.orig
+ 99)/100;
4255 else l
= opts
.liminitconst
;
4256 if (l
> opts
.liminitmax
) l
= opts
.liminitmax
;
4257 if (l
> opts
.maxlimit
) l
= opts
.maxlimit
;
4258 if (l
< opts
.minlimit
) l
= opts
.minlimit
;
4259 limit
.enlarge
.conflicts
= limit
.enlarge
.inc
= limit
.enlarge
.init
= l
;
4260 limit
.reduce
.learned
= limit
.reduce
.init
= l
;
4265 void Solver::enlarge () {
4267 if (opts
.limincmode
) {
4268 limit
.reduce
.learned
=
4269 ((100 + opts
.limincpercent
) * limit
.reduce
.learned
+ 99) / 100;
4270 limit
.enlarge
.inc
= ((100 + opts
.enlinc
) * limit
.enlarge
.inc
+ 99) / 100;
4271 limit
.enlarge
.conflicts
= stats
.conflicts
+ limit
.enlarge
.inc
;
4273 limit
.enlarge
.inc
+= opts
.liminconst1
;
4274 limit
.enlarge
.conflicts
+= limit
.enlarge
.inc
;
4275 limit
.reduce
.learned
+= opts
.liminconst2
;
4277 if (limit
.reduce
.learned
> opts
.maxlimit
) {
4278 limit
.reduce
.learned
= opts
.maxlimit
;
4279 limit
.enlarge
.conflicts
= INT_MAX
;
4285 void Solver::shrink (int old
) {
4286 if (!opts
.shrink
) return;
4287 if (limit
.reduce
.learned
<= opts
.minlimit
) return;
4289 int now
= stats
.clauses
.orig
;
4291 old
/= 100, now
/= 100;
4292 if (old
<= now
) return;
4295 int red
= (100 * (old
- now
)) / old
;
4296 assert (red
<= 100);
4299 int rl
= limit
.reduce
.learned
, drl
;
4300 drl
= (opts
.shrink
< 2) ? limit
.reduce
.init
: rl
;
4301 drl
*= (opts
.shrinkfactor
*red
+99)/100;
4303 if (rl
< opts
.minlimit
) rl
= opts
.minlimit
;
4304 if (limit
.reduce
.learned
== rl
) return;
4306 limit
.reduce
.learned
= rl
;
4313 void Solver::simplify () {
4315 int old
= stats
.clauses
.orig
, inc
, rv
;
4320 if (conflict
) goto DONE
;
4322 if (conflict
) goto DONE
;
4324 if (conflict
) goto DONE
;
4326 if (conflict
) goto DONE
;
4328 ((opts
.rtc
== 2 || opts
.simprtc
== 2) ||
4329 ((opts
.rtc
== 1 || opts
.simprtc
== 1) && !stats
.simps
)))
4332 limit
.props
.simp
= stats
.props
.srch
+ simprd
* clauses ();
4333 limit
.simp
= stats
.vars
.fixed
+ stats
.vars
.merged
;
4334 limit
.fixed
.simp
= stats
.vars
.fixed
;
4337 if (rv
) while (rv
< 1000000) rv
*= 10, inc
/= 2;
4338 simprd
*= 100 + inc
; simprd
+= 99; simprd
/= 100;
4340 if (!stats
.simps
) initreduce ();
4343 if (opts
.print
) print ();
4348 void Solver::flushunits () {
4351 while (units
&& !conflict
) unit (units
.pop ());
4355 void Solver::initrestart () {
4357 limit
.restart
.conflicts
= stats
.conflicts
;
4358 if (opts
.luby
) delta
= opts
.restartint
* luby (limit
.restart
.lcnt
= 1);
4359 else delta
= limit
.restart
.inner
= limit
.restart
.outer
= opts
.restartint
;
4360 limit
.restart
.conflicts
+= delta
;
4363 void Solver::initbias () {
4365 limit
.rebias
.conflicts
= opts
.rebiasint
* luby (limit
.rebias
.lcnt
= 1);
4366 limit
.rebias
.conflicts
+= stats
.conflicts
;
4369 void Solver::iteration () {
4372 assert (limit
.fixed
.iter
< trail
);
4375 int old
= stats
.clauses
.orig
;
4376 while (limit
.fixed
.iter
< trail
) {
4377 int lit
= trail
[limit
.fixed
.iter
++];
4385 inline bool Solver::reducing () const {
4386 int learned_not_locked
= stats
.clauses
.lnd
;
4387 learned_not_locked
-= stats
.clauses
.lckd
;
4388 return 2 * learned_not_locked
> 3 * limit
.reduce
.learned
;
4391 inline bool Solver::eliminating () const {
4392 if (!opts
.elim
) return false;
4393 if (!stats
.elim
.phases
) return true;
4394 if (opts
.rtc
== 2 || opts
.simprtc
== 2 ||
4395 ((opts
.rtc
== 1 || opts
.simprtc
== 1) && !stats
.simps
)) return true;
4396 if (schedule
.elim
) return true;
4397 if (stats
.props
.srch
<= limit
.props
.elim
) return false;
4398 return remvars () < limit
.fixed
.elim
;
4401 inline bool Solver::blocking () const {
4402 if (!opts
.block
) return false;
4403 if (!stats
.elim
.phases
) return true;
4404 if (opts
.rtc
== 2 || opts
.simprtc
== 2 ||
4405 ((opts
.rtc
== 1 || opts
.simprtc
== 1) && !stats
.simps
)) return true;
4406 if (schedule
.block
) return true;
4407 if (stats
.props
.srch
<= limit
.props
.block
) return false;
4408 return remvars () < limit
.fixed
.block
;
4411 inline bool Solver::simplifying () const {
4412 if (!stats
.simps
) return true;
4413 if (stats
.props
.srch
< limit
.props
.simp
) return false;
4414 return limit
.simp
< stats
.vars
.fixed
+ stats
.vars
.merged
;
4417 inline bool Solver::restarting () const {
4418 return level
>= 2 && limit
.restart
.conflicts
<= stats
.conflicts
;
4421 inline bool Solver::rebiasing () const {
4422 return limit
.rebias
.conflicts
<= stats
.conflicts
;
4425 inline bool Solver::probing () const {
4426 if (!opts
.probe
) return false;
4427 if (stats
.props
.srch
< limit
.props
.probe
) return false;
4428 if (!level
) return true;
4429 if (schedule
.probe
) return true;
4430 return limit
.fixed
.probe
< stats
.vars
.fixed
;
4433 inline bool Solver::enlarging () const {
4434 if (limit
.reduce
.learned
>= opts
.maxlimit
) return false;
4435 return stats
.conflicts
>= limit
.enlarge
.conflicts
;
4438 inline bool Solver::exhausted () const {
4439 return stats
.decisions
>= limit
.decisions
;
4442 int Solver::search () {
4443 stats
.entered2
= seconds ();
4445 if (!bcp ()) { if (!analyze ()) return -1; }
4446 else if (iterating
) iteration ();
4447 else if (units
) flushunits ();
4448 else if (probing ()) probe ();
4449 else if (simplifying ()) simplify ();
4450 else if (rebiasing ()) rebias ();
4451 else if (restarting ()) restart ();
4452 else if (reducing ()) reduce ();
4453 else if (enlarging ()) enlarge ();
4454 else if (exhausted ()) return 0;
4455 else if (!decide ()) return 1;
4456 stats
.srchtime
+= seconds () - stats
.entered2
;
4459 void Solver::initlimit (int decision_limit
) {
4460 memset (&limit
, 0, sizeof limit
);
4461 limit
.decisions
= decision_limit
;
4462 simprd
= opts
.simprd
;
4463 rng
.init (opts
.seed
);
4466 void Solver::initsearch (int decision_limit
) {
4467 assert (opts
.fixed
);
4468 initlimit (decision_limit
);
4474 int Solver::solve (int decision_limit
) {
4475 initsearch (decision_limit
);
4476 int res
= search ();
4477 report (1, res
< 0 ? '0' : (res
? '1' : '?'));
4478 if (!stats
.simps
&& opts
.print
) print ();
4482 double Stats::now () {
4484 if (getrusage (RUSAGE_SELF
, &u
))
4486 double res
= u
.ru_utime
.tv_sec
+ 1e-6 * u
.ru_utime
.tv_usec
;
4487 res
+= u
.ru_stime
.tv_sec
+ 1e-6 * u
.ru_stime
.tv_usec
;
4491 double Stats::seconds () {
4492 double t
= now (), delta
= t
- entered
;
4493 delta
= (delta
< 0) ? 0 : delta
;
4499 void Stats::sw2srch () {
4500 double t
= seconds ();
4501 simptime
+= t
- entered2
;
4505 void Stats::sw2simp () {
4506 double t
= seconds ();
4507 srchtime
+= t
- entered2
;
4512 memset (this, 0, sizeof *this);
4517 memset (this, 0, sizeof *this);
4518 budget
.fw
.sub
= budget
.bw
.sub
= budget
.bw
.str
= budget
.fw
.str
= 10000;
4521 void PrecoSat::die (const char * msg
, ...) {
4523 fprintf (stdout
, "c\nc\nc ");
4525 vfprintf (stdout
, msg
, ap
);
4527 fputs ("\nc\nc\n", stdout
);
4532 void Solver::print () {
4536 file
= fopen (opts
.output
, "w");
4537 if (!file
) die ("can not write '%s'", opts
.output
);
4539 } else file
= stdout
, close_file
= false;
4544 if (conflict
) fprintf (file
, "p cnf 0 1\n0\n"), m
=0, n
=1;
4546 size_t bytes
= 2*(maxvar
+1) * sizeof (int);
4547 int * map
= (int*) mem
.callocate (bytes
);
4549 for (int idx
= 1; idx
<= maxvar
; idx
++)
4550 if (vars
[idx
].type
== FREE
) map
[idx
] = ++m
;
4552 assert (m
== remvars ());
4555 for (int i
= 0; i
<= 1; i
++)
4556 for (Cls
* p
= (i
? original
: binary
).tail
; p
; p
= p
->next
)
4557 if (!p
->lnd
&& !satisfied (p
)) n
++;
4559 fprintf (file
, "p cnf %d %d\n", m
, n
);
4562 for (int i
= 0; i
<= 1; i
++)
4563 for (Cls
* p
= (i
? binary
: original
).tail
; p
; p
= p
->next
) {
4564 if (p
->lnd
) continue;
4565 if (satisfied (p
)) continue;
4567 for (int * q
= p
->lits
; (lit
= *q
); q
++) {
4568 Val tmp
= val (lit
);
4569 if (tmp
< 0) continue;
4571 int ilit
= map
[lit
/2];
4572 if (lit
&1) ilit
= -ilit
;
4573 fprintf (file
, "%d ", ilit
);
4575 fputs ("0\n", file
);
4577 mem
.deallocate (map
, bytes
);
4579 if (close_file
) fclose (file
);
4584 void Cls::print (const char * prefix
) const {
4585 fputs (prefix
, stdout
);
4586 for (const int * p
= lits
; *p
; p
++) {
4587 if (p
!= lits
) fputc (' ', stdout
);
4590 fputc ('\n', stdout
);
4593 void Solver::dbgprint (const char * type
, Anchor
<Cls
>& anchor
) {
4594 size_t len
= strlen (type
) + strlen (prfx
) + 80;
4595 char * str
= (char*) mem
.allocate (len
);
4596 sprintf (str
, "%sPRINT %s clause ", prfx
, type
);
4597 for (Cls
* p
= anchor
.tail
; p
; p
= p
->next
) p
->print (str
);
4598 mem
.deallocate (str
, len
);
4601 void Solver::dbgprint (const char * type
, Cls
* cls
) {
4602 size_t len
= strlen (type
) + strlen (prfx
) + 1;
4603 char * str
= (char*) mem
.allocate (len
);
4604 sprintf (str
, "%s%s", prfx
, type
);
4606 mem
.deallocate (str
, len
);
4609 void Solver::dbgprint () {
4610 dbgprint ("binary", binary
);
4611 dbgprint ("original", original
);
4612 for (int glue
= 0; glue
<= opts
.glue
; glue
++) {
4614 sprintf (buffer
, "learned[%u]", glue
);
4615 dbgprint (buffer
, learned
[glue
]);
4617 dbgprint ("fresh", fresh
);
4620 void Solver::dbgprintgate () {
4621 for (Cls
** p
= gate
.begin(); p
< gate
.end (); p
++) {
4622 printf ("%sLOG gate clause", prfx
);
4624 for (const int * q
= c
->lits
; *q
; q
++)