Logo Search packages:      
Sourcecode: sat4j version File versions

DimacsStringSolver.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.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 write down a CNF into a String.
 * 
 * It is especially useful compared to the DimacsOutputSolver 
 * because the number of clauses does not need to be known in 
 * advance.
 *  
 * @author leberre
 * 
 */
00052 public class DimacsStringSolver implements ISolver {

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

    private StringBuffer out;

    private int nbvars;

    private int nbclauses;

    private boolean fixedNbClauses = false;

    private boolean firstConstr = true;

    private int firstCharPos;
    
    private final int initBuilderSize;
    
    public DimacsStringSolver() {
        this(16);
    }

    public DimacsStringSolver(int initSize) {
        out = new StringBuffer(initSize);
        initBuilderSize = initSize;
    }

    public StringBuffer getOut(){
      return out;
    }

00086     public int newVar() {
        return 0;
    }

00090     public int newVar(int howmany) {
        out.append("p cnf " + howmany);
        setNbVars(howmany);
        return howmany;
    }
    
    protected void setNbVars(int howmany){
      nbvars = howmany;
    }

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

00106     public IConstr addClause(IVecInt literals) throws ContradictionException {
        if (firstConstr) {
            if (!fixedNbClauses) {
                firstCharPos = 7 + Integer.toString(nbvars).length();
                out.append("                    ");
                out.append("\n");
                nbclauses=0;
            }
            firstConstr = false;
        }
        if (!fixedNbClauses) nbclauses++;
        
        for (IteratorInt iterator = literals.iterator();iterator.hasNext();)
            out.append(iterator.next()).append(" ");
        out.append("0\n");
        return null;        
    }

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

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

00133     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) {
                firstCharPos = 7 + Integer.toString(nbvars).length();
                out.append("                    ");
                out.append("\n");
                nbclauses=0;
            }
            firstConstr = false;
        }
        
        for (int i = 0; i <= literals.size(); i++) {
            for (int j = i + 1; j < literals.size(); j++) {
                if (!fixedNbClauses) nbclauses++;
                out.append("" + (-literals.get(i)) + " " + (-literals.get(j))
                        + " 0\n");
            }
        }
        return null;
    }

00160     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);
    }

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

    }

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

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

00184     public void reset() {
        fixedNbClauses = false;
        firstConstr  = true;
        out = new StringBuffer(initBuilderSize);
    }

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

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

    }

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

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

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

    }

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

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

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

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

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

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

00237     public int nConstraints() {
        return nbclauses;
    }

00241     public int nVars() {
        return nbvars;
    }
    
    @Override
    public String toString() {
//        String numClauses = Integer.toString(nbclauses);
//        int numClausesLength = numClauses.length();
//        for (int i = 0; i < numClausesLength; ++i) {
//            out.setCharAt(firstCharPos + i, numClauses.charAt(i));
//        }
      out.insert(firstCharPos, nbclauses);
        return out.toString();
    }

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

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

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

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

00273     public void setTimeoutOnConflicts(int count) {
        
    }

00277       public boolean isDBSimplificationAllowed() {
            return false;
      }

00281       public void setDBSimplificationAllowed(boolean status) {
            
      }

}

Generated by  Doxygen 1.6.0   Back to index