
Title:
1033 Number Of Vertices For Variables

Description:

We started with an input to SAT,

and that is going to be a lean formula with n variables

and these are going to be as always x₁, x₂ and so on until you reach xn.

And we are also going to specify the number of clauses

and I'm just going to use the letter m here

so we're going to say we have m clauses

and I'm also going to give them names

so I'm going to call them C₁, C₂ and so on until you reach Cm.

We're now going to construct a graph that represents or encodes this Boolean Formula here

and we are going to do this just as we have done before.

So, this part here is going to represent X₁.

This part over here is going to represent X₂ and so on and this one here Xn.

Now, the question of course is how long these parts for each X need to be,

and that depends on the number of clauses

because we're going to attach clauses to the variables here.

In order to make this safe, we should construct this part

so that we have m of these edge crossings here

because then we know that for each clause we have an edge

where we can attach that clause to.

Now, if we have m of these crossings here

this means that we have m+1 of these groups of three vertices here

so we have 3(m+1) vertices in this part here

and then we have one more vertex here, one more vertex here

so +2 if we extended like this, and this holds true for all of the other parts here as well.

Now, for each clause but of course also going to add a vertex like so

and again this vertex here is going to represent clause 1

this vertex here is going to represent clause 2 and so until we get to clause m.

My first question for you is

how many vertices are we using to represent the variables

so to represent x₁, x₂ and so on until we get to xn

and I would like you to enter this as four numbers

and so it's going to be some number times n plus some number times m

plus some number times mn plus possibly some constant.

Please give me these four numbers here

to correctly count the number of vertices that we have here to represent variables.