View Javadoc

1   /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    * 
4    * Based on the original minisat specification from:
5    * 
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    * 
10   * This library is free software; you can redistribute it and/or modify it under
11   * the terms of the GNU Lesser General Public License as published by the Free
12   * Software Foundation; either version 2.1 of the License, or (at your option)
13   * any later version.
14   * 
15   * This library is distributed in the hope that it will be useful, but WITHOUT
16   * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17   * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18   * details.
19   * 
20   * You should have received a copy of the GNU Lesser General Public License
21   * along with this library; if not, write to the Free Software Foundation, Inc.,
22   * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23   * 
24   */
25  package org.sat4j;
26  
27  import static java.lang.System.out;
28  
29  import org.sat4j.minisat.SolverFactory;
30  import org.sat4j.minisat.core.IOrder;
31  import org.sat4j.minisat.core.Solver;
32  import org.sat4j.minisat.orders.VarOrderHeapObjective;
33  import org.sat4j.opt.ObjectiveFunction;
34  import org.sat4j.opt.PseudoOptDecorator;
35  import org.sat4j.reader.OPBReader2005;
36  import org.sat4j.reader.OPBReader2006;
37  import org.sat4j.reader.Reader;
38  import org.sat4j.specs.IProblem;
39  import org.sat4j.specs.ISolver;
40  import org.sat4j.specs.TimeoutException;
41  
42  /**
43   * Launcher especially dedicated to the pseudo boolean 05 evaluation (@link
44   * http://www.cril.univ-artois.fr/PB05/).
45   * 
46   * @author mederic
47   */
48  public class LanceurPseudo2005 extends AbstractOptimizationLauncher {
49  
50      /**
51       * 
52       */
53      private static final long serialVersionUID = 1L;
54  
55      /**
56       * Lance le prouveur sur un fichier Dimacs
57       * 
58       * @param args
59       *            doit contenir le nom d'un fichier Dimacs, eventuellement
60       *            compress?.
61       */
62      public static void main(final String[] args) {
63          final AbstractLauncher lanceur = new LanceurPseudo2005();
64          lanceur.run(args);
65          System.exit(lanceur.getExitCode().value());
66      }
67  
68      protected ObjectiveFunction obfct;
69  
70      /*
71       * (non-Javadoc)
72       * 
73       * @see org.sat4j.Lanceur#createReader(org.sat4j.specs.ISolver)
74       */
75      @Override
76      protected Reader createReader(ISolver solver, String problemname) {
77          return new OPBReader2006(solver);
78      }
79  
80      @Override
81      protected void solve(IProblem problem) throws TimeoutException {
82          ObjectiveFunction obj = ((OPBReader2005) getReader())
83                  .getObjectiveFunction();
84          ((PseudoOptDecorator) problem).setObjectTiveFunction(obj);
85          IOrder<?> order = ((Solver<?>) ((PseudoOptDecorator) problem).decorated())
86                  .getOrder();
87          if (order instanceof VarOrderHeapObjective) {
88              ((VarOrderHeapObjective) order).setObjectiveFunction(obj);
89          }
90          super.solve(problem);
91      }
92  
93      /*
94       * (non-Javadoc)
95       * 
96       * @see org.sat4j.Lanceur#configureSolver(java.lang.String[])
97       */
98      @Override
99      protected ISolver configureSolver(String[] args) {
100         ISolver solver;
101         if (args.length > 1) {
102             solver = SolverFactory.instance().createSolverByName(args[0]);
103         } else {
104             solver = SolverFactory
105                     .newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncrementalLearnJustClauses();
106 //            solver = SolverFactory
107 //            .newMinimalOPBClauseCardConstrMaxSpecificOrder();
108         }
109         solver = new PseudoOptDecorator(solver);
110         solver.setTimeout(Integer.MAX_VALUE);
111         out.println(solver.toString(COMMENT_PREFIX)); //$NON-NLS-1$
112         return solver;
113     }
114 
115     @Override
116     protected void usage() {
117         out.println("java -jar sat4jPseudo instancename.opb"); //$NON-NLS-1$
118     }
119 
120     @Override
121     protected String getInstanceName(String[] args) {
122         assert args.length == 1 || args.length == 2;
123         return args[args.length - 1];
124     }
125 }