View Javadoc

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.constraints.pb;
27  
28  import java.math.BigInteger;
29  
30  import org.sat4j.core.Vec;
31  import org.sat4j.core.VecInt;
32  import org.sat4j.minisat.core.AssertingClauseGenerator;
33  import org.sat4j.minisat.core.Constr;
34  import org.sat4j.minisat.core.DataStructureFactory;
35  import org.sat4j.minisat.core.Handle;
36  import org.sat4j.minisat.core.ILits;
37  import org.sat4j.minisat.core.IOrder;
38  import org.sat4j.minisat.core.LearningStrategy;
39  import org.sat4j.minisat.core.RestartStrategy;
40  import org.sat4j.minisat.core.SearchParams;
41  import org.sat4j.minisat.core.Solver;
42  import org.sat4j.minisat.restarts.MiniSATRestarts;
43  import org.sat4j.specs.IVec;
44  import org.sat4j.specs.IVecInt;
45  
46  /**
47   * @author parrain To change the template for this generated type comment go to
48   *         Window - Preferences - Java - Code Generation - Code and Comments
49   */
50  public class PBSolver<L extends ILits> extends Solver<L> {
51  
52      private static final long serialVersionUID = 1L;
53      
54      /**
55       * @param acg
56       * @param learner
57       * @param dsf
58       */
59      public PBSolver(AssertingClauseGenerator acg, LearningStrategy<L> learner,
60              DataStructureFactory<L> dsf, IOrder<L> order) {
61          super(acg, learner, dsf, new SearchParams(1.5, 100), order,new MiniSATRestarts());
62      }
63  
64      public PBSolver(AssertingClauseGenerator acg, LearningStrategy<L> learner, DataStructureFactory<L> dsf, SearchParams params, IOrder<L> order, RestartStrategy restarter) {
65          super(acg, learner, dsf, params, order, restarter);
66      }
67  
68      public PBSolver(AssertingClauseGenerator acg, LearningStrategy<L> learner, DataStructureFactory<L> dsf, SearchParams params, IOrder<L> order) {
69          super(acg, learner, dsf, params, order,new MiniSATRestarts());
70      }
71  
72      @Override
73      public int analyze(Constr myconfl, Handle<Constr> outLearntRef) {
74  
75          // first literal implied in the conflict
76          int litImplied = trail.last();
77          int currentLevel = voc.getLevel(litImplied);
78          
79          IConflict confl = chooseConflict(myconfl, currentLevel);
80          BigInteger resDegree = confl.getDegree();
81          assert confl.slackConflict().signum() < 0;
82          while (!confl.isAssertive(currentLevel)) {
83              PBConstr constraint = (PBConstr) voc.getReason(litImplied);
84              // result of the resolution is in the conflict (confl)
85              resDegree = confl.resolve(constraint, litImplied, this);
86              assert confl.slackConflict().signum() <= 0;
87              // implication trail is reduced
88              if (trail.size() == 1)
89                  break;
90              undoOne();
91              assert decisionLevel() > 0;
92              litImplied = trail.last();
93              if (voc.getLevel(litImplied) != currentLevel) {
94                  trailLim.pop();
95                  confl.updateSlack(voc.getLevel(litImplied));
96              }
97              assert voc.getLevel(litImplied) <= currentLevel;
98              currentLevel = voc.getLevel(litImplied);
99              assert confl.slackIsCorrect(currentLevel);
100             assert currentLevel == decisionLevel();
101             assert litImplied > 1;
102         }
103 
104         assert currentLevel == decisionLevel();
105         assert decisionLevel() != 0;
106 
107         undoOne();
108 
109         // necessary informations to build a PB-constrinat
110         // are kept from the conflict
111         IVecInt resLits = new VecInt();
112         IVec<BigInteger> resCoefs = new Vec<BigInteger>();
113         confl.buildConstraintFromConflict(resLits, resCoefs);
114 
115         assert resLits.size() == resCoefs.size();
116 
117         if (resLits.size() == 0) {
118             outLearntRef.obj = null;
119             return -1;
120         }
121 
122         // assertive PB-constraint is build and referenced
123         PBConstr resConstr = (PBConstr) dsfactory
124                 .createUnregisteredPseudoBooleanConstraint(resLits, resCoefs,
125                         resDegree);
126 
127         outLearntRef.obj = resConstr;
128         // the conflict give the highest decision level for the backtrack 
129         // (which is less than current level) 
130         assert confl.isAssertive(currentLevel);
131         return confl.getBacktrackLevel(currentLevel);
132     }
133 
134     IConflict chooseConflict(Constr myconfl, int level) {
135         return ConflictMap.createConflict((PBConstr) myconfl, level);
136     }
137 
138     @Override
139     public String toString(String prefix) {
140         return prefix + "Cutting planes based inference ("
141                 + this.getClass().getName() + ")\n" + super.toString(prefix);
142     }
143 
144 }