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 pseudo boolean algorithms described in:
20 * A fast pseudo-Boolean constraint solver Chai, D.; Kuehlmann, A.
21 * Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
22 * Volume 24, Issue 3, March 2005 Page(s): 305 - 317
23 *
24 * and
25 * Heidi E. Dixon, 2004. Automating Pseudo-Boolean Inference within a DPLL
26 * Framework. Ph.D. Dissertation, University of Oregon.
27 *******************************************************************************/
28 package org.sat4j.pb;
29
30 import java.math.BigInteger;
31
32 import org.sat4j.specs.ContradictionException;
33 import org.sat4j.specs.IConstr;
34 import org.sat4j.specs.ISolver;
35 import org.sat4j.specs.IVec;
36 import org.sat4j.specs.IVecInt;
37
38 /**
39 * A solver able to deal with pseudo boolean constraints.
40 *
41 * @author daniel
42 *
43 */
44 public interface IPBSolver extends ISolver {
45
46 /**
47 * Create a Pseudo-Boolean constraint of the type "at least n or at most n
48 * of those literals must be satisfied"
49 *
50 * @param lits
51 * a set of literals. The vector can be reused since the solver
52 * is not supposed to keep a reference to that vector.
53 * @param coeffs
54 * the coefficients of the literals. The vector can be reused
55 * since the solver is not supposed to keep a reference to that
56 * vector.
57 * @param moreThan
58 * true if it is a constraint >= degree, false if it is a
59 * constraint <= degree
60 * @param d
61 * the degree of the cardinality constraint
62 * @return a reference to the constraint added in the solver, to use in
63 * removeConstr().
64 * @throws ContradictionException
65 * iff the vector of literals is empty or if the constraint is
66 * falsified after unit propagation
67 * @see #removeConstr(IConstr)
68 */
69 IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
70 boolean moreThan, BigInteger d) throws ContradictionException;
71
72 /**
73 * Create a pseudo boolean constraint of the type "at most".
74 *
75 * @param literals
76 * a set of literals The vector can be reused since the solver is
77 * not supposed to keep a reference to that vector.
78 * @param coeffs
79 * the coefficients of the literals. The vector can be reused
80 * since the solver is not supposed to keep a reference to that
81 * vector.
82 * @param degree
83 * the degree of the pseudo-boolean constraint
84 * @return a reference to the constraint added in the solver, to use in
85 * removeConstr().
86 * @throws ContradictionException
87 * iff the constraint is found trivially unsat.
88 * @see #removeConstr(IConstr)
89 * @since 2.3.1
90 */
91
92 IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
93 throws ContradictionException;
94
95 /**
96 * Create a pseudo boolean constraint of the type "at most".
97 *
98 * @param literals
99 * a set of literals The vector can be reused since the solver is
100 * not supposed to keep a reference to that vector.
101 * @param coeffs
102 * the coefficients of the literals. The vector can be reused
103 * since the solver is not supposed to keep a reference to that
104 * vector.
105 * @param degree
106 * the degree of the pseudo-boolean constraint
107 * @return a reference to the constraint added in the solver, to use in
108 * removeConstr().
109 * @throws ContradictionException
110 * iff the constraint is found trivially unsat.
111 * @see #removeConstr(IConstr)
112 * @since 2.3.1
113 */
114
115 IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
116 BigInteger degree) throws ContradictionException;
117
118 /**
119 * Create a pseudo-boolean constraint of the type "at least".
120 *
121 * @param literals
122 * a set of literals. The vector can be reused since the solver
123 * is not supposed to keep a reference to that vector.
124 * @param coeffs
125 * the coefficients of the literals. The vector can be reused
126 * since the solver is not supposed to keep a reference to that
127 * vector.
128 * @param degree
129 * the degree of the pseudo-boolean constraint
130 * @return a reference to the constraint added in the solver, to use in
131 * removeConstr().
132 * @throws ContradictionException
133 * iff the constraint is found trivially unsat.
134 * @see #removeConstr(IConstr)
135 * @since 2.3.1
136 */
137 IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
138 throws ContradictionException;
139
140 /**
141 * Create a pseudo-boolean constraint of the type "at least".
142 *
143 * @param literals
144 * a set of literals. The vector can be reused since the solver
145 * is not supposed to keep a reference to that vector.
146 * @param coeffs
147 * the coefficients of the literals. The vector can be reused
148 * since the solver is not supposed to keep a reference to that
149 * vector.
150 * @param degree
151 * the degree of the pseudo-boolean constraint
152 * @return a reference to the constraint added in the solver, to use in
153 * removeConstr().
154 * @throws ContradictionException
155 * iff the constraint is found trivially unsat.
156 * @see #removeConstr(IConstr)
157 * @since 2.3.1
158 */
159 IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
160 BigInteger degree) throws ContradictionException;
161
162 /**
163 * Create a pseudo-boolean constraint of the type "subset sum".
164 *
165 * @param literals
166 * a set of literals. The vector can be reused since the solver
167 * is not supposed to keep a reference to that vector.
168 * @param coeffs
169 * the coefficients of the literals. The vector can be reused
170 * since the solver is not supposed to keep a reference to that
171 * vector.
172 * @param weight
173 * the number of literals that must be satisfied
174 * @return a reference to the constraint added to the solver. It might
175 * return an object representing a group of constraints.
176 * @throws ContradictionException
177 * iff the constraint is trivially unsatisfiable.
178 * @since 2.3.1
179 */
180 IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
181 throws ContradictionException;
182
183 /**
184 * Create a pseudo-boolean constraint of the type "subset sum".
185 *
186 * @param literals
187 * a set of literals. The vector can be reused since the solver
188 * is not supposed to keep a reference to that vector.
189 * @param coeffs
190 * the coefficients of the literals. The vector can be reused
191 * since the solver is not supposed to keep a reference to that
192 * vector.
193 * @param weight
194 * the number of literals that must be satisfied
195 * @return a reference to the constraint added to the solver. It might
196 * return an object representing a group of constraints.
197 * @throws ContradictionException
198 * iff the constraint is trivially unsatisfiable.
199 * @since 2.3.1
200 */
201 IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
202 BigInteger weight) throws ContradictionException;
203
204 /**
205 * Provide an objective function to the solver.
206 *
207 * @param obj
208 * the objective function
209 */
210 public void setObjectiveFunction(ObjectiveFunction obj);
211
212 /**
213 * Retrieve the objective function from the solver.
214 *
215 * @return the objective function
216 */
217 public ObjectiveFunction getObjectiveFunction();
218 }