1 |
| |
2 |
| |
3 |
| |
4 |
| |
5 |
| |
6 |
| |
7 |
| package org.sat4j.minisat.constraints.cnf; |
8 |
| |
9 |
| import java.io.Serializable; |
10 |
| |
11 |
| import org.sat4j.minisat.core.Constr; |
12 |
| import org.sat4j.minisat.core.ILits; |
13 |
| import org.sat4j.minisat.core.Undoable; |
14 |
| import org.sat4j.minisat.core.UnitPropagationListener; |
15 |
| import org.sat4j.specs.IVecInt; |
16 |
| |
17 |
| |
18 |
| |
19 |
| |
20 |
| public class CBClause implements Constr, Undoable, Serializable { |
21 |
| |
22 |
| private static final long serialVersionUID = 1L; |
23 |
| |
24 |
| protected int falsified; |
25 |
| |
26 |
| private boolean learnt; |
27 |
| |
28 |
| protected final int[] lits; |
29 |
| |
30 |
| protected final ILits voc; |
31 |
| |
32 |
| private double activity; |
33 |
| |
34 |
249668
| public static CBClause brandNewClause(UnitPropagationListener s, ILits voc,
|
35 |
| IVecInt literals) { |
36 |
249668
| CBClause c = new CBClause(literals, voc);
|
37 |
249668
| c.register();
|
38 |
249668
| return c;
|
39 |
| } |
40 |
| |
41 |
| |
42 |
| |
43 |
| |
44 |
9056099
| public CBClause(IVecInt ps, ILits voc, boolean learnt) {
|
45 |
9056099
| this.learnt = learnt;
|
46 |
9056099
| this.lits = new int[ps.size()];
|
47 |
9056099
| this.voc = voc;
|
48 |
9056099
| ps.moveTo(this.lits);
|
49 |
| } |
50 |
| |
51 |
9056099
| public CBClause(IVecInt ps, ILits voc) {
|
52 |
9056099
| this(ps, voc, false);
|
53 |
| } |
54 |
| |
55 |
| |
56 |
| |
57 |
| |
58 |
| |
59 |
| |
60 |
0
| public void remove() {
|
61 |
0
| for (int i = 0; i < lits.length; i++) {
|
62 |
0
| voc.watches(lits[i] ^ 1).remove(this);
|
63 |
| } |
64 |
| } |
65 |
| |
66 |
| |
67 |
| |
68 |
| |
69 |
| |
70 |
| |
71 |
| |
72 |
1162534493
| public boolean propagate(UnitPropagationListener s, int p) {
|
73 |
1162534493
| voc.undos(p).push(this);
|
74 |
1162534493
| falsified++;
|
75 |
| assert falsified != lits.length; |
76 |
1162534493
| if (falsified == lits.length - 1) {
|
77 |
| |
78 |
528741493
| for (int i = 0; i < lits.length; i++) {
|
79 |
1119182651
| if (!voc.isFalsified(lits[i])) {
|
80 |
513388719
| return s.enqueue(lits[i], this);
|
81 |
| } |
82 |
| } |
83 |
| |
84 |
| |
85 |
| |
86 |
15352774
| return false;
|
87 |
| } |
88 |
633793000
| return true;
|
89 |
| } |
90 |
| |
91 |
| |
92 |
| |
93 |
| |
94 |
| |
95 |
| |
96 |
0
| public boolean simplify() {
|
97 |
0
| for (int p : lits) {
|
98 |
0
| if (voc.isSatisfied(p)) {
|
99 |
0
| return true;
|
100 |
| } |
101 |
| } |
102 |
0
| return false;
|
103 |
| } |
104 |
| |
105 |
| |
106 |
| |
107 |
| |
108 |
| |
109 |
| |
110 |
1162636243
| public void undo(int p) {
|
111 |
1162636243
| falsified--;
|
112 |
| } |
113 |
| |
114 |
| |
115 |
| |
116 |
| |
117 |
| |
118 |
| |
119 |
| |
120 |
144099900
| public void calcReason(int p, IVecInt outReason) {
|
121 |
| assert outReason.size() == 0; |
122 |
144099900
| for (int q : lits) {
|
123 |
| assert voc.isFalsified(q) || q == p; |
124 |
790766230
| if (voc.isFalsified(q)) {
|
125 |
661994193
| outReason.push(q ^ 1);
|
126 |
| } |
127 |
| } |
128 |
| assert (p == ILits.UNDEFINED) || (outReason.size() == lits.length - 1); |
129 |
| } |
130 |
| |
131 |
| |
132 |
| |
133 |
| |
134 |
| |
135 |
| |
136 |
144099900
| public boolean learnt() {
|
137 |
144099900
| return learnt;
|
138 |
| } |
139 |
| |
140 |
| |
141 |
| |
142 |
| |
143 |
| |
144 |
| |
145 |
7779697
| public void incActivity(double claInc) {
|
146 |
7779697
| activity += claInc;
|
147 |
| } |
148 |
| |
149 |
| |
150 |
| |
151 |
| |
152 |
| |
153 |
| |
154 |
7779697
| public double getActivity() {
|
155 |
7779697
| return activity;
|
156 |
| } |
157 |
| |
158 |
| |
159 |
| |
160 |
| |
161 |
| |
162 |
| |
163 |
0
| public boolean locked() {
|
164 |
0
| return voc.getReason(lits[0]) == this;
|
165 |
| } |
166 |
| |
167 |
| |
168 |
| |
169 |
| |
170 |
| |
171 |
| |
172 |
8753407
| public void setLearnt() {
|
173 |
8753407
| learnt = true;
|
174 |
| } |
175 |
| |
176 |
| |
177 |
| |
178 |
| |
179 |
| |
180 |
| |
181 |
345550
| public void register() {
|
182 |
345550
| for (int p : lits) {
|
183 |
1568168
| voc.watch(p ^ 1, this);
|
184 |
| } |
185 |
345550
| if (learnt) {
|
186 |
21429
| for (int p : lits) {
|
187 |
522909
| if (voc.isFalsified(p)) {
|
188 |
501480
| voc.undos(p ^ 1).push(this);
|
189 |
501480
| falsified++;
|
190 |
| } |
191 |
| } |
192 |
| assert falsified == lits.length - 1; |
193 |
| } |
194 |
| } |
195 |
| |
196 |
| |
197 |
| |
198 |
| |
199 |
| |
200 |
| |
201 |
1057
| public void rescaleBy(double d) {
|
202 |
1057
| activity *= d;
|
203 |
| } |
204 |
| |
205 |
| |
206 |
| |
207 |
| |
208 |
| |
209 |
| |
210 |
227516682
| public int size() {
|
211 |
227516682
| return lits.length;
|
212 |
| } |
213 |
| |
214 |
| |
215 |
| |
216 |
| |
217 |
| |
218 |
| |
219 |
211129550
| public int get(int i) {
|
220 |
211129550
| return lits[i];
|
221 |
| } |
222 |
| |
223 |
| |
224 |
| |
225 |
| |
226 |
| |
227 |
| |
228 |
8713348
| public void assertConstraint(UnitPropagationListener s) {
|
229 |
| assert voc.isUnassigned(lits[0]); |
230 |
8713348
| boolean ret = s.enqueue(lits[0], this);
|
231 |
| assert ret; |
232 |
| } |
233 |
| |
234 |
0
| @Override
|
235 |
| public String toString() { |
236 |
0
| StringBuffer stb = new StringBuffer();
|
237 |
0
| for (int i = 0; i < lits.length; i++) {
|
238 |
0
| stb.append(lits[i]);
|
239 |
0
| stb.append("[");
|
240 |
0
| stb.append(voc.valueToString(lits[i]));
|
241 |
0
| stb.append("]");
|
242 |
0
| stb.append(" ");
|
243 |
| } |
244 |
0
| return stb.toString();
|
245 |
| } |
246 |
| } |