Efficient way for vertex cover variant

[UnlimitedCookies]

So I have been given an undirected graph G and a value t that specifies how many edges need to be covered at least by a set of vertices of which the total amount need to be minimized.
If I could simply use math like notation I would formulate the equation like this

1. Add a BoolVar for each vertex.
2. Add Constraint that the sum over all edges must be >= t, where for each edge min(u + v, 1) or u OR v is the summand.
3. Minimize the sum of all vertices that is deemed when implicitly casting them to int.

But I am afraid that both of these approaches are not suitable.
So my current solution is

1. Add a BoolVar for each vertex and each edge.
2. Add Constraint that the sum over all edges must be >= t.
3. Add Constraint that edge var implies that both vertices are true.
4. Minimize the sum of all vertices that is deemed when implicitly casting them to int.
   But I am afraid that both of these approaches don't work in linear programming.

Since this increases the amount of variables used, I wanted to ask whether there would be a cleaner/more efficient solution.

[lperron]

just try it.

[UnlimitedCookies]

just try it.

I mean my solution using more BoolVars is working.
My main question was whether I would be able to have a sum of BoolVars where two summands are limited to a maximum of 1.

[lperron]

I do not understand what you are asking for.

[lperron]

for each edge a <-> b, vertex_a and vertex_b are Boolean variables that are true when the corresponding vertex is selected.

   edge_a_b = model.new_bool_var('a-b')
   model.add_implication(edge_a_b, vertex_a)
   model.add_implication(edge_a_b, vertex_b)
   model.add_bool_and(edge_a_b).only_enforce_if(vertex_a, vertex_b)  # This one is optional

then the model:

  model.add(sum(edge_x_y) >= t)
  model.minimize(sum(vertex_x))

I guess this is what you have written. Even it if uses the CP-SAT API, it is clearly linear.

[UnlimitedCookies]

Right, thanks. I was asking whether a solution without the edge_a_b variables would be possible, but I suppose that wouldn't change the runtime that much, right?

And what I am also curious about: What difference does it make to have the biconditional instead of the simple subjunction/implication?