1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30 package org.sat4j.pb;
31
32 import java.io.IOException;
33
34 import org.sat4j.AbstractLauncher;
35 import org.sat4j.ILauncherMode;
36 import org.sat4j.core.ASolverFactory;
37 import org.sat4j.pb.core.ObjectiveReducerPBSolverDecorator;
38 import org.sat4j.pb.reader.OPBReader2006;
39 import org.sat4j.pb.tools.SearchOptimizerListener;
40 import org.sat4j.reader.ParseFormatException;
41 import org.sat4j.reader.Reader;
42 import org.sat4j.specs.ContradictionException;
43 import org.sat4j.specs.ILogAble;
44 import org.sat4j.specs.IProblem;
45 import org.sat4j.specs.ISolver;
46
47
48
49
50
51
52
53 public class LanceurPseudo2005 extends AbstractLauncher implements ILogAble {
54
55 ASolverFactory<IPBSolver> factory;
56
57 public LanceurPseudo2005() {
58 this(SolverFactory.instance());
59 }
60
61 LanceurPseudo2005(ASolverFactory<IPBSolver> factory) {
62 this.factory = factory;
63 setLauncherMode(ILauncherMode.OPTIMIZATION);
64 }
65
66
67
68
69 private static final long serialVersionUID = 1L;
70
71
72
73
74
75
76
77
78 public static void main(final String[] args) {
79 final AbstractLauncher lanceur = new LanceurPseudo2005();
80 lanceur.run(args);
81 System.exit(lanceur.getExitCode().value());
82 }
83
84 protected ObjectiveFunction obfct;
85
86
87
88
89
90
91 @Override
92 protected Reader createReader(ISolver theSolver, String problemname) {
93 return new OPBReader2006((IPBSolver) theSolver);
94 }
95
96
97
98
99
100
101 @Override
102 protected ISolver configureSolver(String[] args) {
103 IPBSolver theSolver;
104 String solverName = args[0];
105 boolean lower = false;
106 if (solverName.startsWith("Lower")) {
107 lower = true;
108 solverName = solverName.substring("Lower".length());
109 }
110 if (args.length > 1) {
111 theSolver = this.factory.createSolverByName(solverName);
112 } else {
113 theSolver = this.factory.defaultSolver();
114 }
115 if (System.getProperty("OBJREDUCER") != null) {
116 if (lower) {
117 theSolver = new ConstraintRelaxingPseudoOptDecorator(
118 new ObjectiveReducerPBSolverDecorator(theSolver));
119 } else {
120 theSolver = new PseudoOptDecorator(
121 new ObjectiveReducerPBSolverDecorator(theSolver));
122 }
123 } else if (System.getProperty("INTERNAL") != null) {
124 theSolver.setSearchListener(new SearchOptimizerListener(
125 ILauncherMode.DECISION));
126 setLauncherMode(ILauncherMode.DECISION);
127 } else {
128 if (lower) {
129 theSolver = new ConstraintRelaxingPseudoOptDecorator(theSolver);
130 } else {
131 theSolver = new PseudoOptDecorator(theSolver);
132 }
133 }
134 if (args.length == 3) {
135 theSolver.setTimeout(Integer.valueOf(args[1]));
136 }
137 this.out.println(theSolver.toString(COMMENT_PREFIX));
138 return theSolver;
139 }
140
141 @Override
142 public void usage() {
143 this.out.println("java -jar sat4j-pb.jar [solvername [timeout]] instancename.opb");
144 showAvailableSolvers(SolverFactory.instance());
145 }
146
147 @Override
148 protected String getInstanceName(String[] args) {
149 assert args.length == 1 || args.length == 2 || args.length == 3;
150 if (args.length == 0) {
151 return null;
152 }
153 return args[args.length - 1];
154 }
155
156 @Override
157 protected IProblem readProblem(String problemname)
158 throws ParseFormatException, IOException, ContradictionException {
159 IProblem problem = super.readProblem(problemname);
160 ObjectiveFunction obj = ((IPBSolver) problem).getObjectiveFunction();
161 if (obj != null) {
162 this.out.println(COMMENT_PREFIX + "objective function length is "
163 + obj.getVars().size() + " literals");
164 }
165 return problem;
166 }
167 }