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.orders;
31
32 import java.io.PrintWriter;
33 import java.util.Random;
34
35 import org.sat4j.minisat.core.ILits;
36 import org.sat4j.minisat.core.IOrder;
37 import org.sat4j.minisat.core.IPhaseSelectionStrategy;
38
39
40
41
42 public class RandomWalkDecorator implements IOrder {
43
44 private final VarOrderHeap decorated;
45
46 private double p;
47
48 private static final Random rand = new Random(123456789);
49 private ILits voc;
50 private int nbRandomWalks;
51
52 public RandomWalkDecorator(VarOrderHeap order) {
53 this(order, 0.01);
54 }
55
56 public RandomWalkDecorator(VarOrderHeap order, double p) {
57 this.decorated = order;
58 this.p = p;
59 }
60
61 public void assignLiteral(int q) {
62 this.decorated.assignLiteral(q);
63 }
64
65 public IPhaseSelectionStrategy getPhaseSelectionStrategy() {
66 return this.decorated.getPhaseSelectionStrategy();
67 }
68
69 public double getProbability() {
70 return this.p;
71 }
72
73 public void setProbability(double p) {
74 this.p = p;
75 }
76
77 public void init() {
78 this.decorated.init();
79 }
80
81 public void printStat(PrintWriter out, String prefix) {
82 out.println(prefix + "random walks\t: " + this.nbRandomWalks);
83 this.decorated.printStat(out, prefix);
84 }
85
86 public int select() {
87 if (rand.nextDouble() < this.p) {
88 int var, lit, max;
89
90 while (!this.decorated.heap.empty()) {
91 max = this.decorated.heap.size();
92 var = this.decorated.heap.get(rand.nextInt(max) + 1);
93 lit = getPhaseSelectionStrategy().select(var);
94 if (this.voc.isUnassigned(lit)) {
95 this.nbRandomWalks++;
96 return lit;
97 }
98 }
99 }
100 return this.decorated.select();
101 }
102
103 public void setLits(ILits lits) {
104 this.decorated.setLits(lits);
105 this.voc = lits;
106 this.nbRandomWalks = 0;
107 }
108
109 public void setPhaseSelectionStrategy(IPhaseSelectionStrategy strategy) {
110 this.decorated.setPhaseSelectionStrategy(strategy);
111 }
112
113 public void setVarDecay(double d) {
114 this.decorated.setVarDecay(d);
115 }
116
117 public void undo(int x) {
118 this.decorated.undo(x);
119 }
120
121 public void updateVar(int q) {
122 this.decorated.updateVar(q);
123 }
124
125 public double varActivity(int q) {
126 return this.decorated.varActivity(q);
127 }
128
129 public void varDecayActivity() {
130 this.decorated.varDecayActivity();
131 }
132
133 public void updateVarAtDecisionLevel(int q) {
134 this.decorated.updateVarAtDecisionLevel(q);
135 }
136
137 @Override
138 public String toString() {
139 return this.decorated.toString() + " with random walks " + this.p;
140 }
141
142 public double[] getVariableHeuristics() {
143 return this.decorated.getVariableHeuristics();
144 }
145
146 }