# Programming in Propositional Logic article notation 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).

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$$".