Logo Search packages:      
Sourcecode: sat4j version File versions

SolverFactory.java

/*******************************************************************************
* SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le
*
* 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.
*******************************************************************************/
package org.sat4j.minisat;

import org.sat4j.core.ASolverFactory;
import org.sat4j.minisat.constraints.CardinalityDataStructure;
import org.sat4j.minisat.constraints.ClausalDataStructureCB;
import org.sat4j.minisat.constraints.ClausalDataStructureCBWL;
import org.sat4j.minisat.constraints.MixedDataStructureDaniel;
import org.sat4j.minisat.constraints.MixedDataStructureWithBinary;
import org.sat4j.minisat.constraints.MixedDataStructureWithBinaryAndTernary;
import org.sat4j.minisat.core.DataStructureFactory;
import org.sat4j.minisat.core.ILits;
import org.sat4j.minisat.core.ILits2;
import org.sat4j.minisat.core.ILits23;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.minisat.core.Solver;
import org.sat4j.minisat.learning.ActiveLearning;
import org.sat4j.minisat.learning.FixedLengthLearning;
import org.sat4j.minisat.learning.LimitedLearning;
import org.sat4j.minisat.learning.MiniSATLearning;
import org.sat4j.minisat.learning.NoLearningButHeuristics;
import org.sat4j.minisat.learning.PercentLengthLearning;
import org.sat4j.minisat.orders.JWOrder;
import org.sat4j.minisat.orders.MyOrder;
import org.sat4j.minisat.orders.PureOrder;
import org.sat4j.minisat.orders.RSATPhaseSelectionStrategy;
import org.sat4j.minisat.orders.VarOrder;
import org.sat4j.minisat.orders.VarOrderHeap;
import org.sat4j.minisat.restarts.ArminRestarts;
import org.sat4j.minisat.restarts.LubyRestarts;
import org.sat4j.minisat.restarts.MiniSATRestarts;
import org.sat4j.minisat.uip.DecisionUIP;
import org.sat4j.minisat.uip.FirstUIP;
import org.sat4j.opt.MinOneDecorator;
import org.sat4j.specs.ISolver;
import org.sat4j.tools.DimacsOutputSolver;
import org.sat4j.tools.OptToSatAdapter;

/**
 * User friendly access to pre-constructed solvers.
 * 
 * @author leberre
 */
00062 public class SolverFactory extends ASolverFactory<ISolver> {

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

    // thread safe implementation of the singleton design pattern
    private static SolverFactory instance;

    /**
     * Private constructor. Use singleton method instance() instead.
     * 
     * @see #instance()
     */
00077     private SolverFactory() {
        super();
    }

    private static synchronized void createInstance() {
        if (instance == null) {
            instance = new SolverFactory();
        }
    }

    /**
     * Access to the single instance of the factory.
     * 
     * @return the singleton of that class.
     */
00092     public static SolverFactory instance() {
        if (instance == null) {
            createInstance();
        }
        return instance;
    }

    /**
     * @return a "default" "minilearning" solver learning clauses of size
     *         smaller than 10 % of the total number of variables
     */
00103     public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearning() {
        return newMiniLearning(10);
    }

    /**
     * @return a "default" "minilearning" solver learning clauses of size
     *         smaller than 10 % of the total number of variables with a heap
     *         based var order.
     */
00112     public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeap() {
        return newMiniLearningHeap(new MixedDataStructureDaniel());
    }

    public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeapEZSimp() {
        Solver<ILits,DataStructureFactory<ILits>> solver = newMiniLearningHeap();
        solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
        return solver;
    }

    public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeapExpSimp() {
        Solver<ILits,DataStructureFactory<ILits>> solver = newMiniLearningHeap();
        solver.setSimplifier(solver.EXPENSIVE_SIMPLIFICATION);
        return solver;
    }

    public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeapRsatExpSimp() {
        Solver<ILits,DataStructureFactory<ILits>> solver = newMiniLearningHeapExpSimp();
        solver.setOrder(new VarOrderHeap<ILits>(new RSATPhaseSelectionStrategy()));
        return solver;
    }

    public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeapRsatExpSimpBiere() {
        Solver<ILits,DataStructureFactory<ILits>> solver = newMiniLearningHeapRsatExpSimp();
        solver.setRestartStrategy(new ArminRestarts());
        solver.setSearchParams(new SearchParams(1.1, 100));
        return solver;
    }

    public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeapRsatExpSimpLuby() {
        Solver<ILits,DataStructureFactory<ILits>> solver = newMiniLearningHeapRsatExpSimp();
        solver.setRestartStrategy(new LubyRestarts());
        return solver;
    }

    /**
     * @param n
     *                the maximal size of the clauses to learn as a percentage
     *                of the initial number of variables
     * @return a "minilearning" solver learning clauses of size smaller than n
     *         of the total number of variables
     */
00154     public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearning(int n) {
        return newMiniLearning(new MixedDataStructureDaniel(), n);
    }

    /**
     * @param dsf
     *                a specific data structure factory
     * @return a default "minilearning" solver using a specific data structure
     *         factory, learning clauses of length smaller or equals to 10 % of
     *         the number of variables.
     */
00165     public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniLearning(
            DataStructureFactory<L> dsf) {
        return newMiniLearning(dsf, 10);
    }

    /**
     * @param dsf
     *                a specific data structure factory
     * @return a default "minilearning" solver using a specific data structure
     *         factory, learning clauses of length smaller or equals to 10 % of
     *         the number of variables and a heap based VSIDS heuristics
     */
00177     public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniLearningHeap(
            DataStructureFactory<L> dsf) {
        return newMiniLearning(dsf, new VarOrderHeap<L>());
    }

    /**
     * @return a default minilearning solver using a specific data structure
     *         described in Lawrence Ryan thesis to handle binary clauses.
     * @see #newMiniLearning
     */
00187     public static Solver<ILits2,DataStructureFactory<ILits2>> newMiniLearning2() {
        return newMiniLearning(new MixedDataStructureWithBinary());
    }

    public static Solver<ILits2,DataStructureFactory<ILits2>> newMiniLearning2Heap() {
        return newMiniLearningHeap(new MixedDataStructureWithBinary());
    }

    /**
     * @return a default minilearning solver using a specific data structures
     *         described in Lawrence Ryan thesis to handle binary and ternary
     *         clauses.
     * @see #newMiniLearning
     */
00201     public static Solver<ILits23,DataStructureFactory<ILits23>> newMiniLearning23() {
        return newMiniLearning(new MixedDataStructureWithBinaryAndTernary());
    }

    /**
     * @return a default minilearning SAT solver using counter-based clause
     *         representation (i.e. all the literals of a clause are watched)
     */
00209     public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningCB() {
        return newMiniLearning(new ClausalDataStructureCB());
    }

    /**
     * @return a default minilearning SAT solver using counter-based clause
     *         representation (i.e. all the literals of a clause are watched)
     *         for the ORIGINAL clauses and watched-literals clause
     *         representation for learnt clauses.
     */
00219     public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningCBWL() {
        return newMiniLearning(new ClausalDataStructureCBWL());
    }

    public static Solver<ILits2,DataStructureFactory<ILits2>> newMiniLearning2NewOrder() {
        return newMiniLearning(new MixedDataStructureWithBinary(),
                new MyOrder());
    }

    /**
     * @return a default minilearning SAT solver choosing periodically to branch
     *         on "pure watched" literals if any. (a pure watched literal l is a
     *         literal that is watched on at least one clause such that its
     *         negation is not watched at all. It is not necessarily a watched
     *         literal.)
     */
00235     public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningPure() {
        return newMiniLearning(new MixedDataStructureDaniel(), new PureOrder());
    }

    /**
     * @return a default minilearning SAT solver choosing periodically to branch
     *         on literal "pure in the original set of clauses" if any.
     */
00243     public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningCBWLPure() {
        return newMiniLearning(new ClausalDataStructureCBWL(), new PureOrder());
    }

    /**
     * @param dsf
     *                the data structure factory used to represent literals and
     *                clauses
     * @param n
     *                the maximum size of learnt clauses as percentage of the
     *                original number of variables.
     * @return a SAT solver with learning limited to clauses of length smaller
     *         or equal to n, the dsf data structure, the FirstUIP clause
     *         generator and a sort of VSIDS heuristics.
     */
00258     public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniLearning(
            DataStructureFactory<L> dsf, int n) {
        LimitedLearning<L,DataStructureFactory<L>> learning = new PercentLengthLearning<L,DataStructureFactory<L>>(n);
        Solver<L,DataStructureFactory<L>> solver = new Solver<L,DataStructureFactory<L>>(new FirstUIP(), learning, dsf,
                new VarOrder<L>(), new MiniSATRestarts());
        learning.setSolver(solver);
        return solver;
    }

    /**
     * @param dsf
     *                the data structure factory used to represent literals and
     *                clauses
     * @param order
     *                the heuristics
     * @return a SAT solver with learning limited to clauses of length smaller
     *         or equal to 10 percent of the total number of variables, the dsf
     *         data structure, the FirstUIP clause generator and order as
     *         heuristics.
     */
00278     public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniLearning(
            DataStructureFactory<L> dsf, IOrder<L> order) {
        LimitedLearning<L,DataStructureFactory<L>> learning = new PercentLengthLearning<L,DataStructureFactory<L>>(10);
        Solver<L,DataStructureFactory<L>> solver = new Solver<L,DataStructureFactory<L>>(new FirstUIP(), learning, dsf, order,
                new MiniSATRestarts());
        learning.setSolver(solver);
        return solver;
    }

    public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningEZSimp() {
        return newMiniLearningEZSimp(new MixedDataStructureDaniel());
    }

    // public static ISolver newMiniLearning2EZSimp() {
    // return newMiniLearningEZSimp(new MixedDataStructureWithBinary());
    // }

    public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniLearningEZSimp(
            DataStructureFactory<L> dsf) {
        LimitedLearning<L,DataStructureFactory<L>> learning = new PercentLengthLearning<L,DataStructureFactory<L>>(10);
        Solver<L,DataStructureFactory<L>> solver = new Solver<L,DataStructureFactory<L>>(new FirstUIP(), learning, dsf,
                new VarOrder<L>(), new MiniSATRestarts());
        learning.setSolver(solver);
        solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
        return solver;
    }

    /**
     * @return a default MiniLearning without restarts.
     */
00308     public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeapEZSimpNoRestarts() {
        LimitedLearning<ILits,DataStructureFactory<ILits>> learning = new PercentLengthLearning<ILits,DataStructureFactory<ILits>>(10);
        Solver<ILits,DataStructureFactory<ILits>> solver = new Solver<ILits,DataStructureFactory<ILits>>(new FirstUIP(), learning,
                new MixedDataStructureDaniel(), new SearchParams(
                        Integer.MAX_VALUE), new VarOrderHeap<ILits>(),
                new MiniSATRestarts());
        learning.setSolver(solver);
        solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
        return solver;
    }

    /**
     * @return a default MiniLearning with restarts beginning at 1000 conflicts.
     */
00322     public static Solver<ILits,DataStructureFactory<ILits>> newMiniLearningHeapEZSimpLongRestarts() {
        LimitedLearning<ILits,DataStructureFactory<ILits>> learning = new PercentLengthLearning<ILits,DataStructureFactory<ILits>>(10);
        Solver<ILits,DataStructureFactory<ILits>> solver = new Solver<ILits,DataStructureFactory<ILits>>(new FirstUIP(), learning,
                new MixedDataStructureDaniel(), new SearchParams(1000),
                new VarOrderHeap<ILits>(), new MiniSATRestarts());
        learning.setSolver(solver);
        solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
        return solver;
    }

    /**
     * @return a SAT solver using First UIP clause generator, watched literals,
     *         VSIDS like heuristics learning only clauses having a great number
     *         of active variables, i.e. variables with an activity strictly
     *         greater than one.
     */
00338     public static Solver<ILits,DataStructureFactory<ILits>> newActiveLearning() {
        ActiveLearning<ILits,DataStructureFactory<ILits>> learning = new ActiveLearning<ILits,DataStructureFactory<ILits>>();
        Solver<ILits,DataStructureFactory<ILits>> s = new Solver<ILits,DataStructureFactory<ILits>>(new FirstUIP(), learning,
                new MixedDataStructureDaniel(), new VarOrder<ILits>(),
                new MiniSATRestarts());
        learning.setOrder(s.getOrder());
        learning.setSolver(s);
        return s;
    }

    /**
     * @return a SAT solver very close to the original MiniSAT sat solver.
     */
00351     public static Solver<ILits,DataStructureFactory<ILits>> newMiniSAT() {
        return newMiniSAT(new MixedDataStructureDaniel());
    }

    /**
     * @return MiniSAT without restarts.
     */
00358     public static Solver<ILits,DataStructureFactory<ILits>> newMiniSATNoRestarts() {
        MiniSATLearning<ILits,DataStructureFactory<ILits>> learning = new MiniSATLearning<ILits,DataStructureFactory<ILits>>();
        Solver<ILits,DataStructureFactory<ILits>> solver = new Solver<ILits,DataStructureFactory<ILits>>(new FirstUIP(), learning,
                new MixedDataStructureDaniel(), new SearchParams(
                        Integer.MAX_VALUE), new VarOrder<ILits>(),
                new MiniSATRestarts());
        learning.setDataStructureFactory(solver.getDSFactory());
        learning.setVarActivityListener(solver);
        return solver;

    }

    /**
     * @return MiniSAT with a special data structure from Lawrence Ryan thesis
     *         for managing binary clauses.
     */
00374     public static Solver<ILits2,DataStructureFactory<ILits2>> newMiniSAT2() {
        return newMiniSAT(new MixedDataStructureWithBinary());
    }

    /**
     * @return MiniSAT with a special data structure from Lawrence Ryan thesis
     *         for managing binary and ternary clauses.
     */
00382     public static Solver<ILits23,DataStructureFactory<ILits23>> newMiniSAT23() {
        return newMiniSAT(new MixedDataStructureWithBinaryAndTernary());
    }

    /**
     * @param dsf
     *                the data structure used for representing clauses and lits
     * @return MiniSAT the data structure dsf.
     */
00391     public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniSAT(
            DataStructureFactory<L> dsf) {
        MiniSATLearning<L,DataStructureFactory<L>> learning = new MiniSATLearning<L,DataStructureFactory<L>>();
        Solver<L,DataStructureFactory<L>> solver = new Solver<L,DataStructureFactory<L>>(new FirstUIP(), learning, dsf,
                new VarOrder<L>(), new MiniSATRestarts());
        learning.setDataStructureFactory(solver.getDSFactory());
        learning.setVarActivityListener(solver);
        return solver;
    }

    /**
     * @return a SAT solver very close to the original MiniSAT sat solver.
     */
00404     public static Solver<ILits,DataStructureFactory<ILits>> newMiniSATHeap() {
        return newMiniSATHeap(new MixedDataStructureDaniel());
    }

    /**
     * @return a SAT solver very close to the original MiniSAT sat solver
     *         including easy reason simplification.
     */
00412     public static Solver<ILits,DataStructureFactory<ILits>> newMiniSATHeapEZSimp() {
        Solver<ILits,DataStructureFactory<ILits>> solver = newMiniSATHeap();
        solver.setSimplifier(solver.SIMPLE_SIMPLIFICATION);
        return solver;
    }

    public static Solver<ILits,DataStructureFactory<ILits>> newMiniSATHeapExpSimp() {
        Solver<ILits,DataStructureFactory<ILits>> solver = newMiniSATHeap();
        solver.setSimplifier(solver.EXPENSIVE_SIMPLIFICATION);
        return solver;
    }

    /**
     * @return MiniSAT with a special data structure from Lawrence Ryan thesis
     *         for managing binary clauses.
     */
00428     public static Solver<ILits2,DataStructureFactory<ILits2>> newMiniSAT2Heap() {
        return newMiniSATHeap(new MixedDataStructureWithBinary());
    }

    /**
     * @return MiniSAT with a special data structure from Lawrence Ryan thesis
     *         for managing binary and ternary clauses.
     */
00436     public static Solver<ILits23,DataStructureFactory<ILits23>> newMiniSAT23Heap() {
        return newMiniSATHeap(new MixedDataStructureWithBinaryAndTernary());
    }

    public static <L extends ILits> Solver<L,DataStructureFactory<L>> newMiniSATHeap(
            DataStructureFactory<L> dsf) {
        MiniSATLearning<L,DataStructureFactory<L>> learning = new MiniSATLearning<L,DataStructureFactory<L>>();
        Solver<L,DataStructureFactory<L>> solver = new Solver<L,DataStructureFactory<L>>(new FirstUIP(), learning, dsf,
                new VarOrderHeap<L>(), new MiniSATRestarts());
        learning.setDataStructureFactory(solver.getDSFactory());
        learning.setVarActivityListener(solver);
        return solver;
    }

    /**
     * @return MiniSAT with data structures to handle cardinality constraints.
     */
00453     public static Solver<ILits,DataStructureFactory<ILits>> newMiniCard() {
        return newMiniSAT(new CardinalityDataStructure());
    }


    /**
     * @return MiniSAT with decision UIP clause generator.
     */
00461     public static Solver<ILits,DataStructureFactory<ILits>> newRelsat() {
        MiniSATLearning<ILits,DataStructureFactory<ILits>> learning = new MiniSATLearning<ILits,DataStructureFactory<ILits>>();
        Solver<ILits,DataStructureFactory<ILits>> solver = new Solver<ILits,DataStructureFactory<ILits>>(new DecisionUIP(), learning,
                new MixedDataStructureDaniel(), new VarOrderHeap<ILits>(),
                new MiniSATRestarts());
        learning.setDataStructureFactory(solver.getDSFactory());
        learning.setVarActivityListener(solver);
        return solver;
    }

    /**
     * @return MiniSAT with VSIDS heuristics, FirstUIP clause generator for
     *         backjumping but no learning.
     */
00475     public static Solver<ILits,DataStructureFactory<ILits>> newBackjumping() {
        NoLearningButHeuristics<ILits,DataStructureFactory<ILits>> learning = new NoLearningButHeuristics<ILits,DataStructureFactory<ILits>>();
        Solver<ILits,DataStructureFactory<ILits>> solver = new Solver<ILits,DataStructureFactory<ILits>>(new FirstUIP(), learning,
                new MixedDataStructureDaniel(), new VarOrderHeap<ILits>(),
                new MiniSATRestarts());
        learning.setVarActivityListener(solver);
        return solver;
    }

    /**
     * @return a SAT solver with learning limited to clauses of length smaller
     *         or equals to 3, with a specific data structure for binary and
     *         ternary clauses as found in Lawrence Ryan thesis, without
     *         restarts, with a Jeroslow/Wang kind of heuristics.
     */
00490     public static Solver<ILits23,DataStructureFactory<ILits23>> newMini3SAT() {
        LimitedLearning<ILits23,DataStructureFactory<ILits23>> learning = new FixedLengthLearning<ILits23,DataStructureFactory<ILits23>>(3);
        Solver<ILits23,DataStructureFactory<ILits23>> solver = new Solver<ILits23,DataStructureFactory<ILits23>>(new FirstUIP(), learning,
                new MixedDataStructureWithBinaryAndTernary(), new SearchParams(
                        Integer.MAX_VALUE), new JWOrder(),
                new MiniSATRestarts());
        learning.setSolver(solver);
        return solver;
    }

    /**
     * @return a Mini3SAT with full learning.
     * @see #newMini3SAT()
     */
00504     public static Solver<ILits23,DataStructureFactory<ILits23>> newMini3SATb() {
        MiniSATLearning<ILits23,DataStructureFactory<ILits23>> learning = new MiniSATLearning<ILits23,DataStructureFactory<ILits23>>();
        Solver<ILits23,DataStructureFactory<ILits23>> solver = new Solver<ILits23,DataStructureFactory<ILits23>>(new FirstUIP(), learning,
                new MixedDataStructureWithBinaryAndTernary(), new SearchParams(
                        Integer.MAX_VALUE), new JWOrder(),
                new MiniSATRestarts());
        learning.setDataStructureFactory(solver.getDSFactory());
        learning.setVarActivityListener(solver);
        return solver;
    }

    /**
     * @return a solver computing models with a minimum number of satisfied literals.
     */
00518     public static ISolver newMinOneSolver() {
        return new OptToSatAdapter(new MinOneDecorator(newDefault()));
    }
    
    /**
     * Default solver of the SolverFactory. This solver is meant to be used on
     * challenging SAT benchmarks.
     * 
     * @return the best "general purpose" SAT solver available in the factory.
     * @see #defaultSolver() the same method, polymorphic, to be called from an
     *      instance of ASolverFactory.
     */
00530     public static ISolver newDefault() {
        return newMiniLearningHeapRsatExpSimpBiere();
    }

    @Override
    public ISolver defaultSolver() {
        return newDefault();
    }

    /**
     * Small footprint SAT solver.
     * 
     * @return a SAT solver suitable for solving small/easy SAT benchmarks.
     * @see #lightSolver() the same method, polymorphic, to be called from an
     *      instance of ASolverFactory.
     */
00546     public static ISolver newLight() {
        return newMini3SAT();
    }

    @Override
    public ISolver lightSolver() {
        return newLight();
    }

    public static ISolver newDimacsOutput() {
        return new DimacsOutputSolver();
    }

}

Generated by  Doxygen 1.6.0   Back to index