How to Solve Vertex Cover Problem by SAT and Optimization?

Question

So right now I am working on using SAT to resolve the minimum vertex cover problem, and here is my encoding for the graph G = {V,E} has k vertex cover, and here are the clauses:

Let n = sizeof(V);

Firstly, at lease one vertex is in the vertex cover:

For i in {1..k}
    Add clause (x<1,i> ∨ x<2,i> ∨ ··· ∨ x<n,i>);

Then, no one vertex can appear twice in vertex cover:

For j in {1..n}
    For l and m in {1..k} with l < m
        Add clause (¬x<j,l> ∨ ¬x<j,m>) 

After that, only one vertex can appear at a specific position in vertex cover:

For j in {1..k}
    For l and m in {1..n} with l < m
        Add clause (¬x<l,j> ∨ ¬x<m,j>) 

Finally, at least one vertex in vertex cover should come from edges:

For i and j in each edge e from E
    Add clause (x<i,1> ∨ x<i,2> ∨ ... ∨ x<i,k> ∨ x<j,1> ∨ ... ∨ x<j,k>)

Now I am able to get the minimum vertex cover by using this encoding but the efficiency is pretty bad. I can only get a result for any graph with < 20 vertices, otherwise it will just take minutes and hours for getting me a result. I am now thinking to reduce it from SAT further more, maybe to 3SAT. But looks like that I cannot simply change all clause from nCNF to 3CNF for getting the same result. Could anyone please help me to figure out what should I do next? Do I need a brand new encoding?

Thank you so much.

BTW, I am using MiniSAT for the solver.

Answer 1

First, let me premise that I have some trouble understanding your encoding, so i'll start from scratch. This is how I would approach the problem.

Note: my example is based on the SMT-LIB syntax and can be solved with a MaxSMT solver like, e.g., z3 and optimathsat. However, since it does not use any SMT feature, you can actually write the same thing with the standard WCNF format used at MaxSAT competitions. This would give you more choice when picking a solver to handle the problem. I may be wrong, but I speculate that MaxSAT solvers may outperform MaxSMT ones on this particular problem.

---

Let G = {V, E} be a graph.

First, declare a Boolean variable for each vertex in the graph:

(declare-fun vertex_1 () Bool)
...
(declare-fun vertex_K () Bool)

(Any vertex without edges should be omitted because it would just waste time.)

Second, declare a Boolean variable for each edge in the graph connecting a vertex i with a vertex j (assume undirected)

(declare-fun edge_i_j () Bool)
...

Third, assert that every edge edge_i_j must be covered:

(assert edge_i_j)
...

Fourth, if an edge edge_i_j is covered, then either vertex i or vertex j must be true:

(assert (=> edge_i_j (or vertex_i vertex_j)))
...

Fifth, for each vertex_i assert with a soft clause that vertex_i should be false. If that isn't the case, get a penalty of value 1 on the value of cover:

(assert-soft (not vertex_i) :weight 1 :id cover)

At last, solve the problem:

(set-option :config opt.maxsmt_engine=maxres) ; only for optimathsat
(minimize cover)                              ; only for optimathsat
(check-sat)
(get-objectives)
(get-model)

At this point, one can use any efficient MaxSAT/MaxSMT engine (e.g. MaxRes) to get a model that covers all of the edges while using the least number of vertices (if any).