1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50 package org.sat4j.minisat.core;
51
52 import static org.sat4j.core.LiteralsUtils.var;
53 import static org.sat4j.core.LiteralsUtils.toDimacs;
54
55 import java.io.PrintStream;
56 import java.io.PrintWriter;
57 import java.io.Serializable;
58 import java.lang.reflect.Field;
59 import java.util.Comparator;
60 import java.util.HashMap;
61 import java.util.Iterator;
62 import java.util.Map;
63 import java.util.Timer;
64 import java.util.TimerTask;
65
66 import org.sat4j.core.Vec;
67 import org.sat4j.core.VecInt;
68 import org.sat4j.specs.ContradictionException;
69 import org.sat4j.specs.IConstr;
70 import org.sat4j.specs.ISolver;
71 import org.sat4j.specs.IVec;
72 import org.sat4j.specs.IVecInt;
73 import org.sat4j.specs.IteratorInt;
74 import org.sat4j.specs.TimeoutException;
75
76
77
78
79
80
81
82 public class Solver<L extends ILits, D extends DataStructureFactory<L>>
83 implements ISolver, UnitPropagationListener, ActivityListener, Learner {
84
85 private static final long serialVersionUID = 1L;
86
87 private static final double CLAUSE_RESCALE_FACTOR = 1e-20;
88
89 private static final double CLAUSE_RESCALE_BOUND = 1 / CLAUSE_RESCALE_FACTOR;
90
91
92
93
94 private final IVec<Constr> constrs = new Vec<Constr>();
95
96
97
98
99 private final IVec<Constr> learnts = new Vec<Constr>();
100
101
102
103
104 private double claInc = 1.0;
105
106
107
108
109 private double claDecay = 1.0;
110
111
112
113
114
115
116 private int qhead = 0;
117
118
119
120
121
122
123 protected final IVecInt trail = new VecInt();
124
125
126
127
128
129
130 protected final IVecInt trailLim = new VecInt();
131
132
133
134
135
136
137 protected int rootLevel;
138
139 private int[] model = null;
140
141 protected L voc;
142
143 private IOrder<L> order;
144
145 private final ActivityComparator comparator = new ActivityComparator();
146
147 private final SolverStats stats = new SolverStats();
148
149 private final LearningStrategy<L, D> learner;
150
151 protected final AssertingClauseGenerator analyzer;
152
153 private volatile boolean undertimeout;
154
155 private long timeout = Integer.MAX_VALUE;
156
157 private boolean timeBasedTimeout = true;
158
159 protected D dsfactory;
160
161 private SearchParams params;
162
163 private final IVecInt __dimacs_out = new VecInt();
164
165 private SearchListener slistener = new NullSearchListener();
166
167 private RestartStrategy restarter;
168
169 private final Map<String, Counter> constrTypes = new HashMap<String, Counter>();
170
171 private boolean isDBSimplificationAllowed = false;
172
173 private int learnedLiterals = 0;
174
175 protected IVecInt dimacs2internal(IVecInt in) {
176
177
178
179
180
181 __dimacs_out.clear();
182 __dimacs_out.ensure(in.size());
183 for (int i = 0; i < in.size(); i++) {
184 assert (in.get(i) != 0);
185 __dimacs_out.unsafePush(voc.getFromPool(in.get(i)));
186 }
187 return __dimacs_out;
188 }
189
190
191
192
193
194
195
196
197
198
199 public Solver(AssertingClauseGenerator acg, LearningStrategy<L, D> learner,
200 D dsf, IOrder<L> order, RestartStrategy restarter) {
201 this(acg, learner, dsf, new SearchParams(), order, restarter);
202 }
203
204 public Solver(AssertingClauseGenerator acg, LearningStrategy<L, D> learner,
205 D dsf, SearchParams params, IOrder<L> order,
206 RestartStrategy restarter) {
207 analyzer = acg;
208 this.learner = learner;
209 this.order = order;
210 this.params = params;
211 setDataStructureFactory(dsf);
212 this.restarter = restarter;
213 }
214
215
216
217
218
219
220
221
222 public final void setDataStructureFactory(D dsf) {
223 dsfactory = dsf;
224 dsfactory.setUnitPropagationListener(this);
225 dsfactory.setLearner(this);
226 voc = dsf.getVocabulary();
227 order.setLits(voc);
228 }
229
230 public void setSearchListener(SearchListener sl) {
231 slistener = sl;
232 }
233
234 public void setTimeout(int t) {
235 timeout = t * 1000L;
236 timeBasedTimeout = true;
237 }
238
239 public void setTimeoutMs(long t) {
240 timeout = t;
241 timeBasedTimeout = true;
242 }
243
244 public void setTimeoutOnConflicts(int count) {
245 timeout = count;
246 timeBasedTimeout = false;
247 }
248
249 public void setSearchParams(SearchParams sp) {
250 params = sp;
251 }
252
253 public void setRestartStrategy(RestartStrategy restarter) {
254 this.restarter = restarter;
255 }
256
257 public void expireTimeout() {
258 undertimeout = false;
259 }
260
261 protected int nAssigns() {
262 return trail.size();
263 }
264
265 public int nConstraints() {
266 return constrs.size() + trail.size() - learnedLiterals;
267 }
268
269 public void learn(Constr c) {
270 learnts.push(c);
271 c.setLearnt();
272 c.register();
273 stats.learnedclauses++;
274 switch (c.size()) {
275 case 2:
276 stats.learnedbinaryclauses++;
277 break;
278 case 3:
279 stats.learnedternaryclauses++;
280 break;
281 default:
282
283 }
284 }
285
286 public int decisionLevel() {
287 return trailLim.size();
288 }
289
290 @Deprecated
291 public int newVar() {
292 int index = voc.nVars() + 1;
293 voc.ensurePool(index);
294 return index;
295 }
296
297 public int newVar(int howmany) {
298 voc.ensurePool(howmany);
299 return voc.nVars();
300 }
301
302 public IConstr addClause(IVecInt literals) throws ContradictionException {
303 IVecInt vlits = dimacs2internal(literals);
304 return addConstr(dsfactory.createClause(vlits));
305 }
306
307 public boolean removeConstr(IConstr co) {
308 if (co == null) {
309 throw new IllegalArgumentException(
310 "Reference to the constraint to remove needed!");
311 }
312 Constr c = (Constr) co;
313 c.remove();
314 constrs.remove(c);
315 clearLearntClauses();
316 cancelLearntLiterals();
317 return true;
318 }
319
320 public void addAllClauses(IVec<IVecInt> clauses)
321 throws ContradictionException {
322 for (Iterator<IVecInt> iterator = clauses.iterator(); iterator
323 .hasNext();) {
324 addClause(iterator.next());
325 }
326 }
327
328 public IConstr addAtMost(IVecInt literals, int degree)
329 throws ContradictionException {
330 int n = literals.size();
331 IVecInt opliterals = new VecInt(n);
332 for (IteratorInt iterator = literals.iterator(); iterator.hasNext();) {
333 opliterals.push(-iterator.next());
334 }
335 return addAtLeast(opliterals, n - degree);
336 }
337
338 public IConstr addAtLeast(IVecInt literals, int degree)
339 throws ContradictionException {
340 IVecInt vlits = dimacs2internal(literals);
341 return addConstr(dsfactory.createCardinalityConstraint(vlits, degree));
342 }
343
344 @SuppressWarnings("unchecked")
345 public boolean simplifyDB() {
346
347
348
349
350
351
352
353
354 IVec<Constr>[] cs = new IVec[] { constrs, learnts };
355 for (int type = 0; type < 2; type++) {
356 int j = 0;
357 for (int i = 0; i < cs[type].size(); i++) {
358 if (cs[type].get(i).simplify()) {
359
360 cs[type].get(i).remove();
361 } else {
362 cs[type].moveTo(j++, i);
363 }
364 }
365 cs[type].shrinkTo(j);
366 }
367 return true;
368 }
369
370
371
372
373
374
375 public int[] model() {
376 if (model == null) {
377 throw new UnsupportedOperationException(
378 "Call the solve method first!!!");
379 }
380 int[] nmodel = new int[model.length];
381 System.arraycopy(model, 0, nmodel, 0, model.length);
382 return nmodel;
383 }
384
385
386
387
388
389
390
391
392 public boolean enqueue(int p) {
393 return enqueue(p, null);
394 }
395
396
397
398
399
400
401
402
403
404
405
406 public boolean enqueue(int p, Constr from) {
407 assert p > 1;
408 if (voc.isSatisfied(p)) {
409
410 return true;
411 }
412 if (voc.isFalsified(p)) {
413
414 return false;
415 }
416
417 voc.satisfies(p);
418 voc.setLevel(p, decisionLevel());
419 voc.setReason(p, from);
420 trail.push(p);
421 return true;
422 }
423
424 private boolean[] mseen = new boolean[0];
425
426 private final IVecInt preason = new VecInt();
427
428 private final IVecInt outLearnt = new VecInt();
429
430 public void analyze(Constr confl, Pair results) {
431 assert confl != null;
432 outLearnt.clear();
433
434 final boolean[] seen = mseen;
435
436 assert outLearnt.size() == 0;
437 for (int i = 0; i < seen.length; i++) {
438 seen[i] = false;
439 }
440
441 analyzer.initAnalyze();
442 int p = ILits.UNDEFINED;
443
444 outLearnt.push(ILits.UNDEFINED);
445
446 int outBtlevel = 0;
447
448 do {
449 preason.clear();
450 assert confl != null;
451 confl.calcReason(p, preason);
452 if (confl.learnt())
453 claBumpActivity(confl);
454
455 for (int j = 0; j < preason.size(); j++) {
456 int q = preason.get(j);
457 order.updateVar(q);
458 if (!seen[q >> 1]) {
459
460 seen[q >> 1] = true;
461 if (voc.getLevel(q) == decisionLevel()) {
462 analyzer.onCurrentDecisionLevelLiteral(q);
463 } else if (voc.getLevel(q) > 0) {
464
465 outLearnt.push(q ^ 1);
466 outBtlevel = Math.max(outBtlevel, voc.getLevel(q));
467 }
468 }
469 }
470
471
472 do {
473 p = trail.last();
474 confl = voc.getReason(p);
475 undoOne();
476 } while (!seen[p >> 1]);
477
478
479 } while (analyzer.clauseNonAssertive(confl));
480
481 outLearnt.set(0, p ^ 1);
482 simplifier.simplify(outLearnt);
483
484 Constr c = dsfactory.createUnregisteredClause(outLearnt);
485 slistener.learn(c);
486
487 results.reason = c;
488
489 assert outBtlevel > -1;
490 results.backtrackLevel = outBtlevel;
491 }
492
493 interface ISimplifier extends Serializable {
494 void simplify(IVecInt outLearnt);
495 }
496
497 public static final ISimplifier NO_SIMPLIFICATION = new ISimplifier() {
498
499
500
501 private static final long serialVersionUID = 1L;
502
503 public void simplify(IVecInt outLearnt) {
504 }
505
506 @Override
507 public String toString() {
508 return "No reason simplification";
509 }
510 };
511
512 public final ISimplifier SIMPLE_SIMPLIFICATION = new ISimplifier() {
513
514
515
516 private static final long serialVersionUID = 1L;
517
518 public void simplify(IVecInt conflictToReduce) {
519 simpleSimplification(conflictToReduce);
520 }
521
522 @Override
523 public String toString() {
524 return "Simple reason simplification";
525 }
526 };
527
528 public final ISimplifier EXPENSIVE_SIMPLIFICATION = new ISimplifier() {
529
530
531
532
533 private static final long serialVersionUID = 1L;
534
535 public void simplify(IVecInt conflictToReduce) {
536 expensiveSimplification(conflictToReduce);
537 }
538
539 @Override
540 public String toString() {
541 return "Expensive reason simplification";
542 }
543 };
544
545 private ISimplifier simplifier = NO_SIMPLIFICATION;
546
547
548
549
550
551
552
553
554
555
556 public void setSimplifier(String simp) {
557 Field f;
558 try {
559 f = Solver.class.getDeclaredField(simp);
560 simplifier = (ISimplifier) f.get(this);
561 } catch (Exception e) {
562 e.printStackTrace();
563 simplifier = NO_SIMPLIFICATION;
564 }
565 }
566
567
568
569
570
571
572
573
574
575
576 public void setSimplifier(ISimplifier simp) {
577 simplifier = simp;
578 }
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602 private void simpleSimplification(IVecInt conflictToReduce) {
603 int i, j;
604 final boolean[] seen = mseen;
605 for (i = j = 1; i < conflictToReduce.size(); i++) {
606 IConstr r = voc.getReason(conflictToReduce.get(i));
607 if (r == null) {
608 conflictToReduce.moveTo(j++, i);
609 } else {
610 for (int k = 0; k < r.size(); k++)
611 if (voc.isFalsified(r.get(k)) && !seen[r.get(k) >> 1]
612 && (voc.getLevel(r.get(k)) != 0)) {
613 conflictToReduce.moveTo(j++, i);
614 break;
615 }
616 }
617 }
618 conflictToReduce.shrink(i - j);
619 stats.reducedliterals += (i - j);
620 }
621
622 private final IVecInt analyzetoclear = new VecInt();
623
624 private final IVecInt analyzestack = new VecInt();
625
626
627 private void expensiveSimplification(IVecInt conflictToReduce) {
628
629
630 int i, j;
631
632 analyzetoclear.clear();
633 conflictToReduce.copyTo(analyzetoclear);
634 for (i = 1, j = 1; i < conflictToReduce.size(); i++)
635 if (voc.getReason(conflictToReduce.get(i)) == null
636 || !analyzeRemovable(conflictToReduce.get(i)))
637 conflictToReduce.moveTo(j++, i);
638 conflictToReduce.shrink(i - j);
639 stats.reducedliterals += (i - j);
640 }
641
642
643
644
645 private boolean analyzeRemovable(int p) {
646 assert voc.getReason(p) != null;
647 analyzestack.clear();
648 analyzestack.push(p);
649 final boolean[] seen = mseen;
650 int top = analyzetoclear.size();
651 while (analyzestack.size() > 0) {
652 int q = analyzestack.last();
653 assert voc.getReason(q) != null;
654 Constr c = voc.getReason(q);
655 analyzestack.pop();
656 for (int i = 0; i < c.size(); i++) {
657 int l = c.get(i);
658 if (voc.isFalsified(l) && !seen[var(l)] && voc.getLevel(l) != 0) {
659 if (voc.getReason(l) == null) {
660 for (int j = top; j < analyzetoclear.size(); j++)
661 seen[analyzetoclear.get(j) >> 1] = false;
662 analyzetoclear.shrink(analyzetoclear.size() - top);
663 return false;
664 }
665 seen[l >> 1] = true;
666 analyzestack.push(l);
667 analyzetoclear.push(l);
668 }
669 }
670 }
671
672 return true;
673 }
674
675
676
677
678
679
680 protected void undoOne() {
681
682 int p = trail.last();
683 assert p > 1;
684 assert voc.getLevel(p) >= 0;
685 int x = p >> 1;
686
687 voc.unassign(p);
688 voc.setReason(p, null);
689 voc.setLevel(p, -1);
690
691 order.undo(x);
692
693 trail.pop();
694
695
696
697 IVec<Undoable> undos = voc.undos(p);
698 assert undos != null;
699 while (undos.size() > 0) {
700 undos.last().undo(p);
701 undos.pop();
702 }
703 }
704
705
706
707
708
709
710
711 public void claBumpActivity(Constr confl) {
712 confl.incActivity(claInc);
713 if (confl.getActivity() > CLAUSE_RESCALE_BOUND)
714 claRescalActivity();
715
716
717
718 }
719
720 public void varBumpActivity(int p) {
721 order.updateVar(p);
722 }
723
724 private void claRescalActivity() {
725 for (int i = 0; i < learnts.size(); i++) {
726 learnts.get(i).rescaleBy(CLAUSE_RESCALE_FACTOR);
727 }
728 claInc *= CLAUSE_RESCALE_FACTOR;
729 }
730
731
732
733
734 public Constr propagate() {
735 while (qhead < trail.size()) {
736 stats.propagations++;
737 int p = trail.get(qhead++);
738 slistener.propagating(toDimacs(p));
739 order.assignLiteral(p);
740
741
742
743 assert p > 1;
744 IVec<Propagatable> watched = dsfactory.getAttachesFor(p);
745
746 final int size = watched.size();
747 for (int i = 0; i < size; i++) {
748 stats.inspects++;
749 if (!watched.get(i).propagate(this, p)) {
750
751
752
753 dsfactory.conflictDetectedInAttachesFor(p, i);
754 qhead = trail.size();
755
756 return (Constr) watched.get(i);
757 }
758 }
759 }
760 return null;
761 }
762
763 void record(Constr constr) {
764 constr.assertConstraint(this);
765 slistener.adding(toDimacs(constr.get(0)));
766 if (constr.size() == 1) {
767 stats.learnedliterals++;
768 learnedLiterals++;
769 } else {
770 learner.learns(constr);
771 }
772 }
773
774
775
776
777 public boolean assume(int p) {
778
779 assert trail.size() == qhead;
780 trailLim.push(trail.size());
781 return enqueue(p);
782 }
783
784
785
786
787 private void cancel() {
788
789 int decisionvar = trail.unsafeGet(trailLim.last());
790 slistener.backtracking(toDimacs(decisionvar));
791 for (int c = trail.size() - trailLim.last(); c > 0; c--) {
792 undoOne();
793 }
794 trailLim.pop();
795 }
796
797
798
799
800 private void cancelLearntLiterals() {
801
802 for (int c = learnedLiterals; c > 0; c--) {
803 undoOne();
804 }
805 qhead = trail.size();
806 }
807
808
809
810
811
812
813 protected void cancelUntil(int level) {
814 while (decisionLevel() > level) {
815 cancel();
816 }
817 qhead = trail.size();
818 }
819
820 private final Pair analysisResult = new Pair();
821
822 private boolean[] fullmodel;
823
824 Lbool search(long nofConflicts) {
825 assert rootLevel == decisionLevel();
826 stats.starts++;
827 int conflictC = 0;
828
829
830 order.setVarDecay(1 / params.getVarDecay());
831 claDecay = 1 / params.getClaDecay();
832
833 do {
834 slistener.beginLoop();
835
836 Constr confl = propagate();
837 assert trail.size() == qhead;
838
839 if (confl == null) {
840
841
842
843 if (decisionLevel() == 0 && isDBSimplificationAllowed) {
844
845
846 stats.rootSimplifications++;
847 boolean ret = simplifyDB();
848 assert ret;
849 }
850
851
852 assert nAssigns() <= voc.realnVars();
853 if (nAssigns() == voc.realnVars()) {
854 slistener.solutionFound();
855 modelFound();
856 return Lbool.TRUE;
857 }
858 if (conflictC >= nofConflicts) {
859
860
861 cancelUntil(rootLevel);
862 return Lbool.UNDEFINED;
863 }
864 if (needToReduceDB) {
865 reduceDB();
866 needToReduceDB = false;
867
868 }
869
870 stats.decisions++;
871 int p = order.select();
872 assert p > 1;
873 slistener.assuming(toDimacs(p));
874 boolean ret = assume(p);
875 assert ret;
876 } else {
877
878 stats.conflicts++;
879 conflictC++;
880 slistener.conflictFound();
881 conflictCount.newConflict();
882 if (decisionLevel() == rootLevel) {
883
884 return Lbool.FALSE;
885 }
886
887 analyze(confl, analysisResult);
888 assert analysisResult.backtrackLevel < decisionLevel();
889 cancelUntil(Math.max(analysisResult.backtrackLevel, rootLevel));
890 assert (decisionLevel() >= rootLevel)
891 && (decisionLevel() >= analysisResult.backtrackLevel);
892 if (analysisResult.reason == null) {
893 return Lbool.FALSE;
894 }
895 record(analysisResult.reason);
896 analysisResult.reason = null;
897 decayActivities();
898 }
899 } while (undertimeout);
900 return Lbool.UNDEFINED;
901 }
902
903 protected void analyzeAtRootLevel(Constr conflict) {
904 }
905
906
907
908
909 void modelFound() {
910 model = new int[trail.size()];
911 fullmodel = new boolean[nVars()];
912 int index = 0;
913 for (int i = 1; i <= voc.nVars(); i++) {
914 if (voc.belongsToPool(i)) {
915 int p = voc.getFromPool(i);
916 if (!voc.isUnassigned(p)) {
917 model[index++] = voc.isSatisfied(p) ? i : -i;
918 fullmodel[i - 1] = voc.isSatisfied(p);
919 }
920 }
921 }
922 assert index == model.length;
923 cancelUntil(rootLevel);
924 }
925
926 public boolean model(int var) {
927 if (var <= 0 || var > nVars()) {
928 throw new IllegalArgumentException(
929 "Use a valid Dimacs var id as argument!");
930 }
931 if (fullmodel == null) {
932 throw new UnsupportedOperationException(
933 "Call the solve method first!!!");
934 }
935 return fullmodel[var - 1];
936 }
937
938
939
940
941 protected void reduceDB() {
942 reduceDB(claInc / learnts.size());
943 }
944
945 public void clearLearntClauses() {
946 for (Iterator<Constr> iterator = learnts.iterator(); iterator.hasNext();)
947 iterator.next().remove();
948 learnts.clear();
949 }
950
951 protected void reduceDB(double lim) {
952 int i, j;
953 sortOnActivity();
954 stats.reduceddb++;
955 for (i = j = 0; i < learnts.size() / 2; i++) {
956 Constr c = learnts.get(i);
957 if (c.locked()) {
958 learnts.set(j++, learnts.get(i));
959 } else {
960 c.remove();
961 }
962 }
963 for (; i < learnts.size(); i++) {
964
965
966
967
968 learnts.set(j++, learnts.get(i));
969
970 }
971 System.out.println("c cleaning " + (learnts.size() - j)
972 + " clauses out of " + learnts.size() + " for limit " + lim);
973 learnts.shrinkTo(j);
974 }
975
976
977
978
979 private void sortOnActivity() {
980 learnts.sort(comparator);
981 }
982
983
984
985
986 protected void decayActivities() {
987 order.varDecayActivity();
988 claDecayActivity();
989 }
990
991
992
993
994 private void claDecayActivity() {
995 claInc *= claDecay;
996 }
997
998
999
1000
1001 public boolean isSatisfiable() throws TimeoutException {
1002 return isSatisfiable(VecInt.EMPTY);
1003 }
1004
1005
1006
1007
1008 public boolean isSatisfiable(boolean global) throws TimeoutException {
1009 return isSatisfiable(VecInt.EMPTY, global);
1010 }
1011
1012 private double timebegin = 0;
1013
1014 private boolean needToReduceDB;
1015
1016 private ConflictTimer conflictCount;
1017
1018 private transient Timer timer;
1019
1020 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
1021 return isSatisfiable(assumps, false);
1022 }
1023
1024 public boolean isSatisfiable(IVecInt assumps, boolean global)
1025 throws TimeoutException {
1026 Lbool status = Lbool.UNDEFINED;
1027
1028 final int howmany = voc.nVars();
1029 if (mseen.length < howmany) {
1030 mseen = new boolean[howmany + 1];
1031 }
1032 trail.ensure(howmany);
1033 trailLim.ensure(howmany);
1034 learnedLiterals = 0;
1035 order.init();
1036 learner.init();
1037 restarter.init(params);
1038 timebegin = System.currentTimeMillis();
1039 slistener.start();
1040 model = null;
1041 fullmodel = null;
1042
1043
1044 Constr confl = propagate();
1045 if (confl != null) {
1046 analyzeAtRootLevel(confl);
1047 slistener.end(Lbool.FALSE);
1048 cancelUntil(0);
1049 return false;
1050 }
1051
1052
1053 for (IteratorInt iterator = assumps.iterator(); iterator.hasNext();) {
1054 if (!assume(voc.getFromPool(iterator.next()))
1055 || (propagate() != null)) {
1056 slistener.end(Lbool.FALSE);
1057 cancelUntil(0);
1058 return false;
1059 }
1060 }
1061 rootLevel = decisionLevel();
1062
1063 final long memorybound = Runtime.getRuntime().freeMemory() / 10;
1064
1065 ConflictTimer freeMem = new ConflictTimerAdapter(500) {
1066 private static final long serialVersionUID = 1L;
1067
1068 @Override
1069 void run() {
1070 long freemem = Runtime.getRuntime().freeMemory();
1071
1072 if (freemem < memorybound) {
1073
1074 needToReduceDB = true;
1075 }
1076 }
1077 };
1078
1079 if (timeBasedTimeout) {
1080 if (!global || timer == null) {
1081 TimerTask stopMe = new TimerTask() {
1082 @Override
1083 public void run() {
1084 undertimeout = false;
1085 }
1086 };
1087 timer = new Timer(true);
1088 timer.schedule(stopMe, timeout);
1089 conflictCount = freeMem;
1090 }
1091 } else {
1092 if (!global || conflictCount == null) {
1093 ConflictTimer conflictTimeout = new ConflictTimerAdapter(
1094 (int) timeout) {
1095 private static final long serialVersionUID = 1L;
1096
1097 @Override
1098 public void run() {
1099 undertimeout = false;
1100 }
1101 };
1102 conflictCount = new ConflictTimerContainer().add(
1103 conflictTimeout).add(freeMem);
1104 }
1105 }
1106 needToReduceDB = false;
1107 undertimeout = true;
1108
1109
1110 while ((status == Lbool.UNDEFINED) && undertimeout) {
1111 status = search(restarter.nextRestartNumberOfConflict());
1112
1113
1114
1115 restarter.onRestart();
1116 }
1117
1118 cancelUntil(0);
1119 if (!global && timeBasedTimeout) {
1120 timer.cancel();
1121 timer = null;
1122 }
1123 slistener.end(status);
1124 if (!undertimeout) {
1125 throw new TimeoutException(" Timeout (" + timeout + "s) exceeded");
1126 }
1127 return status == Lbool.TRUE;
1128 }
1129
1130 public void printInfos(PrintWriter out, String prefix) {
1131 out.print(prefix);
1132 out.println("constraints type ");
1133 for (Map.Entry<String, Counter> entry : constrTypes.entrySet()) {
1134 out.println(prefix + entry.getKey() + " => " + entry.getValue());
1135 }
1136 }
1137
1138 public void printLearntClausesInfos(PrintWriter out, String prefix) {
1139 Map<String,Counter> learntTypes = new HashMap<String,Counter>();
1140 for (Iterator<Constr> it = learnts.iterator(); it.hasNext();) {
1141 String type = it.next().getClass().getName();
1142 Counter count = learntTypes.get(type);
1143 if (count == null) {
1144 learntTypes.put(type, new Counter());
1145 } else {
1146 count.inc();
1147 }
1148 }
1149 out.print(prefix);
1150 out.println("learnt constraints type ");
1151 for (Map.Entry<String, Counter> entry : learntTypes.entrySet()) {
1152 out.println(prefix + entry.getKey() + " => " + entry.getValue());
1153 }
1154 }
1155
1156 public SolverStats getStats() {
1157 return stats;
1158 }
1159
1160 public IOrder<L> getOrder() {
1161 return order;
1162 }
1163
1164 public void setOrder(IOrder<L> h) {
1165 order = h;
1166 order.setLits(voc);
1167 }
1168
1169 public L getVocabulary() {
1170 return voc;
1171 }
1172
1173 public void reset() {
1174
1175 voc.resetPool();
1176 dsfactory.reset();
1177 constrs.clear();
1178 learnts.clear();
1179 stats.reset();
1180 constrTypes.clear();
1181 }
1182
1183 public int nVars() {
1184 return voc.nVars();
1185 }
1186
1187
1188
1189
1190
1191
1192 protected IConstr addConstr(Constr constr) {
1193 if (constr != null) {
1194 constrs.push(constr);
1195 String type = constr.getClass().getName();
1196 Counter count = constrTypes.get(type);
1197 if (count == null) {
1198 constrTypes.put(type, new Counter());
1199 } else {
1200 count.inc();
1201 }
1202 }
1203 return constr;
1204 }
1205
1206 public DataStructureFactory<L> getDSFactory() {
1207 return dsfactory;
1208 }
1209
1210 public IVecInt getOutLearnt() {
1211 return outLearnt;
1212 }
1213
1214
1215
1216
1217
1218
1219
1220
1221 public IConstr getIthConstr(int i) {
1222 return constrs.get(i);
1223 }
1224
1225
1226
1227
1228
1229
1230
1231 public void printStat(PrintStream out, String prefix) {
1232 printStat(new PrintWriter(out), prefix);
1233 }
1234
1235 public void printStat(PrintWriter out, String prefix) {
1236 stats.printStat(out, prefix);
1237 double cputime = (System.currentTimeMillis() - timebegin) / 1000;
1238 out.println(prefix
1239 + "speed (assignments/second)\t: " + stats.propagations
1240 / cputime);
1241 order.printStat(out, prefix);
1242 printLearntClausesInfos(out, prefix);
1243 }
1244
1245
1246
1247
1248
1249
1250 public String toString(String prefix) {
1251 StringBuffer stb = new StringBuffer();
1252 Object[] objs = { analyzer, dsfactory, learner, params, order,
1253 simplifier, restarter };
1254 stb.append(prefix);
1255 stb.append("--- Begin Solver configuration ---");
1256 stb.append("\n");
1257 for (Object o : objs) {
1258 stb.append(prefix);
1259 stb.append(o.toString());
1260 stb.append("\n");
1261 }
1262 stb.append(prefix);
1263 stb.append("timeout=");
1264 if (timeBasedTimeout) {
1265 stb.append(timeout / 1000);
1266 stb.append("s\n");
1267 } else {
1268 stb.append(timeout);
1269 stb.append(" conflicts\n");
1270 }
1271 stb.append(prefix);
1272 stb.append("DB Simplification allowed=");
1273 stb.append(isDBSimplificationAllowed);
1274 stb.append("\n");
1275 stb.append(prefix);
1276 stb.append("--- End Solver configuration ---");
1277 return stb.toString();
1278 }
1279
1280
1281
1282
1283
1284
1285 @Override
1286 public String toString() {
1287 return toString("");
1288 }
1289
1290 public int getTimeout() {
1291 return (int) (timeBasedTimeout ? timeout / 1000 : timeout);
1292 }
1293
1294 public long getTimeoutMs() {
1295 if (!timeBasedTimeout) {
1296 throw new UnsupportedOperationException(
1297 "The timeout is given in number of conflicts!");
1298 }
1299 return timeout;
1300 }
1301
1302 public void setExpectedNumberOfClauses(int nb) {
1303 constrs.ensure(nb);
1304 }
1305
1306 public Map<String, Number> getStat() {
1307 return stats.toMap();
1308 }
1309
1310 public int[] findModel() throws TimeoutException {
1311 if (isSatisfiable()) {
1312 return model();
1313 }
1314
1315
1316 return null;
1317 }
1318
1319 public int[] findModel(IVecInt assumps) throws TimeoutException {
1320 if (isSatisfiable(assumps)) {
1321 return model();
1322 }
1323
1324
1325 return null;
1326 }
1327
1328 public boolean isDBSimplificationAllowed() {
1329 return isDBSimplificationAllowed;
1330 }
1331
1332 public void setDBSimplificationAllowed(boolean status) {
1333 isDBSimplificationAllowed = status;
1334 }
1335
1336 }
1337
1338 class ActivityComparator implements Comparator<Constr>, Serializable {
1339
1340 private static final long serialVersionUID = 1L;
1341
1342
1343
1344
1345
1346
1347 public int compare(Constr c1, Constr c2) {
1348 return (int) Math.round(c1.getActivity() - c2.getActivity());
1349 }
1350 }
1351
1352 interface ConflictTimer {
1353
1354 void reset();
1355
1356 void newConflict();
1357 }
1358
1359 abstract class ConflictTimerAdapter implements Serializable, ConflictTimer {
1360
1361
1362
1363
1364 private static final long serialVersionUID = 1L;
1365
1366 private int counter;
1367
1368 private final int bound;
1369
1370 ConflictTimerAdapter(final int bound) {
1371 this.bound = bound;
1372 counter = 0;
1373 }
1374
1375 public void reset() {
1376 counter = 0;
1377 }
1378
1379 public void newConflict() {
1380 counter++;
1381 if (counter == bound) {
1382 run();
1383 counter = 0;
1384 }
1385 }
1386
1387 abstract void run();
1388 }
1389
1390 class ConflictTimerContainer implements Serializable, ConflictTimer {
1391
1392
1393
1394
1395 private static final long serialVersionUID = 1L;
1396
1397 private final IVec<ConflictTimer> timers = new Vec<ConflictTimer>();
1398
1399 ConflictTimerContainer add(ConflictTimer timer) {
1400 timers.push(timer);
1401 return this;
1402 }
1403
1404 public void reset() {
1405 Iterator<ConflictTimer> it = timers.iterator();
1406 while (it.hasNext()) {
1407 it.next().reset();
1408 }
1409 }
1410
1411 public void newConflict() {
1412 Iterator<ConflictTimer> it = timers.iterator();
1413 while (it.hasNext()) {
1414 it.next().newConflict();
1415 }
1416 }
1417 }