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 original MiniSat specification from:
20   * 
21   * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22   * Sixth International Conference on Theory and Applications of Satisfiability
23   * Testing, LNCS 2919, pp 502-518, 2003.
24   *
25   * See www.minisat.se for the original solver in C++.
26   * 
27   *******************************************************************************/
28  package org.sat4j.opt;
29  
30  import org.sat4j.core.VecInt;
31  import org.sat4j.specs.ContradictionException;
32  import org.sat4j.specs.IConstr;
33  import org.sat4j.specs.ISolver;
34  import org.sat4j.specs.IVecInt;
35  import org.sat4j.specs.TimeoutException;
36  
37  /**
38   * Computes a solution that satisfies the maximum of clauses.
39   * 
40   * @author daniel
41   * 
42   */
43  public final class MaxSatDecorator extends AbstractSelectorVariablesDecorator {
44  
45  	/**
46       * 
47       */
48  	private static final long serialVersionUID = 1L;
49  
50  	public MaxSatDecorator(ISolver solver) {
51  		super(solver);
52  	}
53  
54  	@Override
55  	public void setExpectedNumberOfClauses(int nb) {
56  		super.setExpectedNumberOfClauses(nb);
57  		lits.ensure(nb);
58  	}
59  
60  	@Override
61  	public IConstr addClause(IVecInt literals) throws ContradictionException {
62  		int newvar = nborigvars + ++nbnewvar;
63  		lits.push(newvar);
64  		literals.push(newvar);
65  		return super.addClause(literals);
66  	}
67  
68  	@Override
69  	public void reset() {
70  		nbnewvar = 0;
71  		lits.clear();
72  		super.reset();
73  		prevConstr = null;
74  	}
75  
76  	public boolean hasNoObjectiveFunction() {
77  		return false;
78  	}
79  
80  	public boolean nonOptimalMeansSatisfiable() {
81  		return false;
82  	}
83  
84  	public Number calculateObjective() {
85  		calculateObjectiveValue();
86  		return counter;
87  	}
88  
89  	private final IVecInt lits = new VecInt();
90  
91  	private int counter;
92  
93  	private IConstr prevConstr;
94  
95  	/**
96  	 * @since 2.1
97  	 */
98  	public void discardCurrentSolution() throws ContradictionException {
99  		if (prevConstr != null) {
100 			super.removeSubsumedConstr(prevConstr);
101 		}
102 		prevConstr = super.addAtMost(lits, counter - 1);
103 	}
104 
105 	@Override
106 	public boolean admitABetterSolution(IVecInt assumps)
107 			throws TimeoutException {
108 
109 		boolean result = super.admitABetterSolution(assumps);
110 		if (!result) {
111 			if (prevConstr != null) {
112 				super.removeConstr(prevConstr);
113 				prevConstr = null;
114 			}
115 		}
116 		return result;
117 	}
118 
119 	public void discard() throws ContradictionException {
120 		discardCurrentSolution();
121 	}
122 
123 	/**
124 	 * @since 2.1
125 	 */
126 	public Number getObjectiveValue() {
127 		return counter;
128 	}
129 
130 	@Override
131 	void calculateObjectiveValue() {
132 		counter = 0;
133 		for (int q : prevfullmodel) {
134 			if (q > nborigvars) {
135 				counter++;
136 			}
137 		}
138 	}
139 
140 	/**
141 	 * @since 2.1
142 	 */
143 	public void forceObjectiveValueTo(Number forcedValue)
144 			throws ContradictionException {
145 		super.addAtMost(lits, forcedValue.intValue());
146 	}
147 
148 }