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.LinkedList;
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
43
44 public class TabuListDecorator implements IOrder {
45
46 private final VarOrderHeap decorated;
47
48 private final int tabuSize;
49
50 private ILits voc;
51 private int lastVar = -1;
52
53 private final LinkedList<Integer> tabuList = new LinkedList<Integer>();
54
55 public TabuListDecorator(VarOrderHeap order) {
56 this(order, 10);
57 }
58
59 public TabuListDecorator(VarOrderHeap order, int tabuSize) {
60 this.decorated = order;
61 this.tabuSize = tabuSize;
62 }
63
64 public void assignLiteral(int q) {
65 this.decorated.assignLiteral(q);
66 }
67
68 public IPhaseSelectionStrategy getPhaseSelectionStrategy() {
69 return this.decorated.getPhaseSelectionStrategy();
70 }
71
72 public void init() {
73 this.decorated.init();
74 this.lastVar = -1;
75 }
76
77 public void printStat(PrintWriter out, String prefix) {
78 out.println(prefix + "tabu list size\t: " + this.tabuSize);
79 this.decorated.printStat(out, prefix);
80 }
81
82 public int select() {
83 int lit = this.decorated.select();
84 if (lit == ILits.UNDEFINED) {
85 int var;
86 do {
87 if (this.tabuList.isEmpty()) {
88 return ILits.UNDEFINED;
89 }
90 var = this.tabuList.removeFirst();
91 } while (!this.voc.isUnassigned(var << 1));
92 return getPhaseSelectionStrategy().select(var);
93 }
94 this.lastVar = lit >> 1;
95 return lit;
96 }
97
98 public void setLits(ILits lits) {
99 this.decorated.setLits(lits);
100 this.voc = lits;
101 }
102
103 public void setPhaseSelectionStrategy(IPhaseSelectionStrategy strategy) {
104 this.decorated.setPhaseSelectionStrategy(strategy);
105 }
106
107 public void setVarDecay(double d) {
108 this.decorated.setVarDecay(d);
109 }
110
111 public void undo(int x) {
112 if (this.tabuList.size() == this.tabuSize) {
113 int var = this.tabuList.removeFirst();
114 this.decorated.undo(var);
115 }
116 if (x == this.lastVar) {
117 this.tabuList.add(x);
118 this.lastVar = -1;
119 } else {
120 this.decorated.undo(x);
121 }
122 }
123
124 public void updateVar(int q) {
125 this.decorated.updateVar(q);
126 }
127
128 public double varActivity(int q) {
129 return this.decorated.varActivity(q);
130 }
131
132 public void varDecayActivity() {
133 this.decorated.varDecayActivity();
134 }
135
136 public void updateVarAtDecisionLevel(int q) {
137 this.decorated.updateVarAtDecisionLevel(q);
138 }
139
140 @Override
141 public String toString() {
142 return this.decorated.toString() + " with tabu list of size "
143 + this.tabuSize;
144 }
145
146 public double[] getVariableHeuristics() {
147 return this.decorated.getVariableHeuristics();
148 }
149
150 }