View Javadoc

1   /*******************************************************************************
2   * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le
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  package org.sat4j.csp;
20  
21  import org.sat4j.core.ASolverFactory;
22  import org.sat4j.minisat.constraints.MixedDataStructureDanielWL;
23  import org.sat4j.minisat.core.DataStructureFactory;
24  import org.sat4j.minisat.core.ILits;
25  import org.sat4j.minisat.core.Solver;
26  import org.sat4j.minisat.learning.MiniSATLearning;
27  import org.sat4j.minisat.orders.VarOrderHeap;
28  import org.sat4j.minisat.restarts.MiniSATRestarts;
29  import org.sat4j.specs.ISolver;
30  import org.sat4j.tools.DimacsOutputSolver;
31  
32  /**
33   * User friendly access to pre-constructed solvers.
34   * 
35   * @author leberre
36   */
37  public class SolverFactory extends ASolverFactory<ISolver> {
38  
39      /**
40       * 
41       */
42      private static final long serialVersionUID = 1L;
43  
44      // thread safe implementation of the singleton design pattern
45      private static SolverFactory instance;
46  
47      /**
48       * Private constructor. Use singleton method instance() instead.
49       * 
50       * @see #instance()
51       */
52      private SolverFactory() {
53          super();
54      }
55  
56      private static synchronized void createInstance() {
57          if (instance == null) {
58              instance = new SolverFactory();
59          }
60      }
61  
62      /**
63       * Access to the single instance of the factory.
64       * 
65       * @return the singleton of that class.
66       */
67      public static SolverFactory instance() {
68          if (instance == null) {
69              createInstance();
70          }
71          return instance;
72      }
73  
74      /**
75       * @param dsf
76       *                the data structure used for representing clauses and lits
77       * @return MiniSAT the data structure dsf.
78       */
79      public static <L extends ILits> Solver<DataStructureFactory> newMiniSAT(
80              DataStructureFactory dsf) {
81          MiniSATLearning<DataStructureFactory> learning = new MiniSATLearning<DataStructureFactory>();
82          Solver<DataStructureFactory> solver = new Solver<DataStructureFactory>(learning, dsf,
83                  new VarOrderHeap(), new MiniSATRestarts());
84          learning.setDataStructureFactory(solver.getDSFactory());
85          learning.setVarActivityListener(solver);
86          return solver;
87      }
88  
89  
90      
91      /**
92       * Default solver of the SolverFactory. This solver is meant to be used on
93       * challenging SAT benchmarks.
94       * 
95       * @return the best "general purpose" SAT solver available in the factory.
96       * @see #defaultSolver() the same method, polymorphic, to be called from an
97       *      instance of ASolverFactory.
98       */
99      public static ISolver newDefault() {
100         Solver<DataStructureFactory> solver = newMiniSAT(new MixedDataStructureDanielWL());
101         solver.setSimplifier(solver.EXPENSIVE_SIMPLIFICATION);
102         return solver;
103     }
104 
105     @Override
106     public ISolver defaultSolver() {
107         return newDefault();
108     }
109 
110     /**
111      * Small footprint SAT solver.
112      * 
113      * @return a SAT solver suitable for solving small/easy SAT benchmarks.
114      * @see #lightSolver() the same method, polymorphic, to be called from an
115      *      instance of ASolverFactory.
116      */
117     public static ISolver newLight() {
118     	return newMiniSAT(new MixedDataStructureDanielWL());
119     }
120 
121     @Override
122     public ISolver lightSolver() {
123         return newLight();
124     }
125 
126     public static ISolver newDimacsOutput() {
127         return new DimacsOutputSolver();
128     }
129 
130 }