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