Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
13   92   3   1,62
4   44   0,77   8
8     1,25  
1    
 
  ActiveLearning       Line # 38 13 3 76% 0.76
 
  (99)
 
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.IOrder;
31    import org.sat4j.minisat.core.Solver;
32   
33    /**
34    * Learn clauses with a great number of active variables.
35    *
36    * @author leberre
37    */
 
38    public class ActiveLearning<L extends ILits> extends LimitedLearning<L> {
39   
40    private static final long serialVersionUID = 1L;
41   
42    private double percent;
43   
44    private IOrder<L> order;
45   
 
46  102 toggle public ActiveLearning() {
47  102 this(0.95);
48    }
49   
 
50  102 toggle public ActiveLearning(double d) {
51  102 this.percent = d;
52    }
53   
 
54  102 toggle public void setOrder(IOrder<L> order) {
55  102 this.order = order;
56    }
57   
 
58  102 toggle @Override
59    public void setSolver(Solver<L> s) {
60  102 super.setSolver(s);
61  102 this.order = s.getOrder();
62    }
63   
 
64  0 toggle public void setActivityPercent(double d) {
65  0 percent = d;
66    }
67   
 
68  0 toggle public double getActivityPercent() {
69  0 return percent;
70    }
71   
72    /*
73    * (non-Javadoc)
74    *
75    * @see org.sat4j.minisat.LimitedLearning#learningCondition(org.sat4j.minisat.Constr)
76    */
 
77  86109 toggle @Override
78    protected boolean learningCondition(Constr clause) {
79  86109 int nbactivevars = 0;
80  2584116 for (int i = 0; i < clause.size(); i++) {
81  2498007 if (order.varActivity(clause.get(i)) > 1) {
82  2493254 nbactivevars++;
83    }
84    }
85  86109 return nbactivevars > clause.size() * percent;
86    }
87   
 
88  0 toggle @Override
89    public String toString() {
90  0 return "Limit learning to clauses containing active literals ("+percent*100+"%)"; //$NON-NLS-1$
91    }
92    }