| 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 |
|
package org.sat4j; |
| 26 |
|
|
| 27 |
|
import static java.lang.System.out; |
| 28 |
|
|
| 29 |
|
import org.apache.commons.cli.CommandLine; |
| 30 |
|
import org.apache.commons.cli.HelpFormatter; |
| 31 |
|
import org.apache.commons.cli.Options; |
| 32 |
|
import org.apache.commons.cli.ParseException; |
| 33 |
|
import org.apache.commons.cli.PosixParser; |
| 34 |
|
import org.sat4j.minisat.SolverFactory; |
| 35 |
|
import org.sat4j.opt.MaxSatDecorator; |
| 36 |
|
import org.sat4j.opt.MinCostDecorator; |
| 37 |
|
import org.sat4j.opt.MinOneDecorator; |
| 38 |
|
import org.sat4j.opt.WeightedMaxSatDecorator; |
| 39 |
|
import org.sat4j.reader.DimacsReader; |
| 40 |
|
import org.sat4j.reader.Reader; |
| 41 |
|
import org.sat4j.specs.ISolver; |
| 42 |
|
|
|
|
|
| 0% |
Uncovered Elements: 55 (55) |
Complexity: 8 |
Complexity Density: 0,37 |
|
| 43 |
|
public class GenericOptLauncher extends AbstractOptimizationLauncher { |
| 44 |
|
|
| 45 |
|
|
| 46 |
|
|
| 47 |
|
|
| 48 |
|
private static final long serialVersionUID = 1L; |
| 49 |
|
|
|
|
|
| 0% |
Uncovered Elements: 6 (6) |
Complexity: 1 |
Complexity Density: 0,17 |
|
| 50 |
0
|
@SuppressWarnings("nls")... |
| 51 |
|
private Options createCLIOptions() { |
| 52 |
0
|
Options options = new Options(); |
| 53 |
|
|
| 54 |
0
|
options.addOption("l", "library", true, |
| 55 |
|
"specifies the name of the library used (minisat by default)"); |
| 56 |
0
|
options.addOption("s", "solver", true, |
| 57 |
|
"specifies the name of the solver to use"); |
| 58 |
0
|
options.addOption("t", "timeout", true, |
| 59 |
|
"specifies the timeout (in seconds)"); |
| 60 |
0
|
options.addOption("k", "kind", true, |
| 61 |
|
"kind of problem: minone, maxsat, etc."); |
| 62 |
0
|
return options; |
| 63 |
|
} |
| 64 |
|
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
| 65 |
0
|
@Override... |
| 66 |
|
protected void usage() { |
| 67 |
0
|
out.println("java -jar sat4jopt instance-name"); |
| 68 |
|
} |
| 69 |
|
|
|
|
|
| 0% |
Uncovered Elements: 5 (5) |
Complexity: 2 |
Complexity Density: 0,67 |
|
| 70 |
0
|
@Override... |
| 71 |
|
protected Reader createReader(ISolver solver, String problemname) { |
| 72 |
0
|
if (problemname.endsWith(".wcnf")) { |
| 73 |
0
|
return new DimacsReader(solver, "wcnf"); |
| 74 |
|
} |
| 75 |
0
|
return new DimacsReader(solver); |
| 76 |
|
} |
| 77 |
|
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
| 78 |
0
|
@Override... |
| 79 |
|
protected String getInstanceName(String[] args) { |
| 80 |
0
|
return args[args.length - 1]; |
| 81 |
|
} |
| 82 |
|
|
|
|
|
| 0% |
Uncovered Elements: 34 (34) |
Complexity: 7 |
Complexity Density: 0,32 |
|
| 83 |
0
|
@Override... |
| 84 |
|
protected ISolver configureSolver(String[] args) { |
| 85 |
0
|
ISolver asolver = null; |
| 86 |
0
|
Options options = createCLIOptions(); |
| 87 |
0
|
if (args.length == 0) { |
| 88 |
0
|
HelpFormatter helpf = new HelpFormatter(); |
| 89 |
0
|
helpf.printHelp("java -jar sat4jopt.jar", options, true); |
| 90 |
|
} else { |
| 91 |
0
|
try { |
| 92 |
0
|
CommandLine cmd = new PosixParser().parse(options, args); |
| 93 |
|
|
| 94 |
0
|
String kind = cmd.getOptionValue("k"); |
| 95 |
0
|
if (kind == null) { |
| 96 |
0
|
kind = "maxsat"; |
| 97 |
|
} |
| 98 |
0
|
if ("minone".equalsIgnoreCase(kind)) { |
| 99 |
0
|
asolver = new MinOneDecorator(SolverFactory.newDefault()); |
| 100 |
0
|
} else if ("mincost".equalsIgnoreCase(kind)) { |
| 101 |
0
|
asolver = new MinCostDecorator(SolverFactory |
| 102 |
|
.newMiniOPBClauseCardConstrMax()); |
| 103 |
|
} else { |
| 104 |
0
|
assert "maxsat".equalsIgnoreCase(kind); |
| 105 |
0
|
int problemindex = args.length - 1; |
| 106 |
0
|
if (args[problemindex].endsWith(".wcnf")) { |
| 107 |
0
|
asolver = new WeightedMaxSatDecorator(SolverFactory |
| 108 |
|
.newMinimalOPBClauseCardConstrMaxSpecificOrder()); |
| 109 |
|
} else { |
| 110 |
0
|
asolver = new MaxSatDecorator(SolverFactory |
| 111 |
|
.newMiniMaxSAT()); |
| 112 |
|
} |
| 113 |
|
} |
| 114 |
0
|
log(asolver.toString(COMMENT_PREFIX)); |
| 115 |
|
} catch (ParseException e1) { |
| 116 |
0
|
HelpFormatter helpf = new HelpFormatter(); |
| 117 |
0
|
helpf.printHelp("java -jar sat4jopt.jar", options, true); |
| 118 |
|
} |
| 119 |
|
} |
| 120 |
0
|
return asolver; |
| 121 |
|
} |
| 122 |
|
|
|
|
|
| 0% |
Uncovered Elements: 2 (2) |
Complexity: 1 |
Complexity Density: 0,5 |
|
| 123 |
0
|
public static void main(String[] args) {... |
| 124 |
0
|
AbstractLauncher lanceur = new GenericOptLauncher(); |
| 125 |
0
|
lanceur.run(args); |
| 126 |
|
} |
| 127 |
|
} |