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.constraints.pb; 31 32 import java.math.BigInteger; 33 34 public final class ConflictMapSwitchToClause extends ConflictMap { 35 36 public static int UpperBound; 37 38 public ConflictMapSwitchToClause(PBConstr cpb, int level) { 39 super(cpb, level); 40 } 41 42 public static IConflict createConflict(PBConstr cpb, int level) { 43 return new ConflictMapSwitchToClause(cpb, level); 44 } 45 46 /** 47 * reduces the constraint defined by wpb until the result of the cutting 48 * plane is a conflict. this reduction returns either a clause if . 49 * 50 * @param litImplied 51 * @param ind 52 * @param reducedCoefs 53 * @param wpb 54 * @return BigInteger.ONE 55 */ 56 @Override 57 protected BigInteger reduceUntilConflict(int litImplied, int ind, 58 BigInteger[] reducedCoefs, IWatchPb wpb) { 59 BigInteger degreeCons = super.reduceUntilConflict(litImplied, ind, 60 reducedCoefs, wpb); 61 // updating of the degree of the conflict 62 int i = 0; 63 for (; i < reducedCoefs.length 64 && reducedCoefs[i].equals(BigInteger.ZERO) && i != ind; i++) { 65 } 66 if (i < reducedCoefs.length) { 67 BigInteger bigCoef = reducedCoefs[i].multiply(this.coefMultCons); 68 if (this.weightedLits.containsKey(wpb.get(i))) { 69 bigCoef = bigCoef.add(this.weightedLits.get(wpb.get(i)) 70 .multiply(this.coefMult)); 71 } 72 if (bigCoef.toString().length() > UpperBound) { 73 // if we deal with really big integers 74 // reducing the constraint to a clause 75 this.numberOfReductions++; 76 this.hasBeenReduced = true; 77 degreeCons = reduceToClause(ind, wpb, reducedCoefs); 78 this.coefMultCons = this.weightedLits.get(litImplied ^ 1); 79 this.coefMult = BigInteger.ONE; 80 } 81 } 82 return degreeCons; 83 } 84 85 private BigInteger reduceToClause(int ind, IWatchPb wpb, 86 BigInteger[] reducedCoefs) { 87 for (int i = 0; i < reducedCoefs.length; i++) { 88 if (i == ind || wpb.getVocabulary().isFalsified(wpb.get(i))) { 89 reducedCoefs[i] = BigInteger.ONE; 90 } else { 91 reducedCoefs[i] = BigInteger.ZERO; 92 } 93 } 94 return BigInteger.ONE; 95 } 96 97 }