Logo Search packages:      
Sourcecode: sat4j version File versions

DimacsOutputSolver.java

/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
*
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v1.0
* which accompanies this distribution, and is available at
* http://www.eclipse.org/legal/epl-v10.html
*
* Alternatively, the contents of this file may be used under the terms of
* either the GNU Lesser General Public License Version 2.1 or later (the
* "LGPL"), in which case the provisions of the LGPL are applicable instead
* of those above. If you wish to allow use of your version of this file only
* under the terms of the LGPL, and not to allow others to use your version of
* this file under the terms of the EPL, indicate your decision by deleting
* the provisions above and replace them with the notice and other provisions
* required by the LGPL. If you do not delete the provisions above, a recipient
* may use your version of this file under the terms of the EPL or the LGPL.
* 
* Based on the original MiniSat specification from:
* 
* An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
* Sixth International Conference on Theory and Applications of Satisfiability
* Testing, LNCS 2919, pp 502-518, 2003.
*
* See www.minisat.se for the original solver in C++.
* 
*******************************************************************************/
package org.sat4j.tools;

import java.io.ObjectInputStream;
import java.io.PrintStream;
import java.io.PrintWriter;
import java.util.Map;

import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IConstr;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVec;
import org.sat4j.specs.IVecInt;
import org.sat4j.specs.IteratorInt;
import org.sat4j.specs.TimeoutException;

/**
 * Solver used to display in a writer the CNF instance in Dimacs format.
 * 
 * That solver is useful to produce CNF files to be used by third party solvers.
 * 
 * @author leberre
 * 
 */
00051 public class DimacsOutputSolver implements ISolver {

    /**
     * 
     */
    private static final long serialVersionUID = 1L;

    private transient PrintWriter out;

    private int nbvars;

    private int nbclauses;

    private boolean fixedNbClauses = false;

    private boolean firstConstr = true;
    
    public DimacsOutputSolver() {
        this(new PrintWriter(System.out, true));
    }

    public DimacsOutputSolver(PrintWriter pw) {
        out = pw;
    }

    private void readObject(ObjectInputStream stream) {
        out = new PrintWriter(System.out, true);
    }

00080     public int newVar() {
        return 0;
    }

00084     public int newVar(int howmany) {
        out.print("p cnf " + howmany);
        nbvars = howmany;
        return 0;
    }

00090     public void setExpectedNumberOfClauses(int nb) {
        out.println(" " + nb);
        nbclauses = nb;
        fixedNbClauses = true;
    }

00096     public IConstr addClause(IVecInt literals) throws ContradictionException {
        if (firstConstr) {
            if (!fixedNbClauses) {
                out.println(" XXXXXX");
            }
            firstConstr = false;
        }
        for (IteratorInt iterator = literals.iterator();iterator.hasNext();)
            out.print(iterator.next() + " ");
        out.println("0");
        return null;        
    }

00109     public boolean removeConstr(IConstr c) {
        throw new UnsupportedOperationException();
    }

00113     public void addAllClauses(IVec<IVecInt> clauses)
            throws ContradictionException {
        throw new UnsupportedOperationException();
    }

00118     public IConstr addAtMost(IVecInt literals, int degree)
            throws ContradictionException {
        if (degree > 1) {
            throw new UnsupportedOperationException(
                    "Not a clausal problem! degree " + degree);
        }
        assert degree == 1;
        if (firstConstr) {
            if (!fixedNbClauses) {
                out.println("XXXXXX");
            }
            firstConstr = false;
        }
        for (int i = 0; i <= literals.size(); i++) {
            for (int j = i + 1; j < literals.size(); j++) {
                out.println("" + (-literals.get(i)) + " " + (-literals.get(j))
                        + " 0");
            }
        }
        return null;
    }

00140     public IConstr addAtLeast(IVecInt literals, int degree)
            throws ContradictionException {
        if (degree > 1) {
            throw new UnsupportedOperationException(
                    "Not a clausal problem! degree " + degree);
        }
        assert degree == 1;
        return addClause(literals);
    }

00150     public void setTimeout(int t) {
        // TODO Auto-generated method stub
    }

00154     public void setTimeoutMs(long t) {
        // TODO Auto-generated method stub
    }

00158     public int getTimeout() {
        // TODO Auto-generated method stub
        return 0;
    }

00163     public void reset() {
        fixedNbClauses = false;
        firstConstr  = true;

    }

00169     public void printStat(PrintStream out, String prefix) {
        // TODO Auto-generated method stub

    }

00174     public void printStat(PrintWriter out, String prefix) {
        // TODO Auto-generated method stub

    }

00179     public Map<String, Number> getStat() {
        // TODO Auto-generated method stub
        return null;
    }

00184     public String toString(String prefix) {
        return "Dimacs output solver";
    }

00188     public void clearLearntClauses() {
        // TODO Auto-generated method stub

    }

00193     public int[] model() {
        throw new UnsupportedOperationException();
    }

00197     public boolean model(int var) {
        throw new UnsupportedOperationException();
    }

00201     public boolean isSatisfiable() throws TimeoutException {
        throw new TimeoutException("There is no real solver behind!");
    }

00205     public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
        throw new TimeoutException("There is no real solver behind!");
    }

00209     public int[] findModel() throws TimeoutException {
        throw new UnsupportedOperationException();
    }

00213     public int[] findModel(IVecInt assumps) throws TimeoutException {
        throw new UnsupportedOperationException();
    }

00217     public int nConstraints() {
        return nbclauses;
    }

00221     public int nVars() {
       return nbvars;
    }

00225     public void expireTimeout() {
        // TODO Auto-generated method stub
        
    }

00230     public boolean isSatisfiable(IVecInt assumps, boolean global)
            throws TimeoutException {
        throw new TimeoutException("There is no real solver behind!");
    }

00235     public boolean isSatisfiable(boolean global) throws TimeoutException {
        throw new TimeoutException("There is no real solver behind!");
    }

00239     public void printInfos(PrintWriter out, String prefix) {
    }

00242     public void setTimeoutOnConflicts(int count) {        
    }

00245       public boolean isDBSimplificationAllowed() {
            return false;
      }

00249       public void setDBSimplificationAllowed(boolean status) {
      }

}

Generated by  Doxygen 1.6.0   Back to index