TCS / Studies / T-79.4201 / Home Assignments / Thispage
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science

General Instructions

File formats

Input 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 files

A 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 problem

In 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 example

Download 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.