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.core.VarActivityListener;
30
31 public interface IConflict extends IDataStructurePB {
32
33 /**
34 * Effectue une resolution avec une contrainte PB. Met a jour le Conflict.
35 *
36 * @param cpb
37 * contrainte avec laquelle on va faire la resolution
38 * @param litImplied
39 * litteral devant etre resolu
40 * @param val
41 * TODO
42 * @return la mise a jour du degre
43 */
44 BigInteger resolve(PBConstr cpb, int litImplied, VarActivityListener val);
45
46 BigInteger slackConflict();
47
48 boolean isAssertive(int dl);
49
50 /**
51 * Reduction d'une contrainte On supprime un litteral non assigne
52 * prioritairement, vrai sinon. En aucun cas on ne supprime litImplied.
53 *
54 * @return mise a jour du degre
55 */
56 public BigInteger reduceInConstraint(WatchPb wpb,
57 final BigInteger[] coefsBis, final int indLitImplied,
58 final BigInteger degreeBis);
59
60 /**
61 * retourne le niveau de backtrack : c'est-?-dire le niveau le plus haut
62 * pour lequel la contrainte est assertive
63 *
64 * @param maxLevel
65 * le plus bas niveau pour lequel la contrainte est assertive
66 * @return the highest level (smaller int) for which the constraint is
67 * assertive.
68 */
69 public int getBacktrackLevel(int maxLevel);
70
71 public void updateSlack(int level);
72 public boolean slackIsCorrect(int decisionLevel);
73
74 }