General InstructionsFile formatsInput graphs use an extended DIMACS-format that is described here. You can use the supplied Graph classes for reading the graph-format. Javadoc documentation of the classes is here. Linear programs generated by your program should follow the format described here. Satisfiability problems generated by your program should use the format for constrained boolean circuits described here Needed filesA jar-file containing graph and conversion classes: hoa.jar A Linux x86 binary for the lp_solve solver lp_solve A Linux x86 binary for the constrained boolean circuits solver bczchaff An example linear programming encoding for the INDEPENDENT SET problem: IndependentSetLP.java An example SAT encoding for the INDEPENDENT SET problem: IndependentSetSAT.java A testgraph: testgraph.g An Example: The INDEPENDENT SET problemIn the files IndependentSetLP.java IndependentSetSAT.java are linear program encoder for maximization version and satisfiability encoder for decision version of the INDEPENDENT SET problem, respectively. The linear program encoder creates a boolean variable for each node in the graph. The variable decides whether the node belongs to the independent set. For each edge ek(ni,nj) the encoder creates a constraint ni + nj <= 1. The objective function to maximize is the sum of all node variables ni. The satisfiability encoder creates the same variables as the linear program encoder. It then creates two formulas. The first sets the amount of true node variables to the goal K. The second is a conjunction of expressions for each edge stating that endpoints cannot both be true Compiling and running the exampleDownload the files to a single directory Set the executable flags for the binaries and set java classpath environment variable (with tcsh): chmod u+x bczchaff lp_solve setenv CLASSPATH hoa.jar:. Compile the encodings: javac IndependentSetLP.java IndependentSetSAT.java Test LP and SAT encodings with the testgraph java IndependentSetLP testgraph.g | java lp.ToLPSolve | ./lp_solve | java lp.FromLPSolve java IndependentSetSAT 6 testgraph.g | ./bczchaff | java sat.FromBC [TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links] Latest update: 30 August 2005. |