For this project, you are to augment your code from project 2 to solve the minimal Vertex Cover problem for the input graph. Your approach is based on a polynomial time reduction to CNF- SAT, and use of a SAT solver. The following are the steps you should take for this project.

SAT Solver

We will be using MiniSat SAT solver available at https://github.com/ agurfinkel/ *****（隐私）

MiniSat provides a CMake build system. You can compile it using the usual sequence:

cd PROJECT && mkdir build && cd build && cmake ../ && make

The build process creates an executable minisat and a library libminisat.a. You will need link against the library in your project.

Create a polynomial reduction of the decision version of VERTEX COVER to CNF-SAT. We have discussed the reduction in class. It is also available under the name a4 encoding.pdf on LEARN. You are allowed to use your own reduction provided it is sound and polynomial-time. Implement the reduction and use minisat as a library to solve the minimum VERTEX COVER problem for the graphs that are input to your program (as in project 2).

As soon as you get an input graph via the ’V’ and ’E’ specification you should compute a minimum-sized Vertex Cover, and immediately output it. The output should just be a sequence of vertices in increasing order separated by one space each. You can use qsort(3) or std::sort for sorting.

Assuming that your executable is called ece650-a4, the following is a sample run of your program:

$ ./ece650-a4 V 5

E {<0,4>,<4,1>,<0,3>,<3,4>,<3,2>,<1,3>} 3 4

The lines starting with V and E are the inputs to your program, and the last line is the output. Note that the minimum-sized vertex cover is not necessarily unique. You need to output just one of them.

Marking

We will try different graph inputs and check what vertex cover you output. We will only test your program with syntactically and semantically correct inputs.

0 Marking script for compile/make etc. fails: automatic 0

0 Your program runs, awaits input and does not crash on input: + 20

0 Passes Test Case 1: + 25

0 Passes Test Case 2: + 25

0 Passes Test Case 3: + 25

0 Programming style: + 5

CMake

As discussed below under “Submission Instructions”, you should use a CMakeLists.txt file to build your project. We will build your project using the following sequence:

cd PROJECT && mkdir build && cd build && cmake ../

where PROJECT is the top level directory of your submission. If your code is not compiled from scratch (i.e., from the C++ sources), you get an automatic 0.