|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| LimitedLearning | Line # 40 | 20 | 2 | 81,8% |
0.8181818
|
||||||||||||||||||||||||||||||||||||||||||||||||||||
| (123) | |||
| Result | |||
|
0.6969697
|
org.sat4j.ModelIteratorTest.testModelIterator
org.sat4j.ModelIteratorTest.testModelIterator
|
1 PASS | |
|
0.5151515
|
org.sat4j.ModelIteratorTest.testIsSatisfiableVecInt
org.sat4j.ModelIteratorTest.testIsSatisfiableVecInt
|
1 PASS | |
|
0.5151515
|
org.sat4j.ModelIteratorTest.testCardModel
org.sat4j.ModelIteratorTest.testCardModel
|
1 PASS | |
|
0.5151515
|
org.sat4j.ModelIteratorTest.testIncModel
org.sat4j.ModelIteratorTest.testIncModel
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN5
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN5
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN7
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN7
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN6
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN6
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN9
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN9
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN8
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN8
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN10
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN10
|
3 FAIL | |
|
0.42424244
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg1
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg1
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg2
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg2
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT12
org.sat4j.minisat.AbstractM2Test.testAim50SAT12
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH49
org.sat4j.minisat.AbstractM2Test.testJNH49
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT13
org.sat4j.minisat.AbstractM2Test.testAim50SAT13
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT14
org.sat4j.minisat.AbstractM2Test.testAim50SAT14
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testHole6
org.sat4j.minisat.AbstractM2Test.testHole6
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT15
org.sat4j.minisat.AbstractM2Test.testAim50SAT15
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testHole7
org.sat4j.minisat.AbstractM2Test.testHole7
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testHole8
org.sat4j.minisat.AbstractM2Test.testHole8
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT9
org.sat4j.minisat.AbstractM2Test.testAim50SAT9
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testHole9
org.sat4j.minisat.AbstractM2Test.testHole9
|
3 FAIL | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT10
org.sat4j.minisat.AbstractM2Test.testAim50SAT10
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT11
org.sat4j.minisat.AbstractM2Test.testAim50SAT11
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH41
org.sat4j.minisat.AbstractM2Test.testJNH41
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT4
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT4
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH42
org.sat4j.minisat.AbstractM2Test.testJNH42
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH43
org.sat4j.minisat.AbstractM2Test.testJNH43
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT6
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT6
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH44
org.sat4j.minisat.AbstractM2Test.testJNH44
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT7
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT7
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH45
org.sat4j.minisat.AbstractM2Test.testJNH45
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT16
org.sat4j.minisat.AbstractM2Test.testAim50SAT16
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH46
org.sat4j.minisat.AbstractM2Test.testJNH46
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT1
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT1
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH47
org.sat4j.minisat.AbstractM2Test.testJNH47
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT2
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT2
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH48
org.sat4j.minisat.AbstractM2Test.testJNH48
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT3
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT3
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT5
org.sat4j.minisat.AbstractM2Test.testAim50SAT5
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT4
org.sat4j.minisat.AbstractM2Test.testAim50SAT4
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT7
org.sat4j.minisat.AbstractM2Test.testAim50SAT7
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT6
org.sat4j.minisat.AbstractM2Test.testAim50SAT6
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT1
org.sat4j.minisat.AbstractM2Test.testAim50SAT1
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT2
org.sat4j.minisat.AbstractM2Test.testAim50SAT2
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH23
org.sat4j.minisat.AbstractM2Test.testJNH23
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH24
org.sat4j.minisat.AbstractM2Test.testJNH24
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH21
org.sat4j.minisat.AbstractM2Test.testJNH21
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH22
org.sat4j.minisat.AbstractM2Test.testJNH22
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH19
org.sat4j.minisat.AbstractM2Test.testJNH19
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH20
org.sat4j.minisat.AbstractM2Test.testJNH20
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH17
org.sat4j.minisat.AbstractM2Test.testJNH17
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH18
org.sat4j.minisat.AbstractM2Test.testJNH18
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH15
org.sat4j.minisat.AbstractM2Test.testJNH15
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH16
org.sat4j.minisat.AbstractM2Test.testJNH16
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH13
org.sat4j.minisat.AbstractM2Test.testJNH13
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH14
org.sat4j.minisat.AbstractM2Test.testJNH14
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH11
org.sat4j.minisat.AbstractM2Test.testJNH11
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH12
org.sat4j.minisat.AbstractM2Test.testJNH12
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH9
org.sat4j.minisat.AbstractM2Test.testJNH9
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH10
org.sat4j.minisat.AbstractM2Test.testJNH10
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH40
org.sat4j.minisat.AbstractM2Test.testJNH40
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH39
org.sat4j.minisat.AbstractM2Test.testJNH39
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH38
org.sat4j.minisat.AbstractM2Test.testJNH38
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH37
org.sat4j.minisat.AbstractM2Test.testJNH37
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH36
org.sat4j.minisat.AbstractM2Test.testJNH36
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH35
org.sat4j.minisat.AbstractM2Test.testJNH35
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH34
org.sat4j.minisat.AbstractM2Test.testJNH34
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH33
org.sat4j.minisat.AbstractM2Test.testJNH33
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH32
org.sat4j.minisat.AbstractM2Test.testJNH32
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH31
org.sat4j.minisat.AbstractM2Test.testJNH31
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH30
org.sat4j.minisat.AbstractM2Test.testJNH30
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH29
org.sat4j.minisat.AbstractM2Test.testJNH29
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH28
org.sat4j.minisat.AbstractM2Test.testJNH28
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH27
org.sat4j.minisat.AbstractM2Test.testJNH27
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH26
org.sat4j.minisat.AbstractM2Test.testJNH26
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH25
org.sat4j.minisat.AbstractM2Test.testJNH25
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi12
org.sat4j.minisat.AbstractM2Test.testIi12
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi13
org.sat4j.minisat.AbstractM2Test.testIi13
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi14
org.sat4j.minisat.AbstractM2Test.testIi14
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi15
org.sat4j.minisat.AbstractM2Test.testIi15
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi8
org.sat4j.minisat.AbstractM2Test.testIi8
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi9
org.sat4j.minisat.AbstractM2Test.testIi9
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi10
org.sat4j.minisat.AbstractM2Test.testIi10
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi11
org.sat4j.minisat.AbstractM2Test.testIi11
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi4
org.sat4j.minisat.AbstractM2Test.testIi4
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi5
org.sat4j.minisat.AbstractM2Test.testIi5
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi6
org.sat4j.minisat.AbstractM2Test.testIi6
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi7
org.sat4j.minisat.AbstractM2Test.testIi7
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT8
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT8
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi1
org.sat4j.minisat.AbstractM2Test.testIi1
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi2
org.sat4j.minisat.AbstractM2Test.testIi2
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi3
org.sat4j.minisat.AbstractM2Test.testIi3
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH6
org.sat4j.minisat.AbstractM2Test.testJNH6
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH5
org.sat4j.minisat.AbstractM2Test.testJNH5
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH8
org.sat4j.minisat.AbstractM2Test.testJNH8
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH7
org.sat4j.minisat.AbstractM2Test.testJNH7
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH2
org.sat4j.minisat.AbstractM2Test.testJNH2
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH1
org.sat4j.minisat.AbstractM2Test.testJNH1
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH4
org.sat4j.minisat.AbstractM2Test.testJNH4
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testJNH3
org.sat4j.minisat.AbstractM2Test.testJNH3
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi22
org.sat4j.minisat.AbstractM2Test.testIi22
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi21
org.sat4j.minisat.AbstractM2Test.testIi21
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi24
org.sat4j.minisat.AbstractM2Test.testIi24
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi23
org.sat4j.minisat.AbstractM2Test.testIi23
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi17
org.sat4j.minisat.AbstractM2Test.testIi17
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi16
org.sat4j.minisat.AbstractM2Test.testIi16
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi20
org.sat4j.minisat.AbstractM2Test.testIi20
|
1 PASS | |
|
0.42424244
|
org.sat4j.minisat.AbstractM2Test.testIi18
org.sat4j.minisat.AbstractM2Test.testIi18
|
1 PASS | |
|
0.36363637
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN4
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN4
|
1 PASS | |
|
0.36363637
|
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg3
org.sat4j.minisat.constraints.AbstractRandomCardProblemsTest.testRndDeg3
|
1 PASS | |
|
0.36363637
|
org.sat4j.minisat.AbstractM2Test.testJNH50
org.sat4j.minisat.AbstractM2Test.testJNH50
|
1 PASS | |
|
0.36363637
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT8
org.sat4j.minisat.AbstractM2Test.testAim50SAT8
|
1 PASS | |
|
0.36363637
|
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT5
org.sat4j.minisat.AbstractM2Test.testAim50UNSAT5
|
1 PASS | |
|
0.36363637
|
org.sat4j.minisat.AbstractM2Test.testAim50SAT3
org.sat4j.minisat.AbstractM2Test.testAim50SAT3
|
1 PASS | |
|
0.33333334
|
org.sat4j.minisat.constraints.pb.WatchPbTest.testNormalize
org.sat4j.minisat.constraints.pb.WatchPbTest.testNormalize
|
1 PASS | |
|
0.18181819
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN56
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN56
|
1 PASS | |
|
0.18181819
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN45
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN45
|
1 PASS | |
|
0.18181819
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN78
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN78
|
1 PASS | |
|
0.18181819
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN67
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN67
|
1 PASS | |
|
0.18181819
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN34
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN34
|
1 PASS | |
|
0.18181819
|
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN910
org.sat4j.minisat.constraints.AbstractPigeonHoleWithCardinalityTest.testPN910
|
1 PASS | |
|
0.18181819
|
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 | ||
| 26 | package org.sat4j.minisat.learning; | |
| 27 | ||
| 28 | import org.sat4j.minisat.core.Constr; | |
| 29 | import org.sat4j.minisat.core.ILits; | |
| 30 | import org.sat4j.minisat.core.LearningStrategy; | |
| 31 | import org.sat4j.minisat.core.Solver; | |
| 32 | import org.sat4j.minisat.core.VarActivityListener; | |
| 33 | ||
| 34 | /** | |
| 35 | * Learn only clauses which size is smaller than a percentage of the number of | |
| 36 | * variables. | |
| 37 | * | |
| 38 | * @author leberre | |
| 39 | */ | |
| 40 | public class LimitedLearning<L extends ILits> implements LearningStrategy<L> { | |
| 41 | ||
| 42 | private static final long serialVersionUID = 1L; | |
| 43 | ||
| 44 | private final NoLearningButHeuristics<L> none; | |
| 45 | ||
| 46 | private final MiniSATLearning<L> all; | |
| 47 | ||
| 48 | private int maxpercent; | |
| 49 | ||
| 50 | private L lits; | |
| 51 | ||
| 52 | private int bound; | |
| 53 | ||
| 54 | 205 |
public LimitedLearning() { |
| 55 | 205 | this(10); |
| 56 | } | |
| 57 | ||
| 58 | 1128 |
public LimitedLearning(int percent) { |
| 59 | 1128 | maxpercent = percent; |
| 60 | 1128 | none = new NoLearningButHeuristics<L>(); |
| 61 | 1128 | all = new MiniSATLearning<L>(); |
| 62 | } | |
| 63 | ||
| 64 | 0 |
public void setLimit(int percent) { |
| 65 | 0 | maxpercent = percent; |
| 66 | } | |
| 67 | ||
| 68 | 0 |
public int getLimit() { |
| 69 | 0 | return maxpercent; |
| 70 | } | |
| 71 | ||
| 72 | 1128 |
public void setSolver(Solver<L> s) { |
| 73 | 1128 | this.lits = s.getVocabulary(); |
| 74 | 1128 | setVarActivityListener(s); |
| 75 | 1128 | all.setDataStructureFactory(s.getDSFactory()); |
| 76 | } | |
| 77 | ||
| 78 | 164465757 |
public void learns(Constr constr) { |
| 79 | 164465757 | if (learningCondition(constr)) { |
| 80 | 104703 | all.learns(constr); |
| 81 | } else { | |
| 82 | 164361054 | none.learns(constr); |
| 83 | } | |
| 84 | } | |
| 85 | ||
| 86 | 164379648 |
protected boolean learningCondition(Constr constr) { |
| 87 | 164379648 | return constr.size() <= bound; |
| 88 | } | |
| 89 | ||
| 90 | 972 |
public void init() { |
| 91 | 972 | setBound(lits.realnVars() * maxpercent / 100); |
| 92 | 972 | all.init(); |
| 93 | 972 | none.init(); |
| 94 | } | |
| 95 | ||
| 96 | 1075 |
protected void setBound(int newbound) { |
| 97 | 1075 | bound = newbound; |
| 98 | } | |
| 99 | ||
| 100 | 0 |
@Override |
| 101 | public String toString() { | |
| 102 | 0 | return "Limit learning to clauses of size smaller or equal to " //$NON-NLS-1$ |
| 103 | + maxpercent + "% of the number of variables"; //$NON-NLS-1$ | |
| 104 | } | |
| 105 | ||
| 106 | 1128 |
public void setVarActivityListener(VarActivityListener s) { |
| 107 | 1128 | none.setVarActivityListener(s); |
| 108 | 1128 | all.setVarActivityListener(s); |
| 109 | } | |
| 110 | } | |
|
||||||||||