The 4-queen puzzle is to place four queens in a 4x4 chessboard so that no two queens attack each other by the Chess rules (i.e., they are not in the same row, the same column, or the same diagonal). Please specify the 4-queen puzzle in Propositional Logic so that the 4-queen puzzle has a model iff the puzzle has a solution.