I am currently trying to solve the Minimum Vertex Cover problem via a Weighted MAX SAT solver, but I am stuck with the model. The transformation to a simple SAT is straightforward since every node can be a variable and every edge a clause with a disjunction between start and end node, but I have a problem introducing the minimum boundary. I thought of adding clauses with each just containing a negated variable in order to inhibit that simply all variables are set to true. But this does not work in all instances. Could you hint me on how I could construct that?