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 package org.sat4j.minisat.constraints.pb;
26
27 import java.math.BigInteger;
28
29 import org.sat4j.minisat.constraints.cnf.MixableCBClause;
30 import org.sat4j.minisat.core.ILits;
31 import org.sat4j.minisat.core.UnitPropagationListener;
32 import org.sat4j.specs.IVecInt;
33
34 public class MixableCBClausePB extends MixableCBClause implements PBConstr {
35
36 /**
37 *
38 */
39 private static final long serialVersionUID = 1L;
40
41 public MixableCBClausePB(IVecInt ps, ILits voc, boolean learnt) {
42 super(ps, voc, learnt);
43 }
44
45 public MixableCBClausePB(IVecInt ps, ILits voc) {
46 super(ps, voc);
47 }
48
49 public static MixableCBClausePB brandNewClause(UnitPropagationListener s,
50 ILits voc, IVecInt literals) {
51 MixableCBClausePB c = new MixableCBClausePB(literals, voc);
52 c.register();
53 return c;
54 }
55
56 /*
57 * (non-Javadoc)
58 *
59 * @see org.sat4j.minisat.constraints.pb.PBConstr#computeAnImpliedClause()
60 */
61 public IVecInt computeAnImpliedClause() {
62 return null;
63 }
64
65 /*
66 * (non-Javadoc)
67 *
68 * @see org.sat4j.minisat.constraints.pb.PBConstr#getCoef(int)
69 */
70 public BigInteger getCoef(int literal) {
71 return BigInteger.ONE;
72 }
73
74 /*
75 * (non-Javadoc)
76 *
77 * @see org.sat4j.minisat.constraints.pb.PBConstr#getCoefs()
78 */
79 public BigInteger[] getCoefs() {
80 BigInteger[] tmp = new BigInteger[size()];
81 for (int i = 0; i < tmp.length; i++)
82 tmp[i] = BigInteger.ONE;
83 return tmp;
84 }
85
86 /*
87 * (non-Javadoc)
88 *
89 * @see org.sat4j.minisat.constraints.pb.PBConstr#getDegree()
90 */
91 public BigInteger getDegree() {
92 return BigInteger.ONE;
93 }
94
95 /*
96 * (non-Javadoc)
97 *
98 * @see org.sat4j.minisat.constraints.pb.PBConstr#getLits()
99 */
100 public int[] getLits() {
101 int[] tmp = new int[size()];
102 System.arraycopy(lits, 0, tmp, 0, size());
103 return tmp;
104 }
105
106 /*
107 * (non-Javadoc)
108 *
109 * @see org.sat4j.minisat.constraints.pb.PBConstr#getVocabulary()
110 */
111 public ILits getVocabulary() {
112 return voc;
113 }
114
115 /*
116 * (non-Javadoc)
117 *
118 * @see org.sat4j.minisat.core.Constr#assertConstraint(org.sat4j.minisat.core.UnitPropagationListener)
119 */
120 @Override
121 public void assertConstraint(UnitPropagationListener s) {
122 for (int i = 0; i < size(); i++)
123 if (getVocabulary().isUnassigned(get(i))) {
124 boolean ret = s.enqueue(get(i), this);
125 assert ret;
126 break;
127 }
128 }
129
130 }