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 TernaryClauses implements Constr, Serializable {
41
42 private static final long serialVersionUID = 1L;
43
44 private final IVecInt stubs = new VecInt();
45
46 private final ILits voc;
47
48 private final int phead;
49
50 public TernaryClauses(ILits voc, int p) {
51 this.voc = voc;
52 this.phead = p;
53 }
54
55 public void addTernaryClause(int a, int b) {
56 stubs.push(a);
57 stubs.push(b);
58 }
59
60 /*
61 * (non-Javadoc)
62 *
63 * @see org.sat4j.minisat.Constr#remove()
64 */
65 public void remove() {
66
67 }
68
69 /*
70 * (non-Javadoc)
71 *
72 * @see org.sat4j.minisat.Constr#propagate(org.sat4j.minisat.UnitPropagationListener,
73 * int)
74 */
75 public boolean propagate(UnitPropagationListener s, int p) {
76 assert voc.isSatisfied(p);
77 assert voc.isFalsified(phead);
78 voc.watch(p, this);
79 for (int i = 0; i < stubs.size(); i += 2) {
80 int a = stubs.get(i);
81 int b = stubs.get(i + 1);
82 if (voc.isSatisfied(a) || voc.isSatisfied(b)) {
83 continue;
84 }
85 if (voc.isFalsified(a) && !s.enqueue(b, this)) {
86 return false;
87 } else if (voc.isFalsified(b) && !s.enqueue(a, this)) {
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 return false;
101 }
102
103 /*
104 * (non-Javadoc)
105 *
106 * @see org.sat4j.minisat.Constr#undo(int)
107 */
108 public void undo(int p) {
109 }
110
111 /*
112 * (non-Javadoc)
113 *
114 * @see org.sat4j.minisat.Constr#calcReason(int, org.sat4j.datatype.VecInt)
115 */
116 public void calcReason(int p, IVecInt outReason) {
117 assert voc.isFalsified(this.phead);
118 if (p == ILits.UNDEFINED) {
119 int i = 0;
120 while (!voc.isFalsified(stubs.get(i))
121 || !voc.isFalsified(stubs.get(i + 1))) {
122 i += 2;
123 }
124 outReason.push(this.phead ^ 1);
125 outReason.push(stubs.get(i) ^ 1);
126 outReason.push(stubs.get(i + 1) ^ 1);
127 } else {
128 outReason.push(this.phead ^ 1);
129 int i = 0;
130 while ((stubs.get(i) != p) || (!voc.isFalsified(stubs.get(i ^ 1)))) {
131 i++;
132 }
133 assert !voc.isFalsified(stubs.get(i));
134 outReason.push(stubs.get(i ^ 1) ^ 1);
135 assert voc.isFalsified(stubs.get(i ^ 1));
136 }
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 }
156
157 /*
158 * (non-Javadoc)
159 *
160 * @see org.sat4j.minisat.Constr#getActivity()
161 */
162 public double getActivity() {
163 return 0;
164 }
165
166 /*
167 * (non-Javadoc)
168 *
169 * @see org.sat4j.minisat.Constr#locked()
170 */
171 public boolean locked() {
172 // TODO Auto-generated method stub
173 return false;
174 }
175
176 /*
177 * (non-Javadoc)
178 *
179 * @see org.sat4j.minisat.Constr#setLearnt()
180 */
181 public void setLearnt() {
182
183 }
184
185 /*
186 * (non-Javadoc)
187 *
188 * @see org.sat4j.minisat.Constr#register()
189 */
190 public void register() {
191
192 }
193
194 /*
195 * (non-Javadoc)
196 *
197 * @see org.sat4j.minisat.Constr#rescaleBy(double)
198 */
199 public void rescaleBy(double d) {
200
201 }
202
203 /*
204 * (non-Javadoc)
205 *
206 * @see org.sat4j.minisat.Constr#size()
207 */
208 public int size() {
209 return stubs.size();
210 }
211
212 /*
213 * (non-Javadoc)
214 *
215 * @see org.sat4j.minisat.Constr#get(int)
216 */
217 public int get(int i) {
218 throw new UnsupportedOperationException();
219 }
220
221 public void assertConstraint(UnitPropagationListener s) {
222 throw new UnsupportedOperationException();
223 }
224 }