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 package org.sat4j.minisat.core;
31
32 import static org.sat4j.core.LiteralsUtils.neg;
33 import static org.sat4j.core.LiteralsUtils.toDimacs;
34 import static org.sat4j.core.LiteralsUtils.toInternal;
35 import static org.sat4j.core.LiteralsUtils.var;
36
37 import java.io.PrintStream;
38 import java.io.PrintWriter;
39 import java.lang.reflect.Field;
40 import java.util.ArrayList;
41 import java.util.Collections;
42 import java.util.Comparator;
43 import java.util.HashMap;
44 import java.util.HashSet;
45 import java.util.Iterator;
46 import java.util.List;
47 import java.util.Map;
48 import java.util.Set;
49 import java.util.Timer;
50 import java.util.TimerTask;
51
52 import org.sat4j.core.ConstrGroup;
53 import org.sat4j.core.LiteralsUtils;
54 import org.sat4j.core.Vec;
55 import org.sat4j.core.VecInt;
56 import org.sat4j.specs.ContradictionException;
57 import org.sat4j.specs.IConstr;
58 import org.sat4j.specs.ILogAble;
59 import org.sat4j.specs.ISolver;
60 import org.sat4j.specs.ISolverService;
61 import org.sat4j.specs.IVec;
62 import org.sat4j.specs.IVecInt;
63 import org.sat4j.specs.IteratorInt;
64 import org.sat4j.specs.Lbool;
65 import org.sat4j.specs.SearchListener;
66 import org.sat4j.specs.TimeoutException;
67 import org.sat4j.specs.UnitClauseProvider;
68
69
70
71
72
73
74
75 public class Solver<D extends DataStructureFactory> implements ISolverService,
76 ICDCL<D> {
77
78 private static final long serialVersionUID = 1L;
79
80 private static final double CLAUSE_RESCALE_FACTOR = 1e-20;
81
82 private static final double CLAUSE_RESCALE_BOUND = 1 / CLAUSE_RESCALE_FACTOR;
83
84 protected ILogAble out;
85
86
87
88
89 protected final IVec<Constr> constrs = new Vec<Constr>();
90
91
92
93
94 protected final IVec<Constr> learnts = new Vec<Constr>();
95
96
97
98
99 private double claInc = 1.0;
100
101
102
103
104 private double claDecay = 1.0;
105
106
107
108
109
110 private int qhead = 0;
111
112
113
114
115 protected final IVecInt trail = new VecInt();
116
117
118
119
120 protected final IVecInt trailLim = new VecInt();
121
122
123
124
125 protected int rootLevel;
126
127 private int[] model = null;
128
129 protected ILits voc;
130
131 private IOrder order;
132
133 private final ActivityComparator comparator = new ActivityComparator();
134
135 private SolverStats stats = new SolverStats();
136
137 private LearningStrategy<D> learner;
138
139 protected volatile boolean undertimeout;
140
141 private long timeout = Integer.MAX_VALUE;
142
143 private boolean timeBasedTimeout = true;
144
145 protected D dsfactory;
146
147 private SearchParams params;
148
149 private final IVecInt __dimacs_out = new VecInt();
150
151 protected SearchListener slistener = new VoidTracing();
152
153 private RestartStrategy restarter;
154
155 private final Map<String, Counter> constrTypes = new HashMap<String, Counter>();
156
157 private boolean isDBSimplificationAllowed = false;
158
159 private final IVecInt learnedLiterals = new VecInt();
160
161 private boolean verbose = false;
162
163 private boolean keepHot = false;
164
165 private String prefix = "c ";
166 private int declaredMaxVarId = 0;
167
168 private UnitClauseProvider unitClauseProvider = UnitClauseProvider.VOID;
169
170 protected IVecInt dimacs2internal(IVecInt in) {
171 this.__dimacs_out.clear();
172 this.__dimacs_out.ensure(in.size());
173 int p;
174 for (int i = 0; i < in.size(); i++) {
175 p = in.get(i);
176 if (p == 0) {
177 throw new IllegalArgumentException(
178 "0 is not a valid variable identifier");
179 }
180 this.__dimacs_out.unsafePush(this.voc.getFromPool(p));
181 }
182 return this.__dimacs_out;
183 }
184
185
186
187
188 public void registerLiteral(int p) {
189 this.voc.getFromPool(p);
190 }
191
192
193
194
195
196
197
198 public Solver(LearningStrategy<D> learner, D dsf, IOrder order,
199 RestartStrategy restarter) {
200 this(learner, dsf, new SearchParams(), order, restarter);
201 }
202
203 public Solver(LearningStrategy<D> learner, D dsf, SearchParams params,
204 IOrder order, RestartStrategy restarter) {
205 this(learner, dsf, params, order, restarter, ILogAble.CONSOLE);
206 }
207
208 public Solver(LearningStrategy<D> learner, D dsf, SearchParams params,
209 IOrder order, RestartStrategy restarter, ILogAble logger) {
210 this.order = order;
211 this.params = params;
212 this.restarter = restarter;
213 this.out = logger;
214 setDataStructureFactory(dsf);
215
216 setLearningStrategy(learner);
217 }
218
219
220
221
222
223
224 public final void setDataStructureFactory(D dsf) {
225 this.dsfactory = dsf;
226 this.dsfactory.setUnitPropagationListener(this);
227 this.dsfactory.setLearner(this);
228 this.voc = dsf.getVocabulary();
229 this.order.setLits(this.voc);
230 }
231
232
233
234
235 public boolean isVerbose() {
236 return this.verbose;
237 }
238
239
240
241
242
243 public void setVerbose(boolean value) {
244 this.verbose = value;
245 }
246
247
248
249
250
251
252
253
254 public <S extends ISolverService> void setSearchListener(
255 SearchListener<S> sl) {
256 this.slistener = sl;
257 }
258
259
260
261
262
263
264 public <S extends ISolverService> SearchListener<S> getSearchListener() {
265 return this.slistener;
266 }
267
268
269
270
271
272
273
274 public void setLearner(LearningStrategy<D> strategy) {
275 setLearningStrategy(strategy);
276 }
277
278
279
280
281
282
283
284
285 public void setLearningStrategy(LearningStrategy<D> strategy) {
286 if (this.learner != null) {
287 this.learner.setSolver(null);
288 }
289 this.learner = strategy;
290 strategy.setSolver(this);
291 }
292
293 public void setTimeout(int t) {
294 this.timeout = t * 1000L;
295 this.timeBasedTimeout = true;
296 }
297
298 public void setTimeoutMs(long t) {
299 this.timeout = t;
300 this.timeBasedTimeout = true;
301 }
302
303 public void setTimeoutOnConflicts(int count) {
304 this.timeout = count;
305 this.timeBasedTimeout = false;
306 }
307
308
309
310
311
312
313
314 public void setSearchParams(SearchParams sp) {
315 this.params = sp;
316 }
317
318 public SearchParams getSearchParams() {
319 return this.params;
320 }
321
322
323
324
325
326
327
328
329 public void setRestartStrategy(RestartStrategy restarter) {
330 this.restarter = restarter;
331 }
332
333
334
335
336
337
338 public RestartStrategy getRestartStrategy() {
339 return this.restarter;
340 }
341
342 public void expireTimeout() {
343 this.undertimeout = false;
344 if (this.timeBasedTimeout) {
345 if (this.timer != null) {
346 this.timer.cancel();
347 this.timer = null;
348 }
349 } else {
350 if (this.conflictCount != null) {
351 this.conflictCount = null;
352 }
353 }
354 }
355
356 protected int nAssigns() {
357 return this.trail.size();
358 }
359
360 public int nConstraints() {
361 return this.constrs.size();
362 }
363
364 public void learn(Constr c) {
365 this.slistener.learn(c);
366 this.learnts.push(c);
367 c.setLearnt();
368 c.register();
369 this.stats.learnedclauses++;
370 switch (c.size()) {
371 case 2:
372 this.stats.learnedbinaryclauses++;
373 break;
374 case 3:
375 this.stats.learnedternaryclauses++;
376 break;
377 default:
378
379 }
380 }
381
382 public final int decisionLevel() {
383 return this.trailLim.size();
384 }
385
386 @Deprecated
387 public int newVar() {
388 int index = this.voc.nVars() + 1;
389 this.voc.ensurePool(index);
390 return index;
391 }
392
393 public int newVar(int howmany) {
394 this.voc.ensurePool(howmany);
395 this.declaredMaxVarId = howmany;
396 return howmany;
397 }
398
399 public IConstr addClause(IVecInt literals) throws ContradictionException {
400 IVecInt vlits = dimacs2internal(literals);
401 return addConstr(this.dsfactory.createClause(vlits));
402 }
403
404 public boolean removeConstr(IConstr co) {
405 if (co == null) {
406 throw new IllegalArgumentException(
407 "Reference to the constraint to remove needed!");
408 }
409 Constr c = (Constr) co;
410 c.remove(this);
411 this.constrs.remove(c);
412 clearLearntClauses();
413 String type = c.getClass().getName();
414 this.constrTypes.get(type).dec();
415 return true;
416 }
417
418
419
420
421 public boolean removeSubsumedConstr(IConstr co) {
422 if (co == null) {
423 throw new IllegalArgumentException(
424 "Reference to the constraint to remove needed!");
425 }
426 if (this.constrs.last() != co) {
427 throw new IllegalArgumentException(
428 "Can only remove latest added constraint!!!");
429 }
430 Constr c = (Constr) co;
431 c.remove(this);
432 this.constrs.pop();
433 String type = c.getClass().getName();
434 this.constrTypes.get(type).dec();
435 return true;
436 }
437
438 public void addAllClauses(IVec<IVecInt> clauses)
439 throws ContradictionException {
440 for (Iterator<IVecInt> iterator = clauses.iterator(); iterator
441 .hasNext();) {
442 addClause(iterator.next());
443 }
444 }
445
446 public IConstr addAtMost(IVecInt literals, int degree)
447 throws ContradictionException {
448 int n = literals.size();
449 IVecInt opliterals = new VecInt(n);
450 for (IteratorInt iterator = literals.iterator(); iterator.hasNext();) {
451 opliterals.push(-iterator.next());
452 }
453 return addAtLeast(opliterals, n - degree);
454 }
455
456 public IConstr addAtLeast(IVecInt literals, int degree)
457 throws ContradictionException {
458 IVecInt vlits = dimacs2internal(literals);
459 return addConstr(this.dsfactory.createCardinalityConstraint(vlits,
460 degree));
461 }
462
463 public IConstr addExactly(IVecInt literals, int n)
464 throws ContradictionException {
465 ConstrGroup group = new ConstrGroup(false);
466 group.add(addAtMost(literals, n));
467 group.add(addAtLeast(literals, n));
468 return group;
469 }
470
471 @SuppressWarnings("unchecked")
472 public boolean simplifyDB() {
473
474
475 IVec<Constr>[] cs = new IVec[] { this.constrs, this.learnts };
476 for (int type = 0; type < 2; type++) {
477 int j = 0;
478 for (int i = 0; i < cs[type].size(); i++) {
479 if (cs[type].get(i).simplify()) {
480
481 cs[type].get(i).remove(this);
482 } else {
483 cs[type].moveTo(j++, i);
484 }
485 }
486 cs[type].shrinkTo(j);
487 }
488 return true;
489 }
490
491
492
493
494
495
496 public int[] model() {
497 if (this.model == null) {
498 throw new UnsupportedOperationException(
499 "Call the solve method first!!!");
500 }
501 int[] nmodel = new int[this.model.length];
502 System.arraycopy(this.model, 0, nmodel, 0, this.model.length);
503 return nmodel;
504 }
505
506
507
508
509
510
511 public boolean enqueue(int p) {
512 return enqueue(p, null);
513 }
514
515
516
517
518
519
520
521 public boolean enqueue(int p, Constr from) {
522 assert p > 1;
523 if (this.voc.isSatisfied(p)) {
524
525 return true;
526 }
527 if (this.voc.isFalsified(p)) {
528
529 return false;
530 }
531
532 this.voc.satisfies(p);
533 this.voc.setLevel(p, decisionLevel());
534 this.voc.setReason(p, from);
535 this.trail.push(p);
536 if (from != null && from.learnt()) {
537 this.learnedConstraintsDeletionStrategy.onPropagation(from);
538 }
539 return true;
540 }
541
542 private boolean[] mseen = new boolean[0];
543
544 private final IVecInt mpreason = new VecInt();
545
546 private final IVecInt moutLearnt = new VecInt();
547
548
549
550
551
552 public void analyze(Constr confl, Pair results) throws TimeoutException {
553 assert confl != null;
554
555 final boolean[] seen = this.mseen;
556 final IVecInt outLearnt = this.moutLearnt;
557 final IVecInt preason = this.mpreason;
558
559 outLearnt.clear();
560 assert outLearnt.size() == 0;
561 for (int i = 0; i < seen.length; i++) {
562 seen[i] = false;
563 }
564
565 int counter = 0;
566 int p = ILits.UNDEFINED;
567
568 outLearnt.push(ILits.UNDEFINED);
569
570 int outBtlevel = 0;
571 IConstr prevConfl = null;
572
573 do {
574 preason.clear();
575 assert confl != null;
576 if (prevConfl != confl) {
577 confl.calcReason(p, preason);
578 this.learnedConstraintsDeletionStrategy
579 .onConflictAnalysis(confl);
580
581 for (int j = 0; j < preason.size(); j++) {
582 int q = preason.get(j);
583 this.order.updateVar(q);
584 if (!seen[q >> 1]) {
585 seen[q >> 1] = true;
586 if (this.voc.getLevel(q) == decisionLevel()) {
587 counter++;
588 this.order.updateVarAtDecisionLevel(q);
589 } else if (this.voc.getLevel(q) > 0) {
590
591
592
593 outLearnt.push(q ^ 1);
594 outBtlevel = Math.max(outBtlevel,
595 this.voc.getLevel(q));
596 }
597 }
598 }
599 }
600 prevConfl = confl;
601
602 do {
603 p = this.trail.last();
604 confl = this.voc.getReason(p);
605 undoOne();
606 } while (!seen[p >> 1]);
607
608
609 } while (--counter > 0);
610
611 outLearnt.set(0, p ^ 1);
612 this.simplifier.simplify(outLearnt);
613
614 Constr c = this.dsfactory.createUnregisteredClause(outLearnt);
615
616 this.learnedConstraintsDeletionStrategy.onClauseLearning(c);
617 results.reason = c;
618
619 assert outBtlevel > -1;
620 results.backtrackLevel = outBtlevel;
621 }
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636 public IVecInt analyzeFinalConflictInTermsOfAssumptions(Constr confl,
637 IVecInt assumps, int conflictingLiteral) {
638 if (assumps.size() == 0) {
639 return null;
640 }
641 while (!this.trailLim.isEmpty()
642 && this.trailLim.last() == this.trail.size()) {
643
644 this.trailLim.pop();
645 }
646 final boolean[] seen = this.mseen;
647 final IVecInt outLearnt = this.moutLearnt;
648 final IVecInt preason = this.mpreason;
649
650 outLearnt.clear();
651 if (this.trailLim.size() == 0) {
652
653 return outLearnt;
654 }
655
656 assert outLearnt.size() == 0;
657 for (int i = 0; i < seen.length; i++) {
658 seen[i] = false;
659 }
660
661 if (confl == null) {
662 seen[conflictingLiteral >> 1] = true;
663 }
664
665 int p = ILits.UNDEFINED;
666 while (confl == null && this.trail.size() > 0
667 && this.trailLim.size() > 0) {
668 p = this.trail.last();
669 confl = this.voc.getReason(p);
670 undoOne();
671 if (confl == null && p == (conflictingLiteral ^ 1)) {
672 outLearnt.push(toDimacs(p));
673 }
674 if (this.trail.size() <= this.trailLim.last()) {
675 this.trailLim.pop();
676 }
677 }
678 if (confl == null) {
679 return outLearnt;
680 }
681 do {
682
683 preason.clear();
684 confl.calcReason(p, preason);
685
686 for (int j = 0; j < preason.size(); j++) {
687 int q = preason.get(j);
688 if (!seen[q >> 1]) {
689 seen[q >> 1] = true;
690 if (this.voc.getReason(q) == null
691 && this.voc.getLevel(q) > 0) {
692 assert assumps.contains(toDimacs(q));
693 outLearnt.push(toDimacs(q));
694 }
695 }
696 }
697
698
699 do {
700 p = this.trail.last();
701 confl = this.voc.getReason(p);
702 undoOne();
703 if (decisionLevel() > 0
704 && this.trail.size() <= this.trailLim.last()) {
705 this.trailLim.pop();
706 }
707 } while (this.trail.size() > 0 && decisionLevel() > 0
708 && (!seen[p >> 1] || confl == null));
709 } while (decisionLevel() > 0);
710 return outLearnt;
711 }
712
713 public static final ISimplifier NO_SIMPLIFICATION = new ISimplifier() {
714
715
716
717 private static final long serialVersionUID = 1L;
718
719 public void simplify(IVecInt outLearnt) {
720 }
721
722 @Override
723 public String toString() {
724 return "No reason simplification";
725 }
726 };
727
728 public final ISimplifier SIMPLE_SIMPLIFICATION = new ISimplifier() {
729
730
731
732 private static final long serialVersionUID = 1L;
733
734 public void simplify(IVecInt conflictToReduce) {
735 simpleSimplification(conflictToReduce);
736 }
737
738 @Override
739 public String toString() {
740 return "Simple reason simplification";
741 }
742 };
743
744 public final ISimplifier EXPENSIVE_SIMPLIFICATION = new ISimplifier() {
745
746
747
748
749 private static final long serialVersionUID = 1L;
750
751 public void simplify(IVecInt conflictToReduce) {
752 expensiveSimplification(conflictToReduce);
753 }
754
755 @Override
756 public String toString() {
757 return "Expensive reason simplification";
758 }
759 };
760
761 public final ISimplifier EXPENSIVE_SIMPLIFICATION_WLONLY = new ISimplifier() {
762
763
764
765
766 private static final long serialVersionUID = 1L;
767
768 public void simplify(IVecInt conflictToReduce) {
769 expensiveSimplificationWLOnly(conflictToReduce);
770 }
771
772 @Override
773 public String toString() {
774 return "Expensive reason simplification specific for WL data structure";
775 }
776 };
777
778 private ISimplifier simplifier = NO_SIMPLIFICATION;
779
780
781
782
783
784
785 public void setSimplifier(SimplificationType simp) {
786 Field f;
787 try {
788 f = Solver.class.getDeclaredField(simp.toString());
789 this.simplifier = (ISimplifier) f.get(this);
790 } catch (Exception e) {
791 e.printStackTrace();
792 this.simplifier = NO_SIMPLIFICATION;
793 }
794 }
795
796
797
798
799
800
801
802
803 public void setSimplifier(ISimplifier simp) {
804 this.simplifier = simp;
805 }
806
807
808
809
810
811
812 public ISimplifier getSimplifier() {
813 return this.simplifier;
814 }
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838 private void simpleSimplification(IVecInt conflictToReduce) {
839 int i, j, p;
840 final boolean[] seen = this.mseen;
841 IConstr r;
842 for (i = j = 1; i < conflictToReduce.size(); i++) {
843 r = this.voc.getReason(conflictToReduce.get(i));
844 if (r == null || r.canBePropagatedMultipleTimes()) {
845 conflictToReduce.moveTo(j++, i);
846 } else {
847 for (int k = 0; k < r.size(); k++) {
848 p = r.get(k);
849 if (!seen[p >> 1] && this.voc.isFalsified(p)
850 && this.voc.getLevel(p) != 0) {
851 conflictToReduce.moveTo(j++, i);
852 break;
853 }
854 }
855 }
856 }
857 conflictToReduce.shrink(i - j);
858 this.stats.reducedliterals += i - j;
859 }
860
861 private final IVecInt analyzetoclear = new VecInt();
862
863 private final IVecInt analyzestack = new VecInt();
864
865
866 private void expensiveSimplification(IVecInt conflictToReduce) {
867
868
869 int i, j;
870
871 this.analyzetoclear.clear();
872 conflictToReduce.copyTo(this.analyzetoclear);
873 for (i = 1, j = 1; i < conflictToReduce.size(); i++) {
874 if (this.voc.getReason(conflictToReduce.get(i)) == null
875 || !analyzeRemovable(conflictToReduce.get(i))) {
876 conflictToReduce.moveTo(j++, i);
877 }
878 }
879 conflictToReduce.shrink(i - j);
880 this.stats.reducedliterals += i - j;
881 }
882
883
884
885
886 private boolean analyzeRemovable(int p) {
887 assert this.voc.getReason(p) != null;
888 ILits lvoc = this.voc;
889 IVecInt lanalyzestack = this.analyzestack;
890 IVecInt lanalyzetoclear = this.analyzetoclear;
891 lanalyzestack.clear();
892 lanalyzestack.push(p);
893 final boolean[] seen = this.mseen;
894 int top = lanalyzetoclear.size();
895 while (lanalyzestack.size() > 0) {
896 int q = lanalyzestack.last();
897 assert lvoc.getReason(q) != null;
898 Constr c = lvoc.getReason(q);
899 lanalyzestack.pop();
900 if (c.canBePropagatedMultipleTimes()) {
901 for (int j = top; j < lanalyzetoclear.size(); j++) {
902 seen[lanalyzetoclear.get(j) >> 1] = false;
903 }
904 lanalyzetoclear.shrink(lanalyzetoclear.size() - top);
905 return false;
906 }
907 for (int i = 0; i < c.size(); i++) {
908 int l = c.get(i);
909 if (!seen[var(l)] && lvoc.isFalsified(l)
910 && lvoc.getLevel(l) != 0) {
911 if (lvoc.getReason(l) == null) {
912 for (int j = top; j < lanalyzetoclear.size(); j++) {
913 seen[lanalyzetoclear.get(j) >> 1] = false;
914 }
915 lanalyzetoclear.shrink(lanalyzetoclear.size() - top);
916 return false;
917 }
918 seen[l >> 1] = true;
919 lanalyzestack.push(l);
920 lanalyzetoclear.push(l);
921 }
922 }
923
924 }
925
926 return true;
927 }
928
929
930 private void expensiveSimplificationWLOnly(IVecInt conflictToReduce) {
931
932
933 int i, j;
934
935 this.analyzetoclear.clear();
936 conflictToReduce.copyTo(this.analyzetoclear);
937 for (i = 1, j = 1; i < conflictToReduce.size(); i++) {
938 if (this.voc.getReason(conflictToReduce.get(i)) == null
939 || !analyzeRemovableWLOnly(conflictToReduce.get(i))) {
940 conflictToReduce.moveTo(j++, i);
941 }
942 }
943 conflictToReduce.shrink(i - j);
944 this.stats.reducedliterals += i - j;
945 }
946
947
948
949
950 private boolean analyzeRemovableWLOnly(int p) {
951 assert this.voc.getReason(p) != null;
952 this.analyzestack.clear();
953 this.analyzestack.push(p);
954 final boolean[] seen = this.mseen;
955 int top = this.analyzetoclear.size();
956 while (this.analyzestack.size() > 0) {
957 int q = this.analyzestack.last();
958 assert this.voc.getReason(q) != null;
959 Constr c = this.voc.getReason(q);
960 this.analyzestack.pop();
961 for (int i = 1; i < c.size(); i++) {
962 int l = c.get(i);
963 if (!seen[var(l)] && this.voc.getLevel(l) != 0) {
964 if (this.voc.getReason(l) == null) {
965 for (int j = top; j < this.analyzetoclear.size(); j++) {
966 seen[this.analyzetoclear.get(j) >> 1] = false;
967 }
968 this.analyzetoclear.shrink(this.analyzetoclear.size()
969 - top);
970 return false;
971 }
972 seen[l >> 1] = true;
973 this.analyzestack.push(l);
974 this.analyzetoclear.push(l);
975 }
976 }
977 }
978
979 return true;
980 }
981
982
983
984
985
986
987 protected void undoOne() {
988
989 int p = this.trail.last();
990 assert p > 1;
991 assert this.voc.getLevel(p) >= 0;
992 int x = p >> 1;
993
994 this.voc.unassign(p);
995 this.voc.setReason(p, null);
996 this.voc.setLevel(p, -1);
997
998 this.order.undo(x);
999
1000 this.trail.pop();
1001
1002
1003 IVec<Undoable> undos = this.voc.undos(p);
1004 assert undos != null;
1005 for (int size = undos.size(); size > 0; size--) {
1006 undos.last().undo(p);
1007 undos.pop();
1008 }
1009 }
1010
1011
1012
1013
1014
1015
1016
1017 public void claBumpActivity(Constr confl) {
1018 confl.incActivity(this.claInc);
1019 if (confl.getActivity() > CLAUSE_RESCALE_BOUND) {
1020 claRescalActivity();
1021
1022
1023
1024 }
1025 }
1026
1027 public void varBumpActivity(int p) {
1028 this.order.updateVar(p);
1029 }
1030
1031 private void claRescalActivity() {
1032 for (int i = 0; i < this.learnts.size(); i++) {
1033 this.learnts.get(i).rescaleBy(CLAUSE_RESCALE_FACTOR);
1034 }
1035 this.claInc *= CLAUSE_RESCALE_FACTOR;
1036 }
1037
1038 private final IVec<Propagatable> watched = new Vec<Propagatable>();
1039
1040
1041
1042
1043 public final Constr propagate() {
1044 IVecInt ltrail = this.trail;
1045 SolverStats lstats = this.stats;
1046 IOrder lorder = this.order;
1047 SearchListener lslistener = this.slistener;
1048
1049
1050 while (this.qhead < ltrail.size()) {
1051 lstats.propagations++;
1052 int p = ltrail.get(this.qhead++);
1053 lslistener.propagating(toDimacs(p), null);
1054 lorder.assignLiteral(p);
1055 Constr confl = reduceClausesForFalsifiedLiteral(p);
1056 if (confl != null) {
1057 return confl;
1058 }
1059 }
1060 return null;
1061 }
1062
1063 private Constr reduceClausesForFalsifiedLiteral(int p) {
1064
1065
1066
1067 assert p > 1;
1068 IVec<Propagatable> lwatched = this.watched;
1069 lwatched.clear();
1070 this.voc.watches(p).moveTo(lwatched);
1071 final int size = lwatched.size();
1072 for (int i = 0; i < size; i++) {
1073 this.stats.inspects++;
1074
1075
1076
1077
1078
1079
1080
1081
1082 if (!lwatched.get(i).propagate(this, p)) {
1083
1084
1085
1086 final int sizew = lwatched.size();
1087 for (int j = i + 1; j < sizew; j++) {
1088 this.voc.watch(p, lwatched.get(j));
1089 }
1090 this.qhead = this.trail.size();
1091 return lwatched.get(i).toConstraint();
1092 }
1093 }
1094 return null;
1095 }
1096
1097 void record(Constr constr) {
1098 constr.assertConstraint(this);
1099 int p = toDimacs(constr.get(0));
1100 this.slistener.adding(p);
1101 if (constr.size() == 1) {
1102 this.stats.learnedliterals++;
1103 this.slistener.learnUnit(p);
1104 } else {
1105 this.learner.learns(constr);
1106 }
1107 }
1108
1109
1110
1111
1112 public boolean assume(int p) {
1113
1114 assert this.trail.size() == this.qhead;
1115 assert !this.trailLim.contains(this.trail.size());
1116 this.trailLim.push(this.trail.size());
1117 return enqueue(p);
1118 }
1119
1120
1121
1122
1123 private void cancel() {
1124
1125 int decisionvar = this.trail.unsafeGet(this.trailLim.last());
1126 this.slistener.backtracking(toDimacs(decisionvar));
1127 for (int c = this.trail.size() - this.trailLim.last(); c > 0; c--) {
1128 undoOne();
1129 }
1130 this.trailLim.pop();
1131 this.qhead = this.trail.size();
1132 }
1133
1134
1135
1136
1137 private void cancelLearntLiterals(int learnedLiteralsLimit) {
1138 this.learnedLiterals.clear();
1139
1140 while (this.trail.size() > learnedLiteralsLimit) {
1141 this.learnedLiterals.push(this.trail.last());
1142 undoOne();
1143 }
1144
1145
1146 }
1147
1148
1149
1150
1151
1152
1153 protected void cancelUntil(int level) {
1154 while (decisionLevel() > level) {
1155 cancel();
1156 }
1157 }
1158
1159 private final Pair analysisResult = new Pair();
1160
1161 private boolean[] userbooleanmodel;
1162
1163 private IVecInt unsatExplanationInTermsOfAssumptions;
1164
1165 Lbool search(IVecInt assumps) {
1166 assert this.rootLevel == decisionLevel();
1167 this.stats.starts++;
1168 int backjumpLevel;
1169
1170
1171 this.order.setVarDecay(1 / this.params.getVarDecay());
1172 this.claDecay = 1 / this.params.getClaDecay();
1173
1174 do {
1175 this.slistener.beginLoop();
1176
1177 Constr confl = propagate();
1178 assert this.trail.size() == this.qhead;
1179
1180 if (confl == null) {
1181
1182 if (decisionLevel() == 0 && this.isDBSimplificationAllowed) {
1183 this.stats.rootSimplifications++;
1184 boolean ret = simplifyDB();
1185 assert ret;
1186 }
1187 assert nAssigns() <= this.voc.realnVars();
1188 if (nAssigns() == this.voc.realnVars()) {
1189 modelFound();
1190 this.slistener.solutionFound(
1191 (this.fullmodel != null) ? this.fullmodel
1192 : this.model, this);
1193 if (this.sharedConflict == null) {
1194 cancelUntil(this.rootLevel);
1195 return Lbool.TRUE;
1196 } else {
1197 confl = this.sharedConflict;
1198 }
1199 } else {
1200 if (this.restarter.shouldRestart()) {
1201 cancelUntil(this.rootLevel);
1202 return Lbool.UNDEFINED;
1203 }
1204 if (this.needToReduceDB) {
1205 reduceDB();
1206 this.needToReduceDB = false;
1207 }
1208 if (this.sharedConflict == null) {
1209
1210 this.stats.decisions++;
1211 int p = this.order.select();
1212 if (p == ILits.UNDEFINED) {
1213 confl = preventTheSameDecisionsToBeMade();
1214 this.lastConflictMeansUnsat = false;
1215 } else {
1216 assert p > 1;
1217 this.slistener.assuming(toDimacs(p));
1218 boolean ret = assume(p);
1219 assert ret;
1220 }
1221 } else {
1222 confl = this.sharedConflict;
1223 }
1224 }
1225 }
1226 if (confl != null) {
1227
1228 this.stats.conflicts++;
1229 this.slistener.conflictFound(confl, decisionLevel(),
1230 this.trail.size());
1231 this.conflictCount.newConflict();
1232
1233 if (decisionLevel() == this.rootLevel) {
1234 if (this.lastConflictMeansUnsat) {
1235
1236 this.unsatExplanationInTermsOfAssumptions = analyzeFinalConflictInTermsOfAssumptions(
1237 confl, assumps, ILits.UNDEFINED);
1238 return Lbool.FALSE;
1239 }
1240 return Lbool.UNDEFINED;
1241 }
1242 int conflictTrailLevel = this.trail.size();
1243
1244 try {
1245 analyze(confl, this.analysisResult);
1246 } catch (TimeoutException e) {
1247 return Lbool.UNDEFINED;
1248 }
1249 assert this.analysisResult.backtrackLevel < decisionLevel();
1250 backjumpLevel = Math.max(this.analysisResult.backtrackLevel,
1251 this.rootLevel);
1252 this.slistener.backjump(backjumpLevel);
1253 cancelUntil(backjumpLevel);
1254 if (backjumpLevel == this.rootLevel) {
1255 this.restarter.onBackjumpToRootLevel();
1256 }
1257 if (confl == this.sharedConflict) {
1258 this.sharedConflict.assertConstraintIfNeeded(this);
1259 this.sharedConflict = null;
1260 }
1261 assert decisionLevel() >= this.rootLevel
1262 && decisionLevel() >= this.analysisResult.backtrackLevel;
1263 if (this.analysisResult.reason == null) {
1264 return Lbool.FALSE;
1265 }
1266 record(this.analysisResult.reason);
1267 this.restarter.newLearnedClause(this.analysisResult.reason,
1268 conflictTrailLevel);
1269 this.analysisResult.reason = null;
1270 decayActivities();
1271 }
1272 } while (this.undertimeout);
1273 return Lbool.UNDEFINED;
1274 }
1275
1276 private Constr preventTheSameDecisionsToBeMade() {
1277 IVecInt clause = new VecInt(nVars());
1278 int p;
1279 for (int i = this.trail.size() - 1; i >= this.rootLevel; i--) {
1280 p = this.trail.get(i);
1281 if (this.voc.getReason(p) == null) {
1282 clause.push(p ^ 1);
1283 }
1284 }
1285 return this.dsfactory.createUnregisteredClause(clause);
1286 }
1287
1288 protected void analyzeAtRootLevel(Constr conflict) {
1289 }
1290
1291 private final IVecInt implied = new VecInt();
1292 private final IVecInt decisions = new VecInt();
1293
1294 private int[] fullmodel;
1295
1296
1297
1298
1299 void modelFound() {
1300 IVecInt tempmodel = new VecInt(nVars());
1301 this.userbooleanmodel = new boolean[realNumberOfVariables()];
1302 this.fullmodel = null;
1303 for (int i = 1; i <= nVars(); i++) {
1304 if (this.voc.belongsToPool(i)) {
1305 int p = this.voc.getFromPool(i);
1306 if (!this.voc.isUnassigned(p)) {
1307 tempmodel.push(this.voc.isSatisfied(p) ? i : -i);
1308 this.userbooleanmodel[i - 1] = this.voc.isSatisfied(p);
1309 if (this.voc.getReason(p) == null && voc.getLevel(p) > 0) {
1310 this.decisions.push(tempmodel.last());
1311 } else {
1312 this.implied.push(tempmodel.last());
1313 }
1314 }
1315 }
1316 }
1317 this.model = new int[tempmodel.size()];
1318 tempmodel.copyTo(this.model);
1319 if (realNumberOfVariables() > nVars()) {
1320 for (int i = nVars() + 1; i <= realNumberOfVariables(); i++) {
1321 if (this.voc.belongsToPool(i)) {
1322 int p = this.voc.getFromPool(i);
1323 if (!this.voc.isUnassigned(p)) {
1324 tempmodel.push(this.voc.isSatisfied(p) ? i : -i);
1325 this.userbooleanmodel[i - 1] = this.voc.isSatisfied(p);
1326 if (this.voc.getReason(p) == null) {
1327 this.decisions.push(tempmodel.last());
1328 } else {
1329 this.implied.push(tempmodel.last());
1330 }
1331 }
1332 }
1333 }
1334 this.fullmodel = new int[tempmodel.size()];
1335 tempmodel.moveTo(this.fullmodel);
1336 } else {
1337 this.fullmodel = this.model;
1338 }
1339 }
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350 private Constr forget(int var) {
1351 boolean satisfied = this.voc.isSatisfied(toInternal(var));
1352 this.voc.forgets(var);
1353 Constr confl;
1354 if (satisfied) {
1355 confl = reduceClausesForFalsifiedLiteral(LiteralsUtils
1356 .toInternal(-var));
1357 } else {
1358 confl = reduceClausesForFalsifiedLiteral(LiteralsUtils
1359 .toInternal(var));
1360 }
1361 return confl;
1362 }
1363
1364
1365
1366
1367
1368
1369
1370
1371 private boolean setAndPropagate(int p) {
1372 if (voc.isUnassigned(p)) {
1373 assert !trail.contains(p);
1374 assert !trail.contains(neg(p));
1375 return assume(p) && propagate() == null;
1376 }
1377 return voc.isSatisfied(p);
1378 }
1379
1380 private int[] prime;
1381
1382 public int[] primeImplicant() {
1383 assert this.qhead == this.trail.size() + this.learnedLiterals.size();
1384 if (this.learnedLiterals.size() > 0) {
1385 this.qhead = trail.size();
1386 }
1387 if (isVerbose()) {
1388 System.out.printf("%s implied: %d, decision: %d %n",
1389 getLogPrefix(), implied.size(), decisions.size());
1390 }
1391 this.prime = new int[realNumberOfVariables() + 1];
1392 int p, d;
1393 for (int i = 0; i < this.prime.length; i++) {
1394 this.prime[i] = 0;
1395 }
1396 boolean noproblem;
1397 for (IteratorInt it = this.implied.iterator(); it.hasNext();) {
1398 d = it.next();
1399 p = toInternal(d);
1400 this.prime[Math.abs(d)] = d;
1401 noproblem = setAndPropagate(p);
1402 assert noproblem;
1403 }
1404 boolean canBeRemoved;
1405 int rightlevel;
1406 int removed = 0;
1407 int propagated = 0;
1408 int tested = 0;
1409 int l2propagation = 0;
1410
1411 for (int i = 0; i < this.decisions.size(); i++) {
1412 d = this.decisions.get(i);
1413 assert !this.voc.isFalsified(toInternal(d));
1414 if (this.voc.isSatisfied(toInternal(d))) {
1415
1416 this.prime[Math.abs(d)] = d;
1417 propagated++;
1418 } else if (setAndPropagate(toInternal(-d))) {
1419 canBeRemoved = true;
1420 tested++;
1421 rightlevel = currentDecisionLevel();
1422 for (int j = i + 1; j < this.decisions.size(); j++) {
1423 l2propagation++;
1424 if (!setAndPropagate(toInternal(this.decisions.get(j)))) {
1425 canBeRemoved = false;
1426 break;
1427 }
1428 }
1429 cancelUntil(rightlevel);
1430 if (canBeRemoved) {
1431
1432 forget(Math.abs(d));
1433 IConstr confl = propagate();
1434 assert confl == null;
1435 removed++;
1436 } else {
1437 this.prime[Math.abs(d)] = d;
1438 cancel();
1439 assert voc.isUnassigned(toInternal(d));
1440 noproblem = setAndPropagate(toInternal(d));
1441 assert noproblem;
1442 }
1443 } else {
1444
1445 this.prime[Math.abs(d)] = d;
1446 cancel();
1447 noproblem = setAndPropagate(toInternal(d));
1448 assert noproblem;
1449 }
1450 }
1451 cancelUntil(0);
1452 int[] implicant = new int[this.prime.length - removed - 1];
1453 int index = 0;
1454 for (int i : this.prime) {
1455 if (i != 0) {
1456 implicant[index++] = i;
1457 }
1458 }
1459 if (isVerbose()) {
1460 System.out.printf("%s prime implicant computation statistics%n",
1461 getLogPrefix());
1462 System.out
1463 .printf("%s implied: %d, decision: %d (removed %d, tested %d, propagated %d), l2 propagation:%d%n",
1464 getLogPrefix(), implied.size(), decisions.size(),
1465 removed, tested, propagated, l2propagation);
1466 }
1467 return implicant;
1468 }
1469
1470 public boolean primeImplicant(int p) {
1471 if (p == 0 || Math.abs(p) > realNumberOfVariables()) {
1472 throw new IllegalArgumentException(
1473 "Use a valid Dimacs var id as argument!");
1474 }
1475 if (this.prime == null) {
1476 throw new UnsupportedOperationException(
1477 "Call the primeImplicant method first!!!");
1478 }
1479 return this.prime[Math.abs(p)] == p;
1480 }
1481
1482 public boolean model(int var) {
1483 if (var <= 0 || var > realNumberOfVariables()) {
1484 throw new IllegalArgumentException(
1485 "Use a valid Dimacs var id as argument!");
1486 }
1487 if (this.userbooleanmodel == null) {
1488 throw new UnsupportedOperationException(
1489 "Call the solve method first!!!");
1490 }
1491 return this.userbooleanmodel[var - 1];
1492 }
1493
1494 public void clearLearntClauses() {
1495 for (Iterator<Constr> iterator = this.learnts.iterator(); iterator
1496 .hasNext();) {
1497 iterator.next().remove(this);
1498 }
1499 this.learnts.clear();
1500 this.learnedLiterals.clear();
1501 }
1502
1503 protected final void reduceDB() {
1504 this.stats.reduceddb++;
1505 this.slistener.cleaning();
1506 this.learnedConstraintsDeletionStrategy.reduce(this.learnts);
1507 System.gc();
1508 }
1509
1510
1511
1512
1513 protected void sortOnActivity() {
1514 this.learnts.sort(this.comparator);
1515 }
1516
1517
1518
1519
1520 protected void decayActivities() {
1521 this.order.varDecayActivity();
1522 claDecayActivity();
1523 }
1524
1525
1526
1527
1528 private void claDecayActivity() {
1529 this.claInc *= this.claDecay;
1530 }
1531
1532
1533
1534
1535 public boolean isSatisfiable() throws TimeoutException {
1536 return isSatisfiable(VecInt.EMPTY);
1537 }
1538
1539
1540
1541
1542 public boolean isSatisfiable(boolean global) throws TimeoutException {
1543 return isSatisfiable(VecInt.EMPTY, global);
1544 }
1545
1546 private double timebegin = 0;
1547
1548 private boolean needToReduceDB;
1549
1550 private ConflictTimerContainer conflictCount;
1551
1552 private transient Timer timer;
1553
1554 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
1555 return isSatisfiable(assumps, false);
1556 }
1557
1558 public final LearnedConstraintsDeletionStrategy fixedSize(final int maxsize) {
1559 return new LearnedConstraintsDeletionStrategy() {
1560
1561 private static final long serialVersionUID = 1L;
1562 private final ConflictTimer aTimer = new ConflictTimerAdapter(
1563 maxsize) {
1564
1565 private static final long serialVersionUID = 1L;
1566
1567 @Override
1568 public void run() {
1569 Solver.this.needToReduceDB = true;
1570 }
1571 };
1572
1573 public void reduce(IVec<Constr> learnedConstrs) {
1574 int i, j, k;
1575 for (i = j = k = 0; i < Solver.this.learnts.size()
1576 && Solver.this.learnts.size() - k > maxsize; i++) {
1577 Constr c = Solver.this.learnts.get(i);
1578 if (c.locked() || c.size() == 2) {
1579 Solver.this.learnts
1580 .set(j++, Solver.this.learnts.get(i));
1581 } else {
1582 c.remove(Solver.this);
1583 k++;
1584 }
1585 }
1586 for (; i < Solver.this.learnts.size(); i++) {
1587 Solver.this.learnts.set(j++, Solver.this.learnts.get(i));
1588 }
1589 if (Solver.this.verbose) {
1590 Solver.this.out.log(getLogPrefix()
1591 + "cleaning " + (Solver.this.learnts.size() - j)
1592 + " clauses out of " + Solver.this.learnts.size());
1593
1594 }
1595 Solver.this.learnts.shrinkTo(j);
1596 }
1597
1598 public void onConflictAnalysis(Constr reason) {
1599
1600
1601 }
1602
1603 public void onClauseLearning(Constr outLearnt) {
1604
1605
1606 }
1607
1608 @Override
1609 public String toString() {
1610 return "Fixed size (" + maxsize
1611 + ") learned constraints deletion strategy";
1612 }
1613
1614 public void init() {
1615 }
1616
1617 public ConflictTimer getTimer() {
1618 return this.aTimer;
1619 }
1620
1621 public void onPropagation(Constr from) {
1622
1623
1624 }
1625 };
1626 }
1627
1628 private LearnedConstraintsDeletionStrategy activityBased(
1629 final ConflictTimer timer) {
1630 return new LearnedConstraintsDeletionStrategy() {
1631
1632 private static final long serialVersionUID = 1L;
1633
1634 private final ConflictTimer freeMem = timer;
1635
1636 public void reduce(IVec<Constr> learnedConstrs) {
1637 sortOnActivity();
1638 int i, j;
1639 for (i = j = 0; i < Solver.this.learnts.size() / 2; i++) {
1640 Constr c = Solver.this.learnts.get(i);
1641 if (c.locked() || c.size() == 2) {
1642 Solver.this.learnts
1643 .set(j++, Solver.this.learnts.get(i));
1644 } else {
1645 c.remove(Solver.this);
1646 }
1647 }
1648 for (; i < Solver.this.learnts.size(); i++) {
1649 Solver.this.learnts.set(j++, Solver.this.learnts.get(i));
1650 }
1651 if (Solver.this.verbose) {
1652 Solver.this.out.log(getLogPrefix()
1653 + "cleaning " + (Solver.this.learnts.size() - j)
1654 + " clauses out of " + Solver.this.learnts.size());
1655
1656 }
1657 Solver.this.learnts.shrinkTo(j);
1658 }
1659
1660 public ConflictTimer getTimer() {
1661 return this.freeMem;
1662 }
1663
1664 @Override
1665 public String toString() {
1666 return "Memory based learned constraints deletion strategy";
1667 }
1668
1669 public void init() {
1670
1671 }
1672
1673 public void onClauseLearning(Constr constr) {
1674
1675
1676 }
1677
1678 public void onConflictAnalysis(Constr reason) {
1679 if (reason.learnt()) {
1680 claBumpActivity(reason);
1681 }
1682 }
1683
1684 public void onPropagation(Constr from) {
1685
1686 }
1687 };
1688 }
1689
1690 private final ConflictTimer memoryTimer = new ConflictTimerAdapter(500) {
1691 private static final long serialVersionUID = 1L;
1692 final long memorybound = Runtime.getRuntime().freeMemory() / 10;
1693
1694 @Override
1695 public void run() {
1696 long freemem = Runtime.getRuntime().freeMemory();
1697
1698 if (freemem < this.memorybound) {
1699
1700 Solver.this.needToReduceDB = true;
1701 }
1702 }
1703 };
1704
1705
1706
1707
1708 public final LearnedConstraintsDeletionStrategy memory_based = activityBased(this.memoryTimer);
1709
1710 private class GlucoseLCDS implements LearnedConstraintsDeletionStrategy {
1711
1712 private static final long serialVersionUID = 1L;
1713 private int[] flags = new int[0];
1714 private int flag = 0;
1715
1716
1717 private final ConflictTimer clauseManagement;
1718
1719 GlucoseLCDS(ConflictTimer timer) {
1720 this.clauseManagement = timer;
1721 }
1722
1723 public void reduce(IVec<Constr> learnedConstrs) {
1724 sortOnActivity();
1725 int i, j;
1726 for (i = j = learnedConstrs.size() / 2; i < learnedConstrs.size(); i++) {
1727 Constr c = learnedConstrs.get(i);
1728 if (c.locked() || c.getActivity() <= 2.0) {
1729 learnedConstrs.set(j++, Solver.this.learnts.get(i));
1730 } else {
1731 c.remove(Solver.this);
1732 }
1733 }
1734 if (Solver.this.verbose) {
1735 Solver.this.out
1736 .log(getLogPrefix()
1737 + "cleaning " + (learnedConstrs.size() - j)
1738 + " clauses out of " + learnedConstrs.size() + " with flag " + this.flag + "/" + Solver.this.stats.conflicts);
1739
1740 }
1741 Solver.this.learnts.shrinkTo(j);
1742
1743 }
1744
1745 public ConflictTimer getTimer() {
1746 return this.clauseManagement;
1747 }
1748
1749 @Override
1750 public String toString() {
1751 return "Glucose learned constraints deletion strategy";
1752 }
1753
1754 public void init() {
1755 final int howmany = Solver.this.voc.nVars();
1756
1757 if (this.flags.length <= howmany) {
1758 this.flags = new int[howmany + 1];
1759 }
1760 this.flag = 0;
1761 this.clauseManagement.reset();
1762 }
1763
1764 public void onClauseLearning(Constr constr) {
1765 int nblevel = computeLBD(constr);
1766 constr.incActivity(nblevel);
1767 }
1768
1769 protected int computeLBD(Constr constr) {
1770 int nblevel = 1;
1771 this.flag++;
1772 int currentLevel;
1773 for (int i = 1; i < constr.size(); i++) {
1774 currentLevel = Solver.this.voc.getLevel(constr.get(i));
1775 if (this.flags[currentLevel] != this.flag) {
1776 this.flags[currentLevel] = this.flag;
1777 nblevel++;
1778 }
1779 }
1780 return nblevel;
1781 }
1782
1783 public void onConflictAnalysis(Constr reason) {
1784
1785 }
1786
1787 public void onPropagation(Constr from) {
1788
1789 }
1790 }
1791
1792 private class Glucose2LCDS extends GlucoseLCDS {
1793
1794
1795
1796
1797 private static final long serialVersionUID = 1L;
1798
1799 Glucose2LCDS(ConflictTimer timer) {
1800 super(timer);
1801 }
1802
1803 @Override
1804 public String toString() {
1805 return "Glucose 2 learned constraints deletion strategy";
1806 }
1807
1808 @Override
1809 public void onPropagation(Constr from) {
1810 if (from.getActivity() > 2.0) {
1811 int nblevel = computeLBD(from);
1812 if (nblevel < from.getActivity()) {
1813 Solver.this.stats.updateLBD++;
1814 from.setActivity(nblevel);
1815 }
1816 }
1817 }
1818
1819 }
1820
1821 private final ConflictTimer lbdTimer = new ConflictTimerAdapter(1000) {
1822 private static final long serialVersionUID = 1L;
1823 private int nbconflict = 0;
1824 private static final int MAX_CLAUSE = 5000;
1825 private static final int INC_CLAUSE = 1000;
1826 private int nextbound = MAX_CLAUSE;
1827
1828 @Override
1829 public void run() {
1830 this.nbconflict += bound();
1831 if (this.nbconflict >= this.nextbound) {
1832 this.nextbound += INC_CLAUSE;
1833
1834
1835
1836 this.nbconflict = 0;
1837 Solver.this.needToReduceDB = true;
1838 }
1839 }
1840
1841 @Override
1842 public void reset() {
1843 super.reset();
1844 this.nextbound = MAX_CLAUSE;
1845 if (this.nbconflict >= this.nextbound) {
1846 this.nbconflict = 0;
1847 Solver.this.needToReduceDB = true;
1848 }
1849 }
1850 };
1851
1852
1853
1854
1855 public final LearnedConstraintsDeletionStrategy glucose = new Glucose2LCDS(
1856 this.lbdTimer);
1857
1858 protected LearnedConstraintsDeletionStrategy learnedConstraintsDeletionStrategy = this.glucose;
1859
1860
1861
1862
1863
1864
1865
1866
1867 public void setLearnedConstraintsDeletionStrategy(
1868 LearnedConstraintsDeletionStrategy lcds) {
1869 if (this.conflictCount != null) {
1870 this.conflictCount.add(lcds.getTimer());
1871 assert this.learnedConstraintsDeletionStrategy != null;
1872 this.conflictCount.remove(this.learnedConstraintsDeletionStrategy
1873 .getTimer());
1874 }
1875 this.learnedConstraintsDeletionStrategy = lcds;
1876 }
1877
1878 private boolean lastConflictMeansUnsat;
1879
1880 public boolean isSatisfiable(IVecInt assumps, boolean global)
1881 throws TimeoutException {
1882 Lbool status = Lbool.UNDEFINED;
1883 boolean alreadylaunched = this.conflictCount != null;
1884 final int howmany = this.voc.nVars();
1885 if (this.mseen.length <= howmany) {
1886 this.mseen = new boolean[howmany + 1];
1887 }
1888 this.trail.ensure(howmany);
1889 this.trailLim.ensure(howmany);
1890 this.learnedLiterals.ensure(howmany);
1891 this.decisions.clear();
1892 this.implied.clear();
1893 this.slistener.init(this);
1894 this.slistener.start();
1895 this.model = null;
1896 this.userbooleanmodel = null;
1897 this.prime = null;
1898 this.unsatExplanationInTermsOfAssumptions = null;
1899 if (!alreadylaunched || !this.keepHot) {
1900 this.order.init();
1901 }
1902 this.learnedConstraintsDeletionStrategy.init();
1903 int learnedLiteralsLimit = this.trail.size();
1904
1905
1906 this.qhead = 0;
1907
1908
1909 for (int i = learnedLiteralsLimit - 1; i >= 0; i--) {
1910 int p = this.trail.get(i);
1911 IVec<Undoable> undos = this.voc.undos(p);
1912 assert undos != null;
1913 for (int size = undos.size(); size > 0; size--) {
1914 undos.last().undo(p);
1915 undos.pop();
1916 }
1917 }
1918
1919 for (IteratorInt iterator = this.learnedLiterals.iterator(); iterator
1920 .hasNext();) {
1921 enqueue(iterator.next());
1922 }
1923
1924
1925 Constr confl = propagate();
1926 if (confl != null) {
1927 analyzeAtRootLevel(confl);
1928 this.slistener.conflictFound(confl, 0, 0);
1929 this.slistener.end(Lbool.FALSE);
1930 cancelUntil(0);
1931 cancelLearntLiterals(learnedLiteralsLimit);
1932 return false;
1933 }
1934
1935
1936 for (IteratorInt iterator = assumps.iterator(); iterator.hasNext();) {
1937 int assump = iterator.next();
1938 int p = this.voc.getFromPool(assump);
1939 if (!this.voc.isSatisfied(p) && !assume(p)
1940 || (confl = propagate()) != null) {
1941 if (confl == null) {
1942 this.slistener.conflictFound(p);
1943 this.unsatExplanationInTermsOfAssumptions = analyzeFinalConflictInTermsOfAssumptions(
1944 null, assumps, p);
1945 this.unsatExplanationInTermsOfAssumptions.push(assump);
1946 } else {
1947 this.slistener.conflictFound(confl, decisionLevel(),
1948 this.trail.size());
1949 this.unsatExplanationInTermsOfAssumptions = analyzeFinalConflictInTermsOfAssumptions(
1950 confl, assumps, ILits.UNDEFINED);
1951 }
1952
1953 this.slistener.end(Lbool.FALSE);
1954 cancelUntil(0);
1955 cancelLearntLiterals(learnedLiteralsLimit);
1956 return false;
1957 }
1958 }
1959 this.rootLevel = decisionLevel();
1960
1961
1962 if (!alreadylaunched || !this.keepHot) {
1963 this.order.init();
1964 }
1965 this.learner.init();
1966
1967 if (!alreadylaunched) {
1968 this.conflictCount = new ConflictTimerContainer();
1969 this.conflictCount.add(this.restarter);
1970 this.conflictCount.add(this.learnedConstraintsDeletionStrategy
1971 .getTimer());
1972 }
1973 boolean firstTimeGlobal = false;
1974 if (this.timeBasedTimeout) {
1975 if (!global || this.timer == null) {
1976 firstTimeGlobal = true;
1977 this.undertimeout = true;
1978 TimerTask stopMe = new TimerTask() {
1979 @Override
1980 public void run() {
1981 Solver.this.undertimeout = false;
1982 }
1983 };
1984 this.timer = new Timer(true);
1985 this.timer.schedule(stopMe, this.timeout);
1986
1987 }
1988 } else {
1989 if (!global || !alreadylaunched) {
1990 firstTimeGlobal = true;
1991 this.undertimeout = true;
1992 ConflictTimer conflictTimeout = new ConflictTimerAdapter(
1993 (int) this.timeout) {
1994 private static final long serialVersionUID = 1L;
1995
1996 @Override
1997 public void run() {
1998 Solver.this.undertimeout = false;
1999 }
2000 };
2001 this.conflictCount.add(conflictTimeout);
2002 }
2003 }
2004 if (!global || firstTimeGlobal) {
2005 this.restarter.init(this.params, this.stats);
2006 this.timebegin = System.currentTimeMillis();
2007 }
2008 this.needToReduceDB = false;
2009
2010
2011 this.lastConflictMeansUnsat = true;
2012
2013 while (status == Lbool.UNDEFINED && this.undertimeout
2014 && this.lastConflictMeansUnsat) {
2015 int before = this.trail.size();
2016 unitClauseProvider.provideUnitClauses(this);
2017 this.stats.importedUnits += this.trail.size() - before;
2018 status = search(assumps);
2019 if (status == Lbool.UNDEFINED) {
2020 this.restarter.onRestart();
2021 this.slistener.restarting();
2022 }
2023 }
2024
2025 cancelUntil(0);
2026 cancelLearntLiterals(learnedLiteralsLimit);
2027 if (!global && this.timeBasedTimeout && this.timer != null) {
2028 this.timer.cancel();
2029 this.timer = null;
2030 }
2031 this.slistener.end(status);
2032 if (!this.undertimeout) {
2033 String message = " Timeout (" + this.timeout
2034 + (this.timeBasedTimeout ? "s" : " conflicts")
2035 + ") exceeded";
2036 throw new TimeoutException(message);
2037 }
2038 if (status == Lbool.UNDEFINED && !this.lastConflictMeansUnsat) {
2039 throw new TimeoutException("Cannot decide the satisfiability");
2040 }
2041
2042
2043
2044 return model != null;
2045 }
2046
2047 public void printInfos(PrintWriter out) {
2048 printInfos(out, prefix);
2049 }
2050
2051 public void printInfos(PrintWriter out, String prefix) {
2052 out.print(prefix);
2053 out.println("constraints type ");
2054 long total = 0;
2055 for (Map.Entry<String, Counter> entry : this.constrTypes.entrySet()) {
2056 out.println(prefix + entry.getKey() + " => " + entry.getValue());
2057 total += entry.getValue().getValue();
2058 }
2059 out.print(prefix);
2060 out.print(total);
2061 out.println(" constraints processed.");
2062 }
2063
2064
2065
2066
2067 public void printLearntClausesInfos(PrintWriter out, String prefix) {
2068 Map<String, Counter> learntTypes = new HashMap<String, Counter>();
2069 for (Iterator<Constr> it = this.learnts.iterator(); it.hasNext();) {
2070 String type = it.next().getClass().getName();
2071 Counter count = learntTypes.get(type);
2072 if (count == null) {
2073 learntTypes.put(type, new Counter());
2074 } else {
2075 count.inc();
2076 }
2077 }
2078 out.print(prefix);
2079 out.println("learnt constraints type ");
2080 for (Map.Entry<String, Counter> entry : learntTypes.entrySet()) {
2081 out.println(prefix + entry.getKey() + " => " + entry.getValue());
2082 }
2083 }
2084
2085 public SolverStats getStats() {
2086 return this.stats;
2087 }
2088
2089
2090
2091
2092
2093
2094 protected void initStats(SolverStats myStats) {
2095 this.stats = myStats;
2096 }
2097
2098
2099
2100
2101
2102
2103 public IOrder getOrder() {
2104 return this.order;
2105 }
2106
2107
2108
2109
2110
2111
2112 public void setOrder(IOrder h) {
2113 this.order = h;
2114 this.order.setLits(this.voc);
2115 }
2116
2117 public ILits getVocabulary() {
2118 return this.voc;
2119 }
2120
2121 public void reset() {
2122 if (this.timer != null) {
2123 this.timer.cancel();
2124 this.timer = null;
2125 }
2126 this.trail.clear();
2127 this.trailLim.clear();
2128 this.qhead = 0;
2129 for (Iterator<Constr> iterator = this.constrs.iterator(); iterator
2130 .hasNext();) {
2131 iterator.next().remove(this);
2132 }
2133 this.constrs.clear();
2134 clearLearntClauses();
2135 this.voc.resetPool();
2136 this.dsfactory.reset();
2137 this.stats.reset();
2138 this.constrTypes.clear();
2139 }
2140
2141 public int nVars() {
2142 if (this.declaredMaxVarId == 0) {
2143 return this.voc.nVars();
2144 }
2145 return this.declaredMaxVarId;
2146 }
2147
2148
2149
2150
2151
2152
2153 protected IConstr addConstr(Constr constr) {
2154 if (constr == null) {
2155 Counter count = this.constrTypes
2156 .get("ignored satisfied constraints");
2157 if (count == null) {
2158 this.constrTypes.put("ignored satisfied constraints",
2159 new Counter());
2160 } else {
2161 count.inc();
2162 }
2163 } else {
2164 this.constrs.push(constr);
2165 String type = constr.getClass().getName();
2166 Counter count = this.constrTypes.get(type);
2167 if (count == null) {
2168 this.constrTypes.put(type, new Counter());
2169 } else {
2170 count.inc();
2171 }
2172 }
2173 return constr;
2174 }
2175
2176 public DataStructureFactory getDSFactory() {
2177 return this.dsfactory;
2178 }
2179
2180 public IVecInt getOutLearnt() {
2181 return this.moutLearnt;
2182 }
2183
2184
2185
2186
2187
2188
2189
2190
2191 public IConstr getIthConstr(int i) {
2192 return this.constrs.get(i);
2193 }
2194
2195
2196
2197
2198
2199
2200
2201 public void printStat(PrintStream out, String prefix) {
2202 printStat(new PrintWriter(out, true), prefix);
2203 }
2204
2205 public void printStat(PrintWriter out) {
2206 printStat(out, prefix);
2207 }
2208
2209 public void printStat(PrintWriter out, String prefix) {
2210 this.stats.printStat(out, prefix);
2211 double cputime = (System.currentTimeMillis() - this.timebegin) / 1000;
2212 out.println(prefix
2213 + "speed (assignments/second)\t: " + this.stats.propagations
2214 / cputime);
2215 this.order.printStat(out, prefix);
2216 printLearntClausesInfos(out, prefix);
2217 }
2218
2219
2220
2221
2222
2223
2224 public String toString(String prefix) {
2225 StringBuffer stb = new StringBuffer();
2226 Object[] objs = { this.dsfactory, this.learner, this.params,
2227 this.order, this.simplifier, this.restarter,
2228 this.learnedConstraintsDeletionStrategy };
2229 stb.append(prefix);
2230 stb.append("--- Begin Solver configuration ---");
2231 stb.append("\n");
2232 for (Object o : objs) {
2233 stb.append(prefix);
2234 stb.append(o.toString());
2235 stb.append("\n");
2236 }
2237 stb.append(prefix);
2238 stb.append("timeout=");
2239 if (this.timeBasedTimeout) {
2240 stb.append(this.timeout / 1000);
2241 stb.append("s\n");
2242 } else {
2243 stb.append(this.timeout);
2244 stb.append(" conflicts\n");
2245 }
2246 stb.append(prefix);
2247 stb.append("DB Simplification allowed=");
2248 stb.append(this.isDBSimplificationAllowed);
2249 stb.append("\n");
2250 stb.append(prefix);
2251 if (isSolverKeptHot()) {
2252 stb.append("Heuristics kept accross calls (keep the solver \"hot\")\n");
2253 stb.append(prefix);
2254 }
2255 stb.append("Listener: ");
2256 stb.append(slistener);
2257 stb.append("\n");
2258 stb.append(prefix);
2259 stb.append("--- End Solver configuration ---");
2260 return stb.toString();
2261 }
2262
2263
2264
2265
2266
2267
2268 @Override
2269 public String toString() {
2270 return toString("");
2271 }
2272
2273 public int getTimeout() {
2274 return (int) (this.timeBasedTimeout ? this.timeout / 1000
2275 : this.timeout);
2276 }
2277
2278
2279
2280
2281 public long getTimeoutMs() {
2282 if (!this.timeBasedTimeout) {
2283 throw new UnsupportedOperationException(
2284 "The timeout is given in number of conflicts!");
2285 }
2286 return this.timeout;
2287 }
2288
2289 public void setExpectedNumberOfClauses(int nb) {
2290 this.constrs.ensure(nb);
2291 }
2292
2293 public Map<String, Number> getStat() {
2294 return this.stats.toMap();
2295 }
2296
2297 public int[] findModel() throws TimeoutException {
2298 if (isSatisfiable()) {
2299 return model();
2300 }
2301
2302
2303 return null;
2304 }
2305
2306 public int[] findModel(IVecInt assumps) throws TimeoutException {
2307 if (isSatisfiable(assumps)) {
2308 return model();
2309 }
2310
2311
2312 return null;
2313 }
2314
2315 public boolean isDBSimplificationAllowed() {
2316 return this.isDBSimplificationAllowed;
2317 }
2318
2319 public void setDBSimplificationAllowed(boolean status) {
2320 this.isDBSimplificationAllowed = status;
2321 }
2322
2323
2324
2325
2326 public int nextFreeVarId(boolean reserve) {
2327 return this.voc.nextFreeVarId(reserve);
2328 }
2329
2330
2331
2332
2333 public IConstr addBlockingClause(IVecInt literals)
2334 throws ContradictionException {
2335 return addClause(literals);
2336 }
2337
2338
2339
2340
2341 public void unset(int p) {
2342
2343
2344 if (this.voc.isUnassigned(p) || this.trail.isEmpty()) {
2345 return;
2346 }
2347 int current = this.trail.last();
2348 while (current != p) {
2349 undoOne();
2350 if (this.trail.isEmpty()) {
2351 return;
2352 }
2353 current = this.trail.last();
2354 }
2355 undoOne();
2356 this.qhead = this.trail.size();
2357 }
2358
2359
2360
2361
2362 public void setLogPrefix(String prefix) {
2363 this.prefix = prefix;
2364 }
2365
2366
2367
2368
2369 public String getLogPrefix() {
2370 return this.prefix;
2371 }
2372
2373
2374
2375
2376 public IVecInt unsatExplanation() {
2377 IVecInt copy = new VecInt(
2378 this.unsatExplanationInTermsOfAssumptions.size());
2379 this.unsatExplanationInTermsOfAssumptions.copyTo(copy);
2380 return copy;
2381 }
2382
2383
2384
2385
2386 public int[] modelWithInternalVariables() {
2387 if (this.model == null) {
2388 throw new UnsupportedOperationException(
2389 "Call the solve method first!!!");
2390 }
2391 int[] nmodel;
2392 if (nVars() == realNumberOfVariables()) {
2393 nmodel = new int[this.model.length];
2394 System.arraycopy(this.model, 0, nmodel, 0, nmodel.length);
2395 } else {
2396 nmodel = new int[this.fullmodel.length];
2397 System.arraycopy(this.fullmodel, 0, nmodel, 0, nmodel.length);
2398 }
2399
2400 return nmodel;
2401 }
2402
2403
2404
2405
2406 public int realNumberOfVariables() {
2407 return this.voc.nVars();
2408 }
2409
2410
2411
2412
2413 public void stop() {
2414 expireTimeout();
2415 }
2416
2417 protected Constr sharedConflict;
2418
2419
2420
2421
2422 public void backtrack(int[] reason) {
2423 IVecInt clause = new VecInt(reason.length);
2424 for (int d : reason) {
2425 clause.push(LiteralsUtils.toInternal(d));
2426 }
2427 this.sharedConflict = this.dsfactory.createUnregisteredClause(clause);
2428 learn(this.sharedConflict);
2429 }
2430
2431
2432
2433
2434 public Lbool truthValue(int literal) {
2435 int p = LiteralsUtils.toInternal(literal);
2436 if (this.voc.isFalsified(p)) {
2437 return Lbool.FALSE;
2438 }
2439 if (this.voc.isSatisfied(p)) {
2440 return Lbool.TRUE;
2441 }
2442 return Lbool.UNDEFINED;
2443 }
2444
2445
2446
2447
2448 public int currentDecisionLevel() {
2449 return decisionLevel();
2450 }
2451
2452
2453
2454
2455 public int[] getLiteralsPropagatedAt(int decisionLevel) {
2456 throw new UnsupportedOperationException("Not implemented yet!");
2457 }
2458
2459
2460
2461
2462 public void suggestNextLiteralToBranchOn(int l) {
2463 throw new UnsupportedOperationException("Not implemented yet!");
2464 }
2465
2466 protected boolean isNeedToReduceDB() {
2467 return this.needToReduceDB;
2468 }
2469
2470 public void setNeedToReduceDB(boolean needToReduceDB) {
2471 this.needToReduceDB = needToReduceDB;
2472 }
2473
2474 public void setLogger(ILogAble out) {
2475 this.out = out;
2476 }
2477
2478 public ILogAble getLogger() {
2479 return this.out;
2480 }
2481
2482 public double[] getVariableHeuristics() {
2483 return this.order.getVariableHeuristics();
2484 }
2485
2486 public IVec<Constr> getLearnedConstraints() {
2487 return this.learnts;
2488 }
2489
2490
2491
2492
2493 public void setLearnedConstraintsDeletionStrategy(ConflictTimer timer,
2494 LearnedConstraintsEvaluationType evaluation) {
2495 if (this.conflictCount != null) {
2496 this.conflictCount.add(timer);
2497 this.conflictCount.remove(this.learnedConstraintsDeletionStrategy
2498 .getTimer());
2499 }
2500 switch (evaluation) {
2501 case ACTIVITY:
2502 this.learnedConstraintsDeletionStrategy = activityBased(timer);
2503 break;
2504 case LBD:
2505 this.learnedConstraintsDeletionStrategy = new GlucoseLCDS(timer);
2506 break;
2507 case LBD2:
2508 this.learnedConstraintsDeletionStrategy = new Glucose2LCDS(timer);
2509 break;
2510 }
2511 if (this.conflictCount != null) {
2512 this.learnedConstraintsDeletionStrategy.init();
2513 }
2514 }
2515
2516
2517
2518
2519 public void setLearnedConstraintsDeletionStrategy(
2520 LearnedConstraintsEvaluationType evaluation) {
2521 ConflictTimer aTimer = this.learnedConstraintsDeletionStrategy
2522 .getTimer();
2523 switch (evaluation) {
2524 case ACTIVITY:
2525 this.learnedConstraintsDeletionStrategy = activityBased(aTimer);
2526 break;
2527 case LBD:
2528 this.learnedConstraintsDeletionStrategy = new GlucoseLCDS(aTimer);
2529 break;
2530 case LBD2:
2531 this.learnedConstraintsDeletionStrategy = new Glucose2LCDS(aTimer);
2532 break;
2533 }
2534 if (this.conflictCount != null) {
2535 this.learnedConstraintsDeletionStrategy.init();
2536 }
2537 }
2538
2539 public boolean isSolverKeptHot() {
2540 return this.keepHot;
2541 }
2542
2543 public void setKeepSolverHot(boolean keepHot) {
2544 this.keepHot = keepHot;
2545 }
2546
2547 private final Comparator<Integer> dimacsLevel = new Comparator<Integer>() {
2548 public int compare(Integer i1, Integer i2) {
2549 return voc.getLevel(Math.abs(i2)) - voc.getLevel(Math.abs(i1));
2550 }
2551 };
2552
2553 public IConstr addClauseOnTheFly(int[] literals) {
2554 List<Integer> lliterals = new ArrayList<Integer>();
2555 for (Integer d : literals) {
2556 lliterals.add(d);
2557 }
2558 Collections.sort(lliterals, dimacsLevel);
2559 IVecInt clause = new VecInt(literals.length);
2560 for (int d : lliterals) {
2561 clause.push(LiteralsUtils.toInternal(d));
2562 }
2563 this.sharedConflict = this.dsfactory.createUnregisteredClause(clause);
2564 this.sharedConflict.register();
2565 addConstr(this.sharedConflict);
2566 IVecInt reason = new VecInt();
2567 this.sharedConflict.calcReasonOnTheFly(ILits.UNDEFINED, trail, reason);
2568 Set<Integer> subset = fromLastDecisionLevel(reason);
2569 while (!trail.isEmpty() && !subset.contains(trail.last())) {
2570 undoOne();
2571 if (!trailLim.isEmpty() && trailLim.last() == trail.size()) {
2572 trailLim.pop();
2573 }
2574 }
2575 return this.sharedConflict;
2576 }
2577
2578 public ISolver getSolvingEngine() {
2579 return this;
2580 }
2581
2582
2583
2584
2585
2586 public IConstr addAtMostOnTheFly(int[] literals, int degree) {
2587 IVecInt clause = new VecInt(literals.length);
2588 for (int d : literals) {
2589 clause.push(LiteralsUtils.toInternal(-d));
2590 }
2591 IVecInt copy = new VecInt(clause.size());
2592 clause.copyTo(copy);
2593 this.sharedConflict = this.dsfactory
2594 .createUnregisteredCardinalityConstraint(copy, literals.length
2595 - degree);
2596 this.sharedConflict.register();
2597 addConstr(this.sharedConflict);
2598
2599
2600 IVecInt reason = new VecInt();
2601 this.sharedConflict.calcReasonOnTheFly(ILits.UNDEFINED, trail, reason);
2602 Set<Integer> subset = fromLastDecisionLevel(reason);
2603 while (!trail.isEmpty() && !subset.contains(trail.last())) {
2604 undoOne();
2605 if (!trailLim.isEmpty() && trailLim.last() == trail.size()) {
2606 trailLim.pop();
2607 }
2608 }
2609 return this.sharedConflict;
2610 }
2611
2612 protected Set<Integer> fromLastDecisionLevel(IVecInt lits) {
2613 Set<Integer> subset = new HashSet<Integer>();
2614 int max = -1, q, level;
2615 for (int i = 0; i < lits.size(); i++) {
2616 q = lits.get(i);
2617 level = voc.getLevel(q);
2618 if (level > max) {
2619 subset.clear();
2620 subset.add(q);
2621 max = level;
2622 } else if (level == max) {
2623 subset.add(q);
2624 }
2625 }
2626 return subset;
2627 }
2628
2629 public void setUnitClauseProvider(UnitClauseProvider ucp) {
2630 this.unitClauseProvider = ucp;
2631 }
2632 }