1 /*
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3 *
4 * Based on the original minisat specification from:
5 *
6 * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7 * Sixth International Conference on Theory and Applications of Satisfiability
8 * Testing, LNCS 2919, pp 502-518, 2003.
9 *
10 * This library is free software; you can redistribute it and/or modify it under
11 * the terms of the GNU Lesser General Public License as published by the Free
12 * Software Foundation; either version 2.1 of the License, or (at your option)
13 * any later version.
14 *
15 * This library is distributed in the hope that it will be useful, but WITHOUT
16 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17 * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18 * details.
19 *
20 * You should have received a copy of the GNU Lesser General Public License
21 * along with this library; if not, write to the Free Software Foundation, Inc.,
22 * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23 *
24 */
25
26 package org.sat4j.minisat.constraints.cnf;
27
28 import java.io.Serializable;
29
30 import org.sat4j.core.VecInt;
31 import org.sat4j.minisat.core.Constr;
32 import org.sat4j.minisat.core.ILits;
33 import org.sat4j.minisat.core.UnitPropagationListener;
34 import org.sat4j.specs.IVecInt;
35
36 /**
37 * @author leberre To change the template for this generated type comment go to
38 * Window>Preferences>Java>Code Generation>Code and Comments
39 */
40 public class BinaryClauses implements Constr, Serializable {
41
42 private static final long serialVersionUID = 1L;
43
44 private final ILits voc;
45
46 private final IVecInt clauses = new VecInt();
47
48 private final int reason;
49
50 private int conflictindex = -1;
51
52 /**
53 *
54 */
55 public BinaryClauses(ILits voc, int p) {
56 this.voc = voc;
57 this.reason = p;
58 }
59
60 public void addBinaryClause(int p) {
61 clauses.push(p);
62 }
63
64 /*
65 * (non-Javadoc)
66 *
67 * @see org.sat4j.minisat.Constr#remove()
68 */
69 public void remove() {
70 // do nothing
71 }
72
73 /*
74 * (non-Javadoc)
75 *
76 * @see org.sat4j.minisat.Constr#propagate(org.sat4j.minisat.UnitPropagationListener,
77 * int)
78 */
79 public boolean propagate(UnitPropagationListener s, int p) {
80 assert voc.isFalsified(this.reason);
81 voc.watch(p, this);
82 for (int i = 0; i < clauses.size(); i++) {
83 int q = clauses.get(i);
84 if (!s.enqueue(q, this)) {
85 conflictindex = i;
86 return false;
87 }
88 }
89 return true;
90 }
91
92 /*
93 * (non-Javadoc)
94 *
95 * @see org.sat4j.minisat.Constr#simplify()
96 */
97 public boolean simplify() {
98 IVecInt locclauses = clauses;
99 final int size = clauses.size();
100 for (int i = 0; i < size; i++) {
101 if (voc.isSatisfied(locclauses.get(i))) {
102 return true;
103 }
104 if (voc.isFalsified(locclauses.get(i))) {
105 locclauses.delete(i);
106 }
107
108 }
109 return false;
110 }
111
112 /*
113 * (non-Javadoc)
114 *
115 * @see org.sat4j.minisat.Constr#undo(int)
116 */
117 public void undo(int p) {
118 // no to do
119 }
120
121 /*
122 * (non-Javadoc)
123 *
124 * @see org.sat4j.minisat.Constr#calcReason(int, org.sat4j.datatype.VecInt)
125 */
126 public void calcReason(int p, IVecInt outReason) {
127 outReason.push(this.reason ^ 1);
128 if (p == ILits.UNDEFINED) {
129 // int i=0;
130 // while(!voc.isFalsified(clauses.get(i))) {
131 // i++;
132 // }
133 assert conflictindex > -1;
134 outReason.push(clauses.get(conflictindex) ^ 1);
135 }
136 }
137
138 /*
139 * (non-Javadoc)
140 *
141 * @see org.sat4j.minisat.Constr#learnt()
142 */
143 public boolean learnt() {
144 return false;
145 }
146
147 /*
148 * (non-Javadoc)
149 *
150 * @see org.sat4j.minisat.Constr#incActivity(double)
151 */
152 public void incActivity(double claInc) {
153 // TODO Auto-generated method stub
154 }
155
156 /*
157 * (non-Javadoc)
158 *
159 * @see org.sat4j.minisat.Constr#getActivity()
160 */
161 public double getActivity() {
162 // TODO Auto-generated method stub
163 return 0;
164 }
165
166 /*
167 * (non-Javadoc)
168 *
169 * @see org.sat4j.minisat.Constr#locked()
170 */
171 public boolean locked() {
172 return false;
173 }
174
175 /*
176 * (non-Javadoc)
177 *
178 * @see org.sat4j.minisat.Constr#setLearnt()
179 */
180 public void setLearnt() {
181 // TODO Auto-generated method stub
182 }
183
184 /*
185 * (non-Javadoc)
186 *
187 * @see org.sat4j.minisat.Constr#register()
188 */
189 public void register() {
190 // TODO Auto-generated method stub
191 }
192
193 /*
194 * (non-Javadoc)
195 *
196 * @see org.sat4j.minisat.Constr#rescaleBy(double)
197 */
198 public void rescaleBy(double d) {
199 // TODO Auto-generated method stub
200 }
201
202 /*
203 * (non-Javadoc)
204 *
205 * @see org.sat4j.minisat.Constr#size()
206 */
207 public int size() {
208 return clauses.size();
209 }
210
211 /*
212 * (non-Javadoc)
213 *
214 * @see org.sat4j.minisat.Constr#get(int)
215 */
216 public int get(int i) {
217 // TODO Auto-generated method stub
218 throw new UnsupportedOperationException();
219 }
220
221 public void assertConstraint(UnitPropagationListener s) {
222 throw new UnsupportedOperationException();
223 }
224 }