原文
The SAT Game is a funny representation of the SAT problem. In this problem, one must find a valuation of Boolean variables (true/false) such that a Boolean CNF formula evaluates to true. A line in the game actually represents a clause, which is a disjunction of literals (variables or their negation connected by logical OR). A clause evaluates to true as soon as one of its literals is true. Since clauses are connected by logical AND, all clauses must evaluate to true so that the formula be true.