1 |
| |
2 |
| |
3 |
| |
4 |
| |
5 |
| |
6 |
| |
7 |
| package org.sat4j.minisat.orders; |
8 |
| |
9 |
| |
10 |
| |
11 |
| |
12 |
| |
13 |
| |
14 |
| public class PureOrder extends VarOrder { |
15 |
| |
16 |
| |
17 |
| |
18 |
| |
19 |
| private static final long serialVersionUID = 1L; |
20 |
| |
21 |
| private final int period; |
22 |
| |
23 |
| private int cpt; |
24 |
| |
25 |
2
| public PureOrder() {
|
26 |
2
| this(20);
|
27 |
| } |
28 |
| |
29 |
2
| public PureOrder(int p) {
|
30 |
2
| period = p;
|
31 |
2
| cpt = period;
|
32 |
| } |
33 |
| |
34 |
| |
35 |
| |
36 |
| |
37 |
| |
38 |
| |
39 |
10258106
| @Override
|
40 |
| public int select() { |
41 |
| |
42 |
10258106
| if (cpt < period) {
|
43 |
9769624
| cpt++;
|
44 |
| } else { |
45 |
| |
46 |
488482
| cpt = 0;
|
47 |
488482
| int nblits = 2 * lits.nVars();
|
48 |
488482
| for (int i = 2; i <= nblits; i++) {
|
49 |
48786380
| if (lits.isUnassigned(i) && lits.watches(i).size() > 0
|
50 |
| && lits.watches(i ^ 1).size() == 0) { |
51 |
257069
| return i;
|
52 |
| } |
53 |
| } |
54 |
| } |
55 |
| |
56 |
10001037
| return super.select();
|
57 |
| } |
58 |
| |
59 |
0
| @Override
|
60 |
| public String toString() { |
61 |
0
| return "tries to first branch on a single phase watched unassigned variable (pure literal if using a CB data structure) else VSIDS from MiniSAT";
|
62 |
| } |
63 |
| } |