Is there a standard quantifier notation for an exact number of true values?

Question

When working with SAT Solvers, I need to write quantifiers that give the total number of true values. The usual quantitiers $\forall$ and $\exists$ do not suffice. Is there a standard notation for writing the following statements?

• Exactly one of $x_1, x_2, x_3, x_4$ is true.
• At least two of $x_1, x_2, x_3, x_4$ are true.
• No more than two of $x_1, x_2, x_3, x_4$ are true.

Answer 1

See Generalized quantifiers :

$(∃_{=n})$ or $(∃^{=n})$ for "exactly $n$".

And :

$(∃^{\ge n})$ for "at least $n$".

You can see also : Heinz-Dieter Ebbinghaus & Jörg Flum, Finite Model Theory, Springer (2nd ed., 1999), Ch.3.4 Logics with Counting Quantifiers, page 58-on.