Counting with two variables

We consider the two-variable fragment of first-order logic with counting quantifiers. We show that this logic lacks the finite model property, but that its satisfiability and finite satisfiability problems are both nevertheless in NExpTime. Our proof employs the results on integer linear programming obtained in the previous chapter. We also establish parametrized complexity bounds concerning the satisfiability problem for the two-variable fragment with counting quantifiers.