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(lits,bc,moreThan,bigDeg); 
49  	
50  	    IDataStructurePB mpb = new MapPb(voc.nVars()*2+2);
51  	    if (bigDegree.signum() > 0)
52  	        bigDegree = mpb.cuttingPlane(lits, bc, bigDegree);
53  	    if (bigDegree.signum() > 0)
54  	        bigDegree = mpb.saturation();
55  	    if (bigDegree.signum() <= 0)
56  	        return null;
57  	    return mpb;
58  	}
59  
60  	public static BigInteger niceCheckedParametersForCompetition(int[] lits,
61  	        BigInteger[] bc, boolean moreThan, BigInteger bigDeg) {
62  	    BigInteger bigDegree = bigDeg;
63  	    if (!moreThan) {
64  	        for (int i = 0; i < lits.length; i++) {
65  	            bc[i] = bc[i].negate();
66  	        }
67  	        bigDegree = bigDegree.negate();
68  	    }
69  	
70  	    for (int i = 0; i < bc.length; i++)
71  	        if (bc[i].signum() < 0) {
72  	            lits[i] = lits[i] ^ 1;
73  	            bc[i] = bc[i].negate();
74  	            bigDegree = bigDegree.add(bc[i]);
75  	        }
76  	    
77  	    for (int i = 0; i < bc.length; i++)
78  	        if (bc[i].compareTo(bigDegree) > 0) 
79  	        	bc[i] = bigDegree;
80  	        
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, bigDeg);
112 	}
113 
114 	public static IVec<BigInteger> toVecBigInt(IVecInt vec) {
115 	    IVec<BigInteger> bigVec = new Vec<BigInteger>(vec.size());
116 	    for (int i = 0; i < vec.size(); ++i)
117 	        bigVec.push(BigInteger.valueOf(vec.get(i)));
118 	    return bigVec;
119 	}
120 
121 }