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