1 package org.sat4j.pb.core;
2
3 import org.sat4j.minisat.core.AssertingClauseGenerator;
4 import org.sat4j.minisat.core.IOrder;
5 import org.sat4j.minisat.core.LearningStrategy;
6 import org.sat4j.minisat.core.RestartStrategy;
7 import org.sat4j.minisat.core.SearchParams;
8
9 public class PBSolverResCP extends PBSolverCP {
10
11
12
13
14 private static final long serialVersionUID = 1L;
15
16 public static final long MAXCONFLICTS = 100000L;
17
18 private long bound;
19
20 public PBSolverResCP(AssertingClauseGenerator acg,
21 LearningStrategy<PBDataStructureFactory> learner,
22 PBDataStructureFactory dsf, IOrder order) {
23 this(acg, learner, dsf, order, MAXCONFLICTS);
24 }
25
26 public PBSolverResCP(AssertingClauseGenerator acg,
27 LearningStrategy<PBDataStructureFactory> learner,
28 PBDataStructureFactory dsf, IOrder order, long bound) {
29 super(acg, learner, dsf, order);
30 this.bound = bound;
31 }
32
33 public PBSolverResCP(AssertingClauseGenerator acg,
34 LearningStrategy<PBDataStructureFactory> learner,
35 PBDataStructureFactory dsf, SearchParams params, IOrder order,
36 RestartStrategy restarter) {
37 super(acg, learner, dsf, params, order, restarter);
38
39 }
40
41 public PBSolverResCP(AssertingClauseGenerator acg,
42 LearningStrategy<PBDataStructureFactory> learner,
43 PBDataStructureFactory dsf, SearchParams params, IOrder order) {
44 super(acg, learner, dsf, params, order);
45
46 }
47
48 @Override
49 boolean someCriteria() {
50 if (stats.conflicts == bound) {
51 this.setSimplifier(NO_SIMPLIFICATION);
52 this.reduceDB();
53 stats.numberOfCP++;
54 return true;
55 } else if (stats.conflicts > bound) {
56 stats.numberOfCP++;
57 return true;
58 } else {
59 stats.numberOfResolution++;
60 return false;
61 }
62 }
63
64 }