|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| AtLeastPB | Line # 36 | 23 | 5 | 60,4% |
0.6041667
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
| (43) | |||
| Result | |||
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN5
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN5
|
1 PASS | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN4
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN4
|
1 PASS | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN7
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN7
|
1 PASS | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata103
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata103
|
1 PASS | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata83
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata83
|
1 PASS | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN6
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN6
|
1 PASS | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata63
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata63
|
1 PASS | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc103
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc103
|
1 PASS | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul5051
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul5051
|
3 FAIL | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc83
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc83
|
1 PASS | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc63
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc63
|
1 PASS | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3536
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3536
|
3 FAIL | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul4041
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul4041
|
3 FAIL | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3031
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3031
|
3 FAIL | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul2021
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul2021
|
3 FAIL | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1011
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1011
|
3 FAIL | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN9
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN9
|
1 PASS | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN8
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN8
|
1 PASS | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1516
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1516
|
3 FAIL | |
|
0.6041667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN10
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN10
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul5060
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul5060
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul4050
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul4050
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul4045
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul4045
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul5055
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul5055
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3540
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3540
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3545
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3545
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul2030
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul2030
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3035
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3035
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3040
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul3040
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1520
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1520
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1525
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1525
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul2025
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul2025
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1015
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1015
|
3 FAIL | |
|
0.29166666
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1020
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testaloul1020
|
3 FAIL | |
|
0.25
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata43
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testndata43
|
1 PASS | |
|
0.25
|
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc43
org.sat4j.minisat.constraints.AbstractPseudoBooleanAndPigeonHoleTest.testncirc43
|
1 PASS | |
|
0.16666667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN56
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN56
|
1 PASS | |
|
0.16666667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN45
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN45
|
1 PASS | |
|
0.16666667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN78
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN78
|
1 PASS | |
|
0.16666667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN67
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN67
|
1 PASS | |
|
0.16666667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN34
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN34
|
1 PASS | |
|
0.16666667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN910
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN910
|
1 PASS | |
|
0.16666667
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN89
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN89
|
1 PASS | |
| 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.constraints.card.AtLeast; | |
| 30 | import org.sat4j.minisat.core.Constr; | |
| 31 | import org.sat4j.minisat.core.ILits; | |
| 32 | import org.sat4j.minisat.core.UnitPropagationListener; | |
| 33 | import org.sat4j.specs.ContradictionException; | |
| 34 | import org.sat4j.specs.IVecInt; | |
| 35 | ||
| 36 | public class AtLeastPB extends AtLeast implements PBConstr { | |
| 37 | ||
| 38 | /** | |
| 39 | * | |
| 40 | */ | |
| 41 | private static final long serialVersionUID = 1L; | |
| 42 | ||
| 43 | private final BigInteger degree; | |
| 44 | ||
| 45 | 9921 |
private AtLeastPB(ILits voc, IVecInt ps, int degree) { |
| 46 | 9921 | super(voc, ps, degree); |
| 47 | 9921 | this.degree = BigInteger.valueOf(degree); |
| 48 | } | |
| 49 | ||
| 50 | 9206 |
public static AtLeastPB atLeastNew(UnitPropagationListener s, ILits voc, |
| 51 | IVecInt ps, int n) throws ContradictionException { | |
| 52 | 9206 | int degree = niceParameters(s, voc, ps, n); |
| 53 | 9206 | if (degree == 0) |
| 54 | 0 | return null; |
| 55 | 9206 | return new AtLeastPB(voc, ps, degree); |
| 56 | } | |
| 57 | ||
| 58 | 715 |
public static AtLeastPB atLeastNew(ILits voc, IVecInt ps, int n) { |
| 59 | 715 | return new AtLeastPB(voc, ps, n); |
| 60 | } | |
| 61 | ||
| 62 | 395797 |
public BigInteger getCoef(int literal) { |
| 63 | 395797 | return BigInteger.ONE; |
| 64 | } | |
| 65 | ||
| 66 | 10490 |
public BigInteger getDegree() { |
| 67 | 10490 | return degree; |
| 68 | } | |
| 69 | ||
| 70 | 203015 |
public ILits getVocabulary() { |
| 71 | 203015 | return voc; |
| 72 | } | |
| 73 | ||
| 74 | 0 |
public int[] getLits() { |
| 75 | 0 | int[] tmp = new int[size()]; |
| 76 | 0 | System.arraycopy(lits, 0, tmp, 0, size()); |
| 77 | 0 | return tmp; |
| 78 | } | |
| 79 | ||
| 80 | 0 |
public BigInteger[] getCoefs() { |
| 81 | 0 | BigInteger[] tmp = new BigInteger[size()]; |
| 82 | 0 | for (int i = 0; i < tmp.length; i++) |
| 83 | 0 | tmp[i] = BigInteger.ONE; |
| 84 | 0 | return tmp; |
| 85 | } | |
| 86 | ||
| 87 | /** | |
| 88 | * | |
| 89 | */ | |
| 90 | private boolean learnt = false; | |
| 91 | ||
| 92 | /** | |
| 93 | * D?termine si la contrainte est apprise | |
| 94 | * | |
| 95 | * @return true si la contrainte est apprise, false sinon | |
| 96 | * @see Constr#learnt() | |
| 97 | */ | |
| 98 | 0 |
@Override |
| 99 | public boolean learnt() { | |
| 100 | 0 | return learnt; |
| 101 | } | |
| 102 | ||
| 103 | 715 |
@Override |
| 104 | public void setLearnt() { | |
| 105 | 715 | learnt = true; |
| 106 | } | |
| 107 | ||
| 108 | 715 |
@Override |
| 109 | public void register() { | |
| 110 | 715 | assert learnt; |
| 111 | // countFalsified(); | |
| 112 | } | |
| 113 | ||
| 114 | 715 |
@Override |
| 115 | public void assertConstraint(UnitPropagationListener s) { | |
| 116 | 203060 | for (int i = 0; i < size(); i++) { |
| 117 | 202345 | if (getVocabulary().isUnassigned(get(i))) { |
| 118 | 8344 | boolean ret = s.enqueue(get(i), this); |
| 119 | 8344 | assert ret; |
| 120 | } | |
| 121 | } | |
| 122 | } | |
| 123 | ||
| 124 | 0 |
public IVecInt computeAnImpliedClause() { |
| 125 | 0 | return null; |
| 126 | } | |
| 127 | ||
| 128 | } | |
|
||||||||||