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.minisat.constraints.card.AtLeast;
33  import org.sat4j.minisat.core.ILits;
34  import org.sat4j.minisat.core.UnitPropagationListener;
35  import org.sat4j.specs.ContradictionException;
36  import org.sat4j.specs.IVecInt;
37  
38  public final class AtLeastPB extends AtLeast implements PBConstr {
39  
40  	/**
41       * 
42       */
43  	private static final long serialVersionUID = 1L;
44  
45  	private final BigInteger degree;
46  
47  	private AtLeastPB(ILits voc, IVecInt ps, int degree) {
48  		super(voc, ps, degree);
49  		this.degree = BigInteger.valueOf(degree);
50  	}
51  
52  	public static AtLeastPB atLeastNew(UnitPropagationListener s, ILits voc,
53  			IVecInt ps, int n) throws ContradictionException {
54  		int degree = niceParameters(s, voc, ps, n);
55  		if (degree == 0)
56  			return null;
57  		return new AtLeastPB(voc, ps, degree);
58  	}
59  
60  	public static AtLeastPB atLeastNew(ILits voc, IVecInt ps, int n) {
61  		return new AtLeastPB(voc, ps, n);
62  	}
63  
64  	public BigInteger getCoef(int literal) {
65  		return BigInteger.ONE;
66  	}
67  
68  	public BigInteger getDegree() {
69  		return degree;
70  	}
71  
72  	public ILits getVocabulary() {
73  		return voc;
74  	}
75  
76  	public int[] getLits() {
77  		int[] tmp = new int[size()];
78  		System.arraycopy(lits, 0, tmp, 0, size());
79  		return tmp;
80  	}
81  
82  	public BigInteger[] getCoefs() {
83  		BigInteger[] tmp = new BigInteger[size()];
84  		for (int i = 0; i < tmp.length; i++)
85  			tmp[i] = BigInteger.ONE;
86  		return tmp;
87  	}
88  
89  	/**
90       * 
91       */
92  	private boolean learnt = false;
93  
94  	/**
95  	 * D?termine si la contrainte est apprise
96  	 * 
97  	 * @return true si la contrainte est apprise, false sinon
98  	 * @see org.sat4j.specs.IConstr#learnt()
99  	 */
100 	@Override
101 	public boolean learnt() {
102 		return learnt;
103 	}
104 
105 	@Override
106 	public void setLearnt() {
107 		learnt = true;
108 	}
109 
110 	@Override
111 	public void register() {
112 		assert learnt;
113 		// countFalsified();
114 	}
115 
116 	@Override
117 	public void assertConstraint(UnitPropagationListener s) {
118 		for (int i = 0; i < size(); i++) {
119 			if (getVocabulary().isUnassigned(get(i))) {
120 				boolean ret = s.enqueue(get(i), this);
121 				assert ret;
122 			}
123 		}
124 	}
125 
126 	public IVecInt computeAnImpliedClause() {
127 		return null;
128 	}
129 
130 }