Programming in Propositional Logic article notation question

Question

I was reading this article about propositional logic and transforming problems to SAT. The author often uses the following notation (taken from Dominating set section):

I don't understand what $[v,i]$ and $[w,i]$ stand for in $at\_most\_one$ and $at\_least\_one$ parts. I checked the paper twice and didn't find the part where he defines this notation. Has anyone already seen this notation and knows what it means? Why is $i$ needed? Can anybody provide example for a simple graph and for some K (2 or 3).

Answer 1

The set $X$ is a collection of ordered pairs $[v,i]$ (this is just a strange notation for an ordered pair), in which $v$ is a vertex and $i$ is an index from $1$ to $k$. Informally, $[v,i] \in X$ means that $v$ is the $i$th vertex in the dominating set. The formula $F$ states two things:

• There is at most one $i$th vertex (i.e., $X$ doesn't contain $[v,i],[u,i]$ for $v \neq u$).
• The vertices in $X$ form a dominating set.

The reason we want the index $i$ is that the logic isn't strong enough to count the size of $X$. It is strong enough to express "at most one" and "at least one", so we use this particular encoding to be able to express "the dominating set has size at most $k$".