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