View Javadoc

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.constraints.pb;
29  
30  import java.math.BigInteger;
31  
32  import org.sat4j.core.Vec;
33  import org.sat4j.minisat.core.ILits;
34  import org.sat4j.specs.ContradictionException;
35  import org.sat4j.specs.IVec;
36  import org.sat4j.specs.IVecInt;
37  
38  public abstract class Pseudos {
39  
40  	public static IDataStructurePB niceCheckedParameters(IVecInt ps,
41  			IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg,
42  			ILits voc) {
43  		assert ps.size() != 0 && ps.size() == bigCoefs.size();
44  		int[] lits = new int[ps.size()];
45  		ps.copyTo(lits);
46  		BigInteger[] bc = new BigInteger[bigCoefs.size()];
47  		bigCoefs.copyTo(bc);
48  		BigInteger bigDegree = Pseudos.niceCheckedParametersForCompetition(
49  				lits, bc, moreThan, bigDeg);
50  
51  		IDataStructurePB mpb = new MapPb(voc.nVars() * 2 + 2);
52  		if (bigDegree.signum() > 0)
53  			bigDegree = mpb.cuttingPlane(lits, bc, bigDegree);
54  		if (bigDegree.signum() > 0)
55  			bigDegree = mpb.saturation();
56  		if (bigDegree.signum() <= 0)
57  			return null;
58  		return mpb;
59  	}
60  
61  	public static BigInteger niceCheckedParametersForCompetition(int[] lits,
62  			BigInteger[] bc, boolean moreThan, BigInteger bigDeg) {
63  		BigInteger bigDegree = bigDeg;
64  		if (!moreThan) {
65  			for (int i = 0; i < lits.length; i++) {
66  				bc[i] = bc[i].negate();
67  			}
68  			bigDegree = bigDegree.negate();
69  		}
70  
71  		for (int i = 0; i < bc.length; i++)
72  			if (bc[i].signum() < 0) {
73  				lits[i] = lits[i] ^ 1;
74  				bc[i] = bc[i].negate();
75  				bigDegree = bigDegree.add(bc[i]);
76  			}
77  
78  		for (int i = 0; i < bc.length; i++)
79  			if (bc[i].compareTo(bigDegree) > 0)
80  				bc[i] = bigDegree;
81  
82  		return bigDegree;
83  
84  	}
85  
86  	public static IDataStructurePB niceParameters(IVecInt ps,
87  			IVec<BigInteger> bigCoefs, boolean moreThan, BigInteger bigDeg,
88  			ILits voc) throws ContradictionException {
89  		// Ajouter les simplifications quand la structure sera d?finitive
90  		if (ps.size() == 0) {
91  			throw new ContradictionException("Creating Empty clause ?");
92  		} else if (ps.size() != bigCoefs.size()) {
93  			throw new IllegalArgumentException(
94  					"Contradiction dans la taille des tableaux ps=" + ps.size()
95  							+ " coefs=" + bigCoefs.size() + ".");
96  		}
97  		return niceCheckedParameters(ps, bigCoefs, moreThan, bigDeg, voc);
98  	}
99  
100 	public static BigInteger niceParametersForCompetition(int[] ps,
101 			BigInteger[] bigCoefs, boolean moreThan, BigInteger bigDeg)
102 			throws ContradictionException {
103 		// Ajouter les simplifications quand la structure sera d?finitive
104 		if (ps.length == 0) {
105 			throw new ContradictionException("Creating Empty clause ?");
106 		} else if (ps.length != bigCoefs.length) {
107 			throw new IllegalArgumentException(
108 					"Contradiction dans la taille des tableaux ps=" + ps.length
109 							+ " coefs=" + bigCoefs.length + ".");
110 		}
111 		return niceCheckedParametersForCompetition(ps, bigCoefs, moreThan,
112 				bigDeg);
113 	}
114 
115 	public static IVec<BigInteger> toVecBigInt(IVecInt vec) {
116 		IVec<BigInteger> bigVec = new Vec<BigInteger>(vec.size());
117 		for (int i = 0; i < vec.size(); ++i)
118 			bigVec.push(BigInteger.valueOf(vec.get(i)));
119 		return bigVec;
120 	}
121 
122 	public static BigInteger toBigInt(int i) {
123 		return BigInteger.valueOf(i);
124 	}
125 
126 }