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.FileNotFoundException;
33 import java.io.IOException;
34
35 import org.sat4j.AbstractLauncher;
36 import org.sat4j.AbstractOptimizationLauncher;
37 import org.sat4j.core.ASolverFactory;
38 import org.sat4j.minisat.core.ICDCLLogger;
39 import org.sat4j.pb.reader.OPBReader2006;
40 import org.sat4j.reader.ParseFormatException;
41 import org.sat4j.reader.Reader;
42 import org.sat4j.specs.ContradictionException;
43 import org.sat4j.specs.IProblem;
44 import org.sat4j.specs.ISolver;
45 import org.sat4j.tools.ConflictDepthTracing;
46 import org.sat4j.tools.ConflictLevelTracing;
47 import org.sat4j.tools.DecisionTracing;
48 import org.sat4j.tools.FileBasedVisualizationTool;
49 import org.sat4j.tools.LearnedClausesSizeTracing;
50 import org.sat4j.tools.MultiTracing;
51
52
53
54
55
56
57
58 public class LanceurPseudo2005 extends AbstractOptimizationLauncher implements
59 ICDCLLogger {
60
61 ASolverFactory<IPBSolver> factory;
62
63 public LanceurPseudo2005() {
64 this(SolverFactory.instance());
65 }
66
67 LanceurPseudo2005(ASolverFactory<IPBSolver> factory) {
68 this.factory = factory;
69 }
70
71
72
73
74 private static final long serialVersionUID = 1L;
75
76
77
78
79
80
81
82
83 public static void main(final String[] args) {
84 final AbstractLauncher lanceur = new LanceurPseudo2005();
85 lanceur.run(args);
86 System.exit(lanceur.getExitCode().value());
87 }
88
89 protected ObjectiveFunction obfct;
90
91
92
93
94
95
96 @Override
97 protected Reader createReader(ISolver theSolver, String problemname) {
98 return new OPBReader2006((IPBSolver) theSolver);
99 }
100
101
102
103
104
105
106 @Override
107 protected ISolver configureSolver(String[] args) {
108 IPBSolver theSolver;
109 String solverName = args[0];
110 boolean trace = false;
111 if (solverName.startsWith("Trace")) {
112 trace = true;
113 solverName = solverName.substring("Trace".length());
114 }
115 boolean lower = false;
116 if (solverName.startsWith("Lower")) {
117 lower = true;
118 solverName = solverName.substring("Lower".length());
119 }
120 if (args.length > 1) {
121 theSolver = this.factory.createSolverByName(solverName);
122 } else {
123 theSolver = this.factory.defaultSolver();
124 }
125 if (lower) {
126 theSolver = new ConstraintRelaxingPseudoOptDecorator(theSolver);
127 } else {
128 theSolver = new PseudoOptDecorator(theSolver);
129 }
130 if (args.length == 3) {
131 theSolver.setTimeout(Integer.valueOf(args[1]));
132 }
133 if (trace) {
134 String fileName = args[args.length - 1];
135 theSolver.setSearchListener(new MultiTracing(
136 new ConflictLevelTracing(new FileBasedVisualizationTool(
137 fileName + "-conflict-level"),
138 new FileBasedVisualizationTool(fileName
139 + "-conflict-level-restart"),
140 new FileBasedVisualizationTool(fileName
141 + "-conflict-level-clean")),
142 new DecisionTracing(new FileBasedVisualizationTool(fileName
143 + "-decision-indexes-pos"),
144 new FileBasedVisualizationTool(fileName
145 + "-decision-indexes-neg"),
146 new FileBasedVisualizationTool(fileName
147 + "-decision-indexes-restart"),
148 new FileBasedVisualizationTool(fileName
149 + "-decision-indexes-clean")),
150 new LearnedClausesSizeTracing(
151 new FileBasedVisualizationTool(fileName
152 + "-learned-clauses-size"),
153 new FileBasedVisualizationTool(fileName
154 + "-learned-clauses-size-restart"),
155 new FileBasedVisualizationTool(fileName
156 + "-learned-clauses-size-clean")),
157 new ConflictDepthTracing(new FileBasedVisualizationTool(
158 fileName + "-conflict-depth"),
159 new FileBasedVisualizationTool(fileName
160 + "-conflict-depth-restart"),
161 new FileBasedVisualizationTool(fileName
162 + "-conflict-depth-clean"))));
163 }
164
165 this.out.println(theSolver.toString(COMMENT_PREFIX));
166 return theSolver;
167 }
168
169 @Override
170 public void usage() {
171 this.out.println("java -jar sat4j-pb.jar [solvername [timeout]] instancename.opb");
172 showAvailableSolvers(SolverFactory.instance());
173 }
174
175 @Override
176 protected String getInstanceName(String[] args) {
177 assert args.length == 1 || args.length == 2 || args.length == 3;
178 if (args.length == 0) {
179 return null;
180 }
181 return args[args.length - 1];
182 }
183
184 @Override
185 protected IProblem readProblem(String problemname)
186 throws FileNotFoundException, ParseFormatException, IOException,
187 ContradictionException {
188 IProblem problem = super.readProblem(problemname);
189 ObjectiveFunction obj = ((IPBSolver) problem).getObjectiveFunction();
190 if (obj != null) {
191 this.out.println(COMMENT_PREFIX + "objective function length is "
192 + obj.getVars().size() + " literals");
193 }
194 return problem;
195 }
196 }