How do you encode in a propositional logic formula that in an N x N chessboard you have at least M pieces? (piece type doesn't matter, only the fact that square sq(i, j) is occupied).

The formula must be true iff at least M squares are occupied (if you encode occupied as sq(i, j) then you need at least M of these literals true).