Merge pull request #5 from TiloW/lp-solver

Lp Solver

.travis.yml

@@ -2,7 +2,23 @@ language: java
 sudo: false
 
 jdk:
-- oraclejdk8
+  - oraclejdk7
+
+cache:
+  directories:
+    - ~/.bin
+    - ~/gradle/caches
+    - /tmp/scip
+
+env:
+  global:
+    - BIN_PATH=~/.bin
+
+before_install:
+- export PATH="$PATH:$BIN_PATH"
+
+install:
+  - if [ ! -f $BIN_PATH/scip ]; then ./script/scip-setup.sh; fi
 
 script:
   - gradle check

script/scip-setup.sh

@@ -0,0 +1,14 @@
+#!/bin/bash
+
+if [ -z "$BIN_PATH" ]; then
+	BIN_PATH=$HOME/bin
+fi
+
+FILENAME="scip-3.1.0.linux.x86_64.gnu.opt.spx"
+mkdir -p /tmp/scip
+wget -nc http://scip.zib.de/download/release/$FILENAME.zip -O /tmp/scip/scip.zip
+unzip /tmp/scip/scip.zip -d /tmp
+mv /tmp/$FILENAME $BIN_PATH/scip
+echo $BIN_PATH
+ls -l $BIN_PATH
+scip -c "quit"

src/main/java/proof/exception/LinearProgramException.java

@@ -0,0 +1,33 @@
+package proof.exception;
+
+import proof.solver.Solver;
+
+/**
+ * Thrown whenever a linear program could not be solved.
+ *
+ * @author Tilo Wiedera
+ */
+public class LinearProgramException extends InvalidProofException {
+  /**
+   * Creates a new linear program exception. Includes the provided error message.
+   *
+   * @param solver The executing solver
+   * @param filename The file containing the linear program
+   * @param errorMessage An optional error message, set to {@code null} to ignore
+   */
+  public LinearProgramException(Solver solver, String filename, String errorMessage) {
+    super(
+        solver.getClass().getSimpleName() + " error while solving " + filename + errorMessage == null ? ""
+            : ("\n" + errorMessage));
+  }
+
+  /**
+   * Creates a new linear program exception.
+   *
+   * @param solver The executing solver
+   * @param filename The file containing the linear program
+   */
+  public LinearProgramException(Solver solver, String filename) {
+    this(solver, filename, null);
+  }
+}

src/main/java/proof/exception/UnsupportedSolverException.java

@@ -0,0 +1,19 @@
+package proof.exception;
+
+/**
+ * Exception to be thrown when a linear program solver is requested that is not available on the
+ * command line.
+ *
+ * @author Tilo Wiedera
+ */
+public class UnsupportedSolverException extends RuntimeException {
+
+  /**
+   * Initializes a new unsupported solver exception.
+   *
+   * @param description The description should include the unsupported solvers.
+   */
+  public UnsupportedSolverException(String description) {
+    super(description);
+  }
+}

src/main/java/proof/solver/Cplex.java

@@ -0,0 +1,26 @@
+package proof.solver;
+
+import proof.exception.LinearProgramException;
+
+/**
+ * Wrapper class for calling the CPLEX optimization suite linear program solver.
+ *
+ * @author Tilo Wiedera
+ */
+class Cplex extends Solver {
+  @Override
+  protected String getCommand(String filename) {
+    return "clpex -c read " + filename + " optimize";
+  }
+
+  @Override
+  protected void handleLine(String line) throws LinearProgramException {
+    if (line.contains("Dual simplex - Optimal:")) {
+      setResult(parseDouble(line));
+    } else if (line.contains("No problem exists.")) {
+      setResult(0);
+    } else if (line.contains("Infeasible.")) {
+      returnInfeasiblity();
+    }
+  }
+}

src/main/java/proof/solver/Gurobi.java

@@ -0,0 +1,24 @@
+package proof.solver;
+
+import proof.exception.LinearProgramException;
+
+/**
+ * Wrapper class for performing calls to the Gurobi linear program solver.
+ *
+ * @author Tilo Wiedera
+ */
+class Gurobi extends Solver {
+  @Override
+  protected String getCommand(String filename) {
+    return "gurobi_cl " + filename;
+  }
+
+  @Override
+  protected void handleLine(String line) throws LinearProgramException {
+    if (line.contains("Infeasible model")) {
+      returnInfeasiblity();
+    } else if (line.contains("Optimal objective")) {
+      setResult(parseDouble(line));
+    }
+  }
+}

src/main/java/proof/solver/Scip.java

@@ -0,0 +1,35 @@
+package proof.solver;
+
+import proof.exception.LinearProgramException;
+
+
+/**
+ * Simple wrapper for executing the SCIP optimization suite linear program solver. This requires the
+ * scip command to be available on the console.
+ *
+ * @author Tilo Wiedera
+ */
+class Scip extends Solver {
+  private boolean isFeasible;
+
+  @Override
+  protected void prepareSolver() {
+    isFeasible = false;
+  }
+
+  @Override
+  protected String getCommand(String filename) {
+    return "scip -f " + filename;
+  }
+
+  @Override
+  protected void handleLine(String line) throws LinearProgramException {
+    if (line.contains("problem is solved [optimal solution found]")) {
+      isFeasible = true;
+    } else if (line.contains("problem is solved [infeasible]")) {
+      returnInfeasiblity();
+    } else if (isFeasible && line.contains("objective value:")) {
+      setResult(parseDouble(line));
+    }
+  }
+}

src/main/java/proof/solver/Solver.java

@@ -0,0 +1,159 @@
+package proof.solver;
+
+import java.io.BufferedReader;
+import java.io.File;
+import java.io.IOException;
+import java.io.InputStreamReader;
+import java.io.PrintWriter;
+import java.util.StringTokenizer;
+
+import proof.exception.LinearProgramException;
+import proof.exception.UnsupportedSolverException;
+
+/**
+ * Common interface for all linear program solvers.
+ *
+ * @author Tilo Wiedera
+ */
+public abstract class Solver {
+  private Double result;
+  private String filename;
+
+  public Solver() {
+    if (!isAvailable()) {
+      throw new UnsupportedSolverException(getClass().getName()
+          + " is not available. Calling this solver would fail: "
+          + getCommand("my-linear-program.lp"));
+    }
+  }
+
+  /**
+   * Solves the linear program contained in the given file. The file must contain a problem
+   * described in CPLEX lp format. Will return 0 if the given file is empty.
+   *
+   * @param filename The file containing the problem
+   * @return The optimal objective value
+   */
+  public double solve(String filename) throws LinearProgramException {
+    Process process = null;
+    result = null;
+    this.filename = filename;
+
+    prepareSolver();
+
+    try {
+      process = Runtime.getRuntime().exec(getCommand(filename));
+      BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream()));
+      BufferedReader errorReader =
+          new BufferedReader(new InputStreamReader(process.getErrorStream()));
+
+      for (String line = reader.readLine(); result == null && line != null; line =
+          reader.readLine()) {
+        if (errorReader.ready()) {
+          throw new LinearProgramException(this, filename, errorReader.readLine());
+        } else {
+          handleLine(line);
+        }
+      }
+    } catch (IOException e) {
+      Exception exception = new LinearProgramException(this, filename);
+      exception.initCause(e);
+    } finally {
+      if (process != null) {
+        process.destroy();
+      }
+    }
+
+    if (result == null) {
+      throw new LinearProgramException(this, filename, "output is missing some information.");
+    }
+
+    return result;
+  }
+
+  /**
+   * Sets the result of the current computation.
+   *
+   * @param value The optimal objective value
+   */
+  protected void setResult(double value) {
+    result = value;
+  }
+
+  /**
+   * Throws an exception to mark this linear program as infeasible.
+   *
+   * @throws LinearProgramException since the linear program is declared infeasible
+   */
+  protected void returnInfeasiblity() throws LinearProgramException {
+    throw new LinearProgramException(this, filename, "linear program is infeasible.");
+  }
+
+  /**
+   * Called just before parsing any lines from the solver output.
+   */
+  protected void prepareSolver() {}
+
+  /**
+   * Parses the last double value contained in the line.
+   *
+   * @param line The line containing the double, typically the optimal objective value.
+   * @return The parsed value
+   *
+   * @return true if this solver can be used
+   */
+  protected double parseDouble(String line) {
+    StringTokenizer st = new StringTokenizer(line);
+    String value = null;
+
+    while (st.hasMoreTokens()) {
+      value = st.nextToken();
+    }
+
+    return Double.parseDouble(value);
+  }
+
+  /**
+   * Returns the command used to execute this solver via command line.
+   *
+   * @param filename The file containing the linear program to be solved
+   * @return The string used to execute the solver
+   */
+  protected abstract String getCommand(String filename);
+
+  /**
+   * Called for each line in the solvers output. This method must be overridden to parse the actual
+   * results.
+   *
+   * @param line The currently investigated line from the solvers output
+   */
+  protected abstract void handleLine(String line) throws LinearProgramException;
+
+  /**
+   * Returns true if this solver is available on the command line.
+   *
+   * @return true if this solver can be used
+   */
+  private boolean isAvailable() {
+    Integer opt = null;
+
+    try {
+      File file = File.createTempFile("simple-linear-program", ".lp");
+      PrintWriter writer = new PrintWriter(file.getAbsoluteFile(), "UTF-8");
+
+      writer.println("Minimize");
+      writer.println("obj: x + y");
+      writer.println("Subject To");
+      writer.println("c1: x >= 2");
+      writer.println("c2: y >= 1");
+      writer.println("End");
+      writer.close();
+
+      opt = (int) solve(file.getAbsoluteFile().toString());
+    } catch (LinearProgramException | IOException e) {
+      // solver is not available
+    }
+
+    return opt != null && opt == 3;
+  }
+}