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 package org.sat4j.minisat.constraints.cnf;
29
30 import static org.sat4j.core.LiteralsUtils.neg;
31
32 import java.io.Serializable;
33
34 import org.sat4j.minisat.core.Constr;
35 import org.sat4j.minisat.core.ILits;
36 import org.sat4j.minisat.core.UnitPropagationListener;
37 import org.sat4j.specs.IVecInt;
38
39
40
41
42
43
44 public abstract class BinaryClause implements Constr, Serializable {
45
46 private static final long serialVersionUID = 1L;
47
48 private double activity;
49
50 private final ILits voc;
51
52 private int head;
53
54 private int tail;
55
56
57
58
59
60
61
62
63
64 public BinaryClause(IVecInt ps, ILits voc) {
65 assert ps.size() == 2;
66 head = ps.get(0);
67 tail = ps.get(1);
68 this.voc = voc;
69 activity = 0;
70 }
71
72
73
74
75
76
77 public void calcReason(int p, IVecInt outReason) {
78 if (voc.isFalsified(head)) {
79 outReason.push(neg(head));
80 }
81 if (voc.isFalsified(tail)) {
82 outReason.push(neg(tail));
83 }
84 }
85
86
87
88
89
90
91 public void remove() {
92 voc.attaches(neg(head)).remove(this);
93 voc.attaches(neg(tail)).remove(this);
94 }
95
96
97
98
99
100
101 public boolean simplify() {
102 if (voc.isSatisfied(head) || voc.isSatisfied(tail)) {
103 return true;
104 }
105 return false;
106 }
107
108 public boolean propagate(UnitPropagationListener s, int p) {
109 voc.attach(p, this);
110 if (head == neg(p)) {
111 return s.enqueue(tail, this);
112 }
113 assert tail == neg(p);
114 return s.enqueue(head, this);
115 }
116
117
118
119
120 public boolean locked() {
121 return voc.getReason(head) == this || voc.getReason(tail) == this;
122 }
123
124
125
126
127 public double getActivity() {
128 return activity;
129 }
130
131 @Override
132 public String toString() {
133 StringBuffer stb = new StringBuffer();
134 stb.append(Lits.toString(head));
135 stb.append("[");
136 stb.append(voc.valueToString(head));
137 stb.append("]");
138 stb.append(" ");
139 stb.append(Lits.toString(tail));
140 stb.append("[");
141 stb.append(voc.valueToString(tail));
142 stb.append("]");
143 return stb.toString();
144 }
145
146
147
148
149
150
151
152
153
154 public int get(int i) {
155 if (i == 0)
156 return head;
157 assert i == 1;
158 return tail;
159 }
160
161
162
163
164 public void incActivity(double claInc) {
165 activity += claInc;
166 }
167
168
169
170
171 public void rescaleBy(double d) {
172 activity *= d;
173 }
174
175 public int size() {
176 return 2;
177 }
178
179 public void assertConstraint(UnitPropagationListener s) {
180 boolean ret;
181 if (voc.isUnassigned(head)) {
182 ret = s.enqueue(head, this);
183 } else {
184 assert voc.isUnassigned(tail);
185 ret = s.enqueue(tail, this);
186 }
187 assert ret;
188 }
189
190 public ILits getVocabulary() {
191 return voc;
192 }
193
194 public int[] getLits() {
195 int[] tmp = new int[2];
196 tmp[0] = head;
197 tmp[1] = tail;
198 return tmp;
199 }
200
201 @Override
202 public boolean equals(Object obj) {
203 if (obj == null)
204 return false;
205 try {
206 BinaryClause wcl = (BinaryClause) obj;
207 if (wcl.head != head || wcl.tail != tail) {
208 return false;
209 }
210 return true;
211 } catch (ClassCastException e) {
212 return false;
213 }
214 }
215
216 @Override
217 public int hashCode() {
218 long sum = head + tail;
219 return (int) sum / 2;
220 }
221
222 public void register() {
223 voc.attach(neg(head), this);
224 voc.attach(neg(tail), this);
225 }
226 }