1 /*******************************************************************************
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
3 *
4 * All rights reserved. This program and the accompanying materials
5 * are made available under the terms of the Eclipse Public License v1.0
6 * which accompanies this distribution, and is available at
7 * http://www.eclipse.org/legal/epl-v10.html
8 *
9 * Alternatively, the contents of this file may be used under the terms of
10 * either the GNU Lesser General Public License Version 2.1 or later (the
11 * "LGPL"), in which case the provisions of the LGPL are applicable instead
12 * of those above. If you wish to allow use of your version of this file only
13 * under the terms of the LGPL, and not to allow others to use your version of
14 * this file under the terms of the EPL, indicate your decision by deleting
15 * the provisions above and replace them with the notice and other provisions
16 * required by the LGPL. If you do not delete the provisions above, a recipient
17 * may use your version of this file under the terms of the EPL or the LGPL.
18 *
19 * Based on the original MiniSat specification from:
20 *
21 * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22 * Sixth International Conference on Theory and Applications of Satisfiability
23 * Testing, LNCS 2919, pp 502-518, 2003.
24 *
25 * See www.minisat.se for the original solver in C++.
26 *
27 *******************************************************************************/
28 package org.sat4j.minisat.constraints.cnf;
29
30 import java.io.Serializable;
31
32 import org.sat4j.core.VecInt;
33 import org.sat4j.minisat.core.Constr;
34 import org.sat4j.minisat.core.ILits;
35 import org.sat4j.minisat.core.UnitPropagationListener;
36 import org.sat4j.specs.IVecInt;
37
38 /**
39 * @author leberre To change the template for this generated type comment go to
40 * Window>Preferences>Java>Code Generation>Code and Comments
41 */
42 public class BinaryClauses implements Constr, Serializable {
43
44 private static final long serialVersionUID = 1L;
45
46 private final ILits voc;
47
48 private final IVecInt clauses = new VecInt();
49
50 private final int reason;
51
52 private int conflictindex = -1;
53
54 /**
55 *
56 */
57 public BinaryClauses(ILits voc, int p) {
58 this.voc = voc;
59 this.reason = p;
60 }
61
62 public void addBinaryClause(int p) {
63 clauses.push(p);
64 }
65
66 /*
67 * (non-Javadoc)
68 *
69 * @see org.sat4j.minisat.Constr#remove()
70 */
71 public void remove() {
72 // do nothing
73 }
74
75 /*
76 * (non-Javadoc)
77 *
78 * @see org.sat4j.minisat.Constr#propagate(org.sat4j.minisat.UnitPropagationListener,
79 * int)
80 */
81 public boolean propagate(UnitPropagationListener s, int p) {
82 // assert voc.isFalsified(this.reason);
83 voc.attach(p, this);
84 for (int i = 0; i < clauses.size(); i++) {
85 int q = clauses.get(i);
86 if (!s.enqueue(q, this)) {
87 conflictindex = i;
88 return false;
89 }
90 }
91 return true;
92 }
93
94 /*
95 * (non-Javadoc)
96 *
97 * @see org.sat4j.minisat.Constr#simplify()
98 */
99 public boolean simplify() {
100 IVecInt locclauses = clauses;
101 final int size = clauses.size();
102 for (int i = 0; i < size; i++) {
103 if (voc.isSatisfied(locclauses.get(i))) {
104 return true;
105 }
106 if (voc.isFalsified(locclauses.get(i))) {
107 locclauses.delete(i);
108 }
109
110 }
111 return false;
112 }
113
114 /*
115 * (non-Javadoc)
116 *
117 * @see org.sat4j.minisat.Constr#undo(int)
118 */
119 public void undo(int p) {
120 // no to do
121 }
122
123 /*
124 * (non-Javadoc)
125 *
126 * @see org.sat4j.minisat.Constr#calcReason(int, org.sat4j.datatype.VecInt)
127 */
128 public void calcReason(int p, IVecInt outReason) {
129 outReason.push(this.reason ^ 1);
130 if (p == ILits.UNDEFINED) {
131 // int i=0;
132 // while(!voc.isFalsified(clauses.get(i))) {
133 // i++;
134 // }
135 assert conflictindex > -1;
136 outReason.push(clauses.get(conflictindex) ^ 1);
137 }
138 }
139
140 /*
141 * (non-Javadoc)
142 *
143 * @see org.sat4j.minisat.Constr#learnt()
144 */
145 public boolean learnt() {
146 return false;
147 }
148
149 /*
150 * (non-Javadoc)
151 *
152 * @see org.sat4j.minisat.Constr#incActivity(double)
153 */
154 public void incActivity(double claInc) {
155 // TODO Auto-generated method stub
156 }
157
158 /*
159 * (non-Javadoc)
160 *
161 * @see org.sat4j.minisat.Constr#getActivity()
162 */
163 public double getActivity() {
164 // TODO Auto-generated method stub
165 return 0;
166 }
167
168 /*
169 * (non-Javadoc)
170 *
171 * @see org.sat4j.minisat.Constr#locked()
172 */
173 public boolean locked() {
174 return false;
175 }
176
177 /*
178 * (non-Javadoc)
179 *
180 * @see org.sat4j.minisat.Constr#setLearnt()
181 */
182 public void setLearnt() {
183 // TODO Auto-generated method stub
184 }
185
186 /*
187 * (non-Javadoc)
188 *
189 * @see org.sat4j.minisat.Constr#register()
190 */
191 public void register() {
192 // TODO Auto-generated method stub
193 }
194
195 /*
196 * (non-Javadoc)
197 *
198 * @see org.sat4j.minisat.Constr#rescaleBy(double)
199 */
200 public void rescaleBy(double d) {
201 // TODO Auto-generated method stub
202 }
203
204 /*
205 * (non-Javadoc)
206 *
207 * @see org.sat4j.minisat.Constr#size()
208 */
209 public int size() {
210 return clauses.size();
211 }
212
213 /*
214 * (non-Javadoc)
215 *
216 * @see org.sat4j.minisat.Constr#get(int)
217 */
218 public int get(int i) {
219 // TODO Auto-generated method stub
220 throw new UnsupportedOperationException();
221 }
222
223 public void assertConstraint(UnitPropagationListener s) {
224 throw new UnsupportedOperationException();
225 }
226 }