Commit 2ed4678c authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files

CNF Solver works on Windows; Fixed the timing kery names; going to more after...

CNF Solver works on Windows; Fixed the timing kery names; going to more after I merge in Mahesh's HOTFIX for a "lethal bug"
parent 09bb9854
package vagabond.reduction.cnfsat;
import java.io.*;
import java.util.ArrayList;
import java.util.LinkedList;
import java.util.List;
import java.util.*;
import java.util.concurrent.TimeUnit;
import org.apache.commons.lang3.StringUtils;
import vagabond.circuit.*;
import vagabond.pieces.EpochHistory;
import vagabond.reduction.ReduceTo;
......@@ -14,13 +14,27 @@ import vagabond.singleton.VagabondSettings;
import vagabond.timing.TimingManager;
public class RunSolverCNFSAT implements RunSolver {
public static VagabondSettings settings;
public TimingManager timing = null;
public String tp = "Epoch_Unknown";
String solverloc = new String("/home/tripunit/Desktop/lingeling");
String cnfloc = new String("/home/tripunit/Desktop/instance.cnf");
String solverloc;
String cnfloc;// OLD VALUE = new String("/home/tripunit/Desktop/instance.cnf");
ReduceToCNFSAT _r = null;
int EACH_DECISION_INSTANCE_TIMEOUT = -1; // Seconds. -1 means infinity
public RunSolverCNFSAT() throws IOException {
settings = VagabondSettings.getInstance();
timing = settings.timing;
solverloc = settings.getCNFSolverExceutable().getAbsolutePath();
cnfloc = settings.getCNFInstanceFile().getAbsolutePath();
}
@Override
public void setTimerKeyPrefix(String keyPrefix) {
tp = keyPrefix;
}
/**
* A circuit that multiplies two non-negative integers. The first encoded in n bits, and the second in m bits.
*
......@@ -73,7 +87,7 @@ public class RunSolverCNFSAT implements RunSolver {
return c;
}
List<Circuit.Wire> getInWires(Circuit r, int k, int c,
public List<Circuit.Wire> getInWires(Circuit r, int k, int c,
int nc, int ns, List<Integer> nv) throws Exception {
List<Circuit.Wire> ret = new LinkedList<Circuit.Wire>();
......@@ -148,7 +162,7 @@ public class RunSolverCNFSAT implements RunSolver {
}
int zc0c1 = _r._eh._sumOfInformationLeakage.get(c0, c1);
//System.out.println("z["+c0+","+c1+"]: "+zc0c1);
// System.out.println("z["+c0+","+c1+"]: "+zc0c1);
IntegerAsCircuit circ_zc0c1 = new IntegerAsCircuit(zc0c1);
c.union(circ_zc0c1);
for (int l = 0; l < circ_zc0c1.getOutputs().size(); l++) {
......@@ -178,42 +192,43 @@ public class RunSolverCNFSAT implements RunSolver {
}
}
}
// If we're doing total info. leak, we should add all of values in s[] up, and return a single
// sum circuit
if(!VagabondSettings.getInstance().minimizeMaxClientToClientInfoLeak) {
List<Integer> li = new ArrayList<Integer>();
for(int i = 0; i < s.length; i++) {
li.add(new Integer(s[i].getOutputs().size()));
}
Sum tot = new Sum(li);
c.union(tot);
int totinidx = 0;
for(int i = 0; i < s.length; i++) {
for(int j = 0; j < s[i].getOutputs().size(); j++) {
c.fuse(s[i].getOutputs().get(j), tot.getInputs().get(totinidx++));
}
}
for(int i = 0; i < tot.getOutputs().size(); i++) {
c.removeAsOutput(tot.getOutputs().get(i));
}
s = new Sum[1];
s[0] = tot;
if (!VagabondSettings.getInstance().minimizeMaxClientToClientInfoLeak) {
List<Integer> li = new ArrayList<Integer>();
for (int i = 0; i < s.length; i++) {
li.add(new Integer(s[i].getOutputs().size()));
}
Sum tot = new Sum(li);
c.union(tot);
int totinidx = 0;
for (int i = 0; i < s.length; i++) {
for (int j = 0; j < s[i].getOutputs().size(); j++) {
c.fuse(s[i].getOutputs().get(j), tot.getInputs().get(totinidx++));
}
}
for (int i = 0; i < tot.getOutputs().size(); i++) {
c.removeAsOutput(tot.getOutputs().get(i));
}
s = new Sum[1];
s[0] = tot;
}
return s;
}
public void constraintInfoLeakUb(Circuit c, LessEquals le[], BigAndOr band, Sum s[], int nclientpairs, int ub) throws Exception {
public void constraintInfoLeakUb(Circuit c, LessEquals le[], BigAndOr band, Sum s[], int nclientpairs, int ub)
throws Exception {
IntegerAsCircuit midc = new IntegerAsCircuit(ub);
c.union(midc);
for (int j = 0; j < midc.getOutputs().size(); j++) {
c.removeAsOutput(midc.getOutputs().get(j));
}
for (int i = 0; i < le.length; i++) {
if (le[i] != null) {
c.gates.removeAll(le[i].gates);
......@@ -232,11 +247,11 @@ public class RunSolverCNFSAT implements RunSolver {
}
}
if(band != null) {
c.gates.removeAll(band.gates);
c.wires.removeAll(band.wires);
c.inputs.removeAll(band.wires);
c.outputs.removeAll(band.wires);
if (band != null) {
c.gates.removeAll(band.gates);
c.wires.removeAll(band.wires);
c.inputs.removeAll(band.wires);
c.outputs.removeAll(band.wires);
}
band = addBigAnd(c);
......@@ -265,13 +280,6 @@ public class RunSolverCNFSAT implements RunSolver {
return band;
}
public String tp = "Epoch_Unknown";
@Override
public void setTimerKeyPrefix(String keyPrefix) {
tp = keyPrefix;
}
@Override
public boolean load(ReduceTo r) {
// Confirm that the timing manager is setup
......@@ -291,12 +299,7 @@ public class RunSolverCNFSAT implements RunSolver {
@Override
public EpochHistory run() throws Exception {
// Confirm that the timing manager is setup
if (timing == null) {
timing = VagabondSettings.getInstance().timing;
}
/*TIMING*/ timing.toggleTimer("RunSolverCNFSAT::run");
/*TIMING*/ timing.toggleTimer(tp + "RunSolverCNFSAT::run");
// Get CNF-SAT instance from ReduceTo argument to load().
// Run the solver. Get raw string result. Then invoke
......@@ -305,8 +308,7 @@ 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;
......@@ -316,16 +318,15 @@ public class RunSolverCNFSAT implements RunSolver {
s = constraintSumInfoLeak(c, _r, nclientpairs);
} catch (Exception e) {
e.printStackTrace();
/*TIMING*/ timing.cancelTimer("RunSolverCNFSAT::run");
fw.close();
/*TIMING*/ timing.cancelTimer(tp + "RunSolverCNFSAT::run");
return null;
}
// All the sum circuits whose outputs we want to compare against are now in s[]
int hi;
if(VagabondSettings.getInstance().minimizeMaxClientToClientInfoLeak) {
if (VagabondSettings.getInstance().minimizeMaxClientToClientInfoLeak) {
int maxclientnv = -1;
for (int i = 0; i < _r.nv.size(); i++) {
if (_r.nv.get(i) > maxclientnv) {
......@@ -333,54 +334,55 @@ public class RunSolverCNFSAT implements RunSolver {
}
}
hi = _r._eh._sumOfInformationLeakage.getMaxInformationLeak() + maxclientnv * maxclientnv;
}
else {
hi = _r._eh._sumOfInformationLeakage.getSumInformationLeak() + _r._eh.get(0).getSumInformationLeak();
hi = _r._eh._sumOfInformationLeakage.getMaxInformationLeak() + maxclientnv * maxclientnv;
} else {
hi = _r._eh._sumOfInformationLeakage.getSumInformationLeak() + _r._eh.get(0).getSumInformationLeak();
}
int lo = 0;
LessEquals le[];
if(VagabondSettings.getInstance().minimizeMaxClientToClientInfoLeak) {
le = new LessEquals[nclientpairs];
if (VagabondSettings.getInstance().minimizeMaxClientToClientInfoLeak) {
le = new LessEquals[nclientpairs];
for (int i = 0; i < nclientpairs; i++) {
le[i] = null;
}
} else {
le = new LessEquals[1];
le[0] = null;
}
else {
le = new LessEquals[1];
le[0] = null;
}
BigAndOr band = null;
List<String> cnfcert = null;
// certificate from cnf-sat
// Binary search
/*TIMING*/ timing.toggleTimer("RunSolverCNFSAT::run::binarySearch");
/*TIMING*/ timing.toggleTimer(tp + "RunSolverCNFSAT::run::binarySearch::totalTime");
String searchVal;
int loopCount = 0;
for (int mid = hi; hi >= lo; mid = (hi + lo) / 2) {
/*TIMING*/ timing.toggleTimer("RunSolverCNFSAT::run::binarySearch::loopVal=" + mid);
// System.out.println("mid = "+mid); System.out.flush();
searchVal = StringUtils.leftPad(loopCount + "", (int) Math.floor(Math.log10(hi)) + 1, "0") + "::mid::"
+ StringUtils.leftPad(mid + "", (int) Math.floor(Math.log10(hi)) + 1, "0");
/*TIMING*/ timing.toggleTimer(tp + "RunSolverCNFSAT::run::binarySearch::loopVal::" + searchVal);
// System.out.println("mid = "+mid); System.out.flush();
try {
constraintInfoLeakUb(c, le, band, s, nclientpairs, mid);
/*TIMING*/ timing.toggleTimer("RunSolverCNFSAT::run::binarySearch::cnfSatToFile " + mid);
/*TIMING*/ timing.toggleTimer(tp + "RunSolverCNFSAT::run::binarySearch::cnfSatToFile::" + searchVal);
// Now convert to cnf, invoke solver and adjust mid as needed.
CircuitUtils.cnfSatToFile(c, cnfloc);
/*TIMING*/ timing.toggleTimer("RunSolverCNFSAT::run::binarySearch::cnfSatToFile " + mid);
/*TIMING*/ timing.writeOutSingle(fw, "RunSolverCNFSAT::run::binarySearch::cnfSatToFile " + mid);
/*TIMING*/ timing.toggleTimer(tp + "RunSolverCNFSAT::run::binarySearch::cnfSatToFile::" + searchVal);
/*TIMING*/ timing.toggleTimer("RunSolverCNFSAT::run::binarySearch::exec " + mid);
/*TIMING*/ timing.toggleTimer(tp + "RunSolverCNFSAT::run::binarySearch::exec::" + searchVal);
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.toggleTimer("RunSolverCNFSAT::run::binarySearch::exec " + mid);
/*TIMING*/ timing.writeOutSingle(fw,"RunSolverCNFSAT::run::binarySearch::exec " + mid);
continue;
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.toggleTimer(tp + "RunSolverCNFSAT::run::binarySearch::exec::" + searchVal);
continue;
}
BufferedReader solveroutput = new BufferedReader(new InputStreamReader(p.getInputStream()));
......@@ -388,58 +390,61 @@ public class RunSolverCNFSAT implements RunSolver {
List<String> lines = new LinkedList<String>();
boolean recordlines = false;
for (String str = null; (str = solveroutput.readLine()) != null;) {
if(recordlines) {
if (recordlines) {
lines.add(str);
if(str.contains(Integer.toString(c.getInputs().size()))) {
// System.out.println("Breaking at: "+str+", #inputs = "+c.getInputs().size());
break;
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;
}
// else
if (str.contains("s SATISFIABLE")) {
// Start to record sufficient # of variables
recordlines = true;
}
}
/*TIMING*/ timing.toggleTimer(tp + "RunSolverCNFSAT::run::binarySearch::exec::" + searchVal);
if (!recordlines)
lo = mid + 1; // unsat
else {
cnfcert = lines;
hi = mid - 1;
}
/*TIMING*/ timing.toggleTimer("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);
// /*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::searchSatisfiable"+searchVal);
// if (lines.contains("s SATISFIABLE")) {
// cnfcert = lines;
// hi = mid - 1;
// } else {
// lo = mid + 1;
// }
// /*TIMING*/ timing.toggleTime("RunSolverCNFSAT::run::binarySearch::searchSatisfiable"+searchVal);
// /*TIMING*/
// timing.writeOutSingle(fw,"RunSolverCNFSAT::run::binarySearch::searchSatisfiable"+searchVal);
} catch (Exception e) {
e.printStackTrace();
/*TIMING*/ timing.cancelTimer("RunSolverCNFSAT::run");
/*TIMING*/ timing.cancelTimer(tp + "RunSolverCNFSAT::run");
return null;
}
/*TIMING*/ timing.toggleTimer("RunSolverCNFSAT::run::binarySearch::loopVal=" + mid);
/*TIMING*/ timing.toggleTimer(tp + "RunSolverCNFSAT::run::binarySearch::loopVal::" + searchVal);
}
/*TIMING*/ timing.toggleTimer("RunSolverCNFSAT::run::binarySearch");
/*TIMING*/ timing.toggleTimer(tp + "RunSolverCNFSAT::run::binarySearch::totalTime");
// Build an epochhistory data structure as required by this function's signature
if (cnfcert == null) {
/*TIMING*/ timing.cancelTimer("RunSolverCNFSAT::run");
/*TIMING*/ timing.cancelTimer(tp + "RunSolverCNFSAT::run");
return null;
}
EpochHistory ret = new EpochHistory(1);
ret.add(PlacementMapFromCNFSATSolver.getPlacementMap(_r, cnfcert));
/*TIMING*/ timing.toggleTimer("RunSolverCNFSAT::run");
/*TIMING*/ timing.writeOutSingle(fw,"RunSolverCNFSAT::run");
/*TIMING*/ timing.toggleTimer(tp + "RunSolverCNFSAT::run");
return ret;
}
}
......@@ -5,6 +5,8 @@ import java.text.DateFormat;
import java.text.SimpleDateFormat;
import java.util.logging.*;
import org.apache.commons.lang3.SystemUtils;
import vagabond.VagabondInstance;
import vagabond.VagabondOptionString;
import vagabond.enums.InformationLeakageType;
......@@ -88,30 +90,43 @@ public class VagabondSettings {
public String resultsFile = "vagabond.results.txt";
/**
* The IBM OPL file for the minimize the <b>MAX</b> Client to Client Information Leakage
* @see #getIlpOplFile()
*/
public String ilpOplFile = "ilp.mod";
/**
* The IBM OPL file for the minimize the <b>MAX</b> Client to Client Information Leakage
* with <b>no Migration Budget</b>.
* @see #getIlpOplNoMigrationFile()
*/
public String ilpOplNoMigrationFile = "ilpNoMigration.mod";
/**
* The IBM OPL file for the minimize the <b>SUM</b> Client to Client Information Leakage
* @see #getIlpOplFile()
*/
public String ilpOplFileSumInfoLeak = "ilp_sum.mod";
/**
* The IBM OPL file for the minimize the <b>SUM</b> Client to Client Information Leakage
* with <b>no Migration Budget</b>.
* @see #getIlpOplNoMigrationFile()
*/
public String ilpOplNoMigrationFileSumInfoLeak = "ilpNoMigration_sum.mod";
/**
* File to write out the CNF SAT reduction to then pass to the CNF SAT Solver
* @see #getCNFInstanceFile()
*/
public String cnfInstanceFile = "instance.cnf";
// ################################################################
// PROGRAMS
/**
* Filename of the CNF Solver executable;
* can change this if you are on Linux/Mac to the binary compiled for that system.
* Filename of the CNF Solver executable for Windows;
* Automatically changes this if you are on Linux/Mac to the binary compiled for that system.
*/
public String cnfSolverProgram = "lingeling.exe";
public String cnfSolverProgram_Win = "lingeling.exe";
/**
* Filename of the CNF Solver executable for Linux;
* Automatically changes this if you are on Linux/Mac to the binary compiled for that system.
*/
public String cnfSolverProgram_Linux = "/home/tripunit/Desktop/lingeling";
/**
* Filename of the Nomad executable;
* can change this if you are on Linux/Mac to the binary compiled for that system.
......@@ -456,21 +471,15 @@ public class VagabondSettings {
/**
* Function to return the file path of the CNF Solver executable; by default it is Lingeling.
* @return File object to the CNF Solver executable
*/
public File getCNFSolverExceutable() {
return new File(programFolder + File.separator + cnfSolverFolder + File.separator + cnfSolverProgram);
}
/**
* Closes all of the open handles and removes all the locks from log files.
* If System.exit() needs to be called or the program exits normally,
* then this function should be called before hand.
*/
public void shutdown() {
if (logger != null) {
for (Handler h : logger.getHandlers()) {
h.close();// must call h.close or a .LCK file will remain.
}
* @throws IOException Is thrown if you are on an operating system that doesn't have a binary for the CNF solver
*/
public File getCNFSolverExceutable() throws IOException {
if (SystemUtils.IS_OS_WINDOWS) {
return new File(programFolder + File.separator + cnfSolverFolder + File.separator + cnfSolverProgram_Win);
} else if (SystemUtils.IS_OS_LINUX) {
return new File(cnfSolverProgram_Linux);
} else {
throw new IOException("There is no CNF Solver binary for your OS: " + SystemUtils.OS_NAME);
}
}
......@@ -498,4 +507,21 @@ public class VagabondSettings {
return new File(dataFolder + File.separator + ilpOplNoMigrationFileSumInfoLeak);
}
/**
* Closes all of the open handles and removes all the locks from log files.
* If System.exit() needs to be called or the program exits normally,
* then this function should be called before hand.
*/
public void shutdown() {
if (logger != null) {
for (Handler h : logger.getHandlers()) {
h.close();// must call h.close or a .LCK file will remain.
}
}
}
public File getCNFInstanceFile() {
return new File(dataFolder + File.separator + cnfInstanceFile);
}
}
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