|
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 |
| } |