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.tools;
29  
30  import org.sat4j.core.VecInt;
31  import org.sat4j.specs.ContradictionException;
32  import org.sat4j.specs.ISolver;
33  import org.sat4j.specs.IVecInt;
34  import org.sat4j.specs.TimeoutException;
35  
36  /**
37   * Computes models with a minimal number (with respect to cardinality) of
38   * negative literals. This is done be adding a constraint on the number of
39   * negative literals each time a model if found (the number of negative literals
40   * occuring in the model minus one).
41   * 
42   * @author leberre
43   * @see org.sat4j.specs.ISolver#addAtMost(IVecInt, int)
44   */
45  public class Minimal4CardinalityModel extends SolverDecorator<ISolver> {
46  
47  	private static final long serialVersionUID = 1L;
48  
49  	/**
50  	 * @param solver
51  	 */
52  	public Minimal4CardinalityModel(ISolver solver) {
53  		super(solver);
54  	}
55  
56  	/*
57  	 * (non-Javadoc)
58  	 * 
59  	 * @see org.sat4j.ISolver#model()
60  	 */
61  	@Override
62  	public int[] model() {
63  		int[] prevmodel = null;
64  		IVecInt vec = new VecInt();
65  		try {
66  			do {
67  				prevmodel = super.model();
68  				vec.clear();
69  				for (int i = 1; i <= nVars(); i++) {
70  					vec.push(-i);
71  				}
72  				int counter = 0;
73  				for (int q : prevmodel) {
74  					if (q < 0) {
75  						counter++;
76  					}
77  				}
78  				addAtMost(vec, counter - 1);
79  			} while (isSatisfiable());
80  		} catch (TimeoutException e) {
81  			throw new IllegalStateException("Solver timed out"); //$NON-NLS-1$
82  		} catch (ContradictionException e) {
83  			// added trivial unsat clauses
84  		}
85  		// restore();
86  		return prevmodel;
87  	}
88  }