Commit d2471f03 authored by Mahesh Tripunitara's avatar Mahesh Tripunitara
Browse files

Improved sat solver output processing. Tried to add waitFor() to process...

Improved sat solver output processing. Tried to add waitFor() to process runtime, but that makes things that ran fairly fast seem to run much slower.
parent 5987c204
......@@ -17,5 +17,5 @@ public interface RunSolver {
*/
public boolean checkIfSolverIsReachable();
public EpochHistory run();
public EpochHistory run() throws Exception;
}
......@@ -3,6 +3,7 @@ package vagabond.reduction.cnfsat;
import java.io.*;
import java.util.LinkedList;
import java.util.List;
import java.util.concurrent.TimeUnit;
import vagabond.circuit.*;
import vagabond.pieces.EpochHistory;
......@@ -17,6 +18,7 @@ public class RunSolverCNFSAT implements RunSolver {
String solverloc = new String("/home/tripunit/Desktop/lingeling");
String cnfloc = new String("/home/tripunit/Desktop/instance.cnf");
ReduceToCNFSAT _r = null;
int EACH_DECISION_INSTANCE_TIMEOUT = -1; // Seconds. -1 means infinity
/**
* A circuit that multiplies two non-negative integers. The first encoded in n bits, and the second in m bits.
......@@ -240,7 +242,7 @@ public class RunSolverCNFSAT implements RunSolver {
}
@Override
public EpochHistory run() {
public EpochHistory run() throws Exception {
// Confirm that the timing manager is setup
if (timing == null) {
timing = VagabondSettings.getInstance().timing;
......@@ -255,6 +257,8 @@ public class RunSolverCNFSAT implements RunSolver {
// Constraint Line (1) -- optimization objective
// Setup for binary search
FileWriter fw = new FileWriter("/home/tripunit/Desktop/timing.out");
Circuit c = _r._circ;
// for each pair of clients a sum circuit
int nclientpairs = ((_r.nc - 1) * (_r.nc)) / 2;
......@@ -265,6 +269,7 @@ public class RunSolverCNFSAT implements RunSolver {
} catch (Exception e) {
e.printStackTrace();
/*TIMING*/ timing.cancelTimer("RunSolverCNFSAT::run");
fw.close();
return null;
}
......@@ -288,35 +293,65 @@ public class RunSolverCNFSAT implements RunSolver {
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch");
for (int mid = hi; hi >= lo; mid = (hi + lo) / 2) {
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::loopVal=" + mid);
// System.out.println("mid = "+mid); System.out.flush();
// System.out.println("mid = "+mid); System.out.flush();
try {
constraintInfoLeakUb(c, le, s, nclientpairs, mid);
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::cnfSatToFile");
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::cnfSatToFile " + mid);
// Now convert to cnf, invoke solver and adjust mid as needed.
CircuitUtils.cnfSatToFile(c, cnfloc);
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::cnfSatToFile");
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::cnfSatToFile " + mid);
/*TIMING*/ timing.writeOutSingle(fw, "RunSolverCNFSAT::run::binarySearch::cnfSatToFile " + mid);
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::exec");
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::exec " + mid);
Process p = Runtime.getRuntime().exec(solverloc + " " + cnfloc);
// Activate the following 'if,' if we want to put in a time-limit for every decision instance.
if(mid < hi && EACH_DECISION_INSTANCE_TIMEOUT > 0 && !p.waitFor(EACH_DECISION_INSTANCE_TIMEOUT, TimeUnit.SECONDS)) {
// Treat this as unsat
lo = mid+1;
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::exec " + mid);
/*TIMING*/ timing.writeOutSingle(fw,"RunSolverCNFSAT::run::binarySearch::exec " + mid);
continue;
}
// TODO: Jon -- timing issues with I/O after solver-run.
BufferedReader solveroutput = new BufferedReader(new InputStreamReader(p.getInputStream()));
// save the certificate
List<String> lines = new LinkedList<String>();
boolean recordlines = false;
for (String str = null; (str = solveroutput.readLine()) != null;) {
lines.add(str);
}
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::exec");
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::searchSatisfiable");
if (lines.contains("s SATISFIABLE")) {
cnfcert = lines;
hi = mid - 1;
} else {
lo = mid + 1;
if(recordlines) {
lines.add(str);
if(str.contains(Integer.toString(c.getInputs().size()))) {
// System.out.println("Breaking at: "+str+", #inputs = "+c.getInputs().size());
break;
}
// else
continue;
}
// else
if(str.contains("s SATISFIABLE")) {
// Start to record sufficient # of variables
recordlines = true;
}
}
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::searchSatisfiable");
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::exec " + mid);
/*TIMING*/ timing.writeOutSingle(fw,"RunSolverCNFSAT::run::binarySearch::exec " + mid);
if(!recordlines) lo = mid + 1; // unsat
else { cnfcert = lines; hi = mid - 1; }
// /*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::searchSatisfiable" + mid);
// if (lines.contains("s SATISFIABLE")) {
// cnfcert = lines;
// hi = mid - 1;
// } else {
// lo = mid + 1;
// }
// /*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::searchSatisfiable" + mid);
// /*TIMING*/ timing.writeOutSingle(fw,"RunSolverCNFSAT::run::binarySearch::searchSatisfiable" + mid);
} catch (Exception e) {
e.printStackTrace();
/*TIMING*/ timing.cancelTimer("RunSolverCNFSAT::run");
......@@ -335,6 +370,7 @@ public class RunSolverCNFSAT implements RunSolver {
ret.add(PlacementMapFromCNFSATSolver.getPlacementMap(_r, cnfcert));
/*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run");
/*TIMING*/ timing.writeOutSingle(fw,"RunSolverCNFSAT::run");
return ret;
}
......
......@@ -22,7 +22,7 @@ public class CNFEverythingTests {
@Test
public void equalSpreadTest() throws Exception {
VagabondSettings vs = VagabondSettings.getInstance();
vs.migrationBudget = new Integer(4);
vs.migrationBudget = new Integer(-1);
vs.numberOfClients = new Integer(3);
vs.numberOfMachineSlots = new Integer(3);
vs.numberOfEpochs = new Integer(5);
......@@ -56,8 +56,8 @@ public class CNFEverythingTests {
@Test
public void equalSpreadBiggerTest() throws Exception {
int testparam = 15;
int migbudget = -1;
int testparam = 10;
int migbudget = 3;
VagabondSettings vs = VagabondSettings.getInstance();
vs.migrationBudget = new Integer(migbudget);
vs.numberOfClients = new Integer(testparam);
......
......@@ -90,7 +90,7 @@ public class TimingManager {
if (t == null) {
startTimer(key);
} else {
startTimer(key);
stopTimer(key);
}
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment