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.core;
29  
30  import org.sat4j.core.Vec;
31  import org.sat4j.minisat.core.Constr;
32  import org.sat4j.minisat.core.IOrder;
33  import org.sat4j.minisat.core.LearningStrategy;
34  import org.sat4j.minisat.core.Pair;
35  import org.sat4j.minisat.core.RestartStrategy;
36  import org.sat4j.minisat.core.SearchParams;
37  import org.sat4j.minisat.restarts.MiniSATRestarts;
38  import org.sat4j.pb.constraints.pb.ConflictMap;
39  import org.sat4j.pb.constraints.pb.IConflict;
40  import org.sat4j.pb.constraints.pb.PBConstr;
41  import org.sat4j.specs.IVec;
42  import org.sat4j.specs.TimeoutException;
43  
44  /**
45   * @author parrain To change the template for this generated type comment go to
46   *         Window - Preferences - Java - Code Generation - Code and Comments
47   */
48  public class PBSolverCP extends PBSolver {
49  
50  	private static final long serialVersionUID = 1L;
51  
52  	/**
53  	 * @param acg
54  	 * @param learner
55  	 * @param dsf
56  	 */
57  	public PBSolverCP(LearningStrategy<PBDataStructureFactory> learner,
58  			PBDataStructureFactory dsf, IOrder order) {
59  		super(learner, dsf, new SearchParams(1.5, 100), order,
60  				new MiniSATRestarts());
61  	}
62  
63  	public PBSolverCP(LearningStrategy<PBDataStructureFactory> learner,
64  			PBDataStructureFactory dsf, SearchParams params, IOrder order,
65  			RestartStrategy restarter) {
66  		super(learner, dsf, params, order, restarter);
67  	}
68  
69  	public PBSolverCP(LearningStrategy<PBDataStructureFactory> learner,
70  			PBDataStructureFactory dsf, SearchParams params, IOrder order) {
71  		super(learner, dsf, params, order, new MiniSATRestarts());
72  	}
73  
74  	@Override
75  	public void analyze(Constr myconfl, Pair results) throws TimeoutException {
76  		if (someCriteria())
77  			analyzeCP(myconfl, results);
78  		else
79  			super.analyze(myconfl, results);
80  	}
81  
82  	public void analyzeCP(Constr myconfl, Pair results) throws TimeoutException {
83  		int litImplied = trail.last();
84  		int currentLevel = voc.getLevel(litImplied);
85  		IConflict confl = chooseConflict((PBConstr) myconfl, currentLevel);
86  		assert confl.slackConflict().signum() < 0;
87  		while (!confl.isAssertive(currentLevel)) {
88  			if (!undertimeout) {
89  				throw new TimeoutException();
90  			}
91  			PBConstr constraint = (PBConstr) voc.getReason(litImplied);
92  			// result of the resolution is in the conflict (confl)
93  			confl.resolve(constraint, litImplied, this);
94  			updateNumberOfReductions(confl);
95  			assert confl.slackConflict().signum() <= 0;
96  			// implication trail is reduced
97  			if (trail.size() == 1)
98  				break;
99  			undoOne();
100 			// assert decisionLevel() >= 0;
101 			if (decisionLevel() == 0)
102 				break;
103 			litImplied = trail.last();
104 			if (voc.getLevel(litImplied) != currentLevel) {
105 				trailLim.pop();
106 				confl.updateSlack(voc.getLevel(litImplied));
107 			}
108 			assert voc.getLevel(litImplied) <= currentLevel;
109 			currentLevel = voc.getLevel(litImplied);
110 			assert confl.slackIsCorrect(currentLevel);
111 			assert currentLevel == decisionLevel();
112 			assert litImplied > 1;
113 		}
114 		assert confl.isAssertive(currentLevel) || trail.size() == 1
115 				|| decisionLevel() == 0;
116 
117 		assert currentLevel == decisionLevel();
118 		undoOne();
119 
120 		updateNumberOfReducedLearnedConstraints(confl);
121 		// necessary informations to build a PB-constraint
122 		// are kept from the conflict
123 		if ((confl.size() == 0)
124 				|| ((decisionLevel() == 0 || trail.size() == 0) && confl
125 						.slackConflict().signum() < 0)) {
126 			results.reason = null;
127 			results.backtrackLevel = -1;
128 			return;
129 		}
130 
131 		// assertive PB-constraint is build and referenced
132 		PBConstr resConstr = (PBConstr) dsfactory
133 				.createUnregisteredPseudoBooleanConstraint(confl);
134 
135 		results.reason = resConstr;
136 		getSearchListener().learn(resConstr);
137 
138 		// the conflict give the highest decision level for the backtrack
139 		// (which is less than current level)
140 		// assert confl.isAssertive(currentLevel);
141 		if (decisionLevel() == 0 || trail.size() == 0)
142 			results.backtrackLevel = -1;
143 		else
144 			results.backtrackLevel = confl.getBacktrackLevel(currentLevel);
145 	}
146 
147 	IConflict chooseConflict(PBConstr myconfl, int level) {
148 		return ConflictMap.createConflict(myconfl, level);
149 	}
150 
151 	@Override
152 	public String toString(String prefix) {
153 		return prefix + "Cutting planes based inference ("
154 				+ this.getClass().getName() + ")\n" + super.toString(prefix);
155 	}
156 
157 	private final IVec<String> conflictVariables = new Vec<String>();
158 	private final IVec<String> conflictConstraints = new Vec<String>();
159 
160 	void initExplanation() {
161 		conflictVariables.clear();
162 		conflictConstraints.clear();
163 	}
164 
165 	boolean someCriteria() {
166 		return true;
167 	}
168 
169 	protected void updateNumberOfReductions(IConflict confl) {
170 	}
171 
172 	protected void updateNumberOfReducedLearnedConstraints(IConflict confl) {
173 	}
174 
175 }