SAT问题也称为合取范式的可满足问题，一个合取范式形如：A1∧A2∧…∧An，子句Ai（1≤i≤n）形如：a1∨a2∨…∨ak，其中ai为文字，为某一布尔变量或该布尔变量的非。SAT问题是指：是否存在一组对所有布尔变量的赋值（TRUE或FALSE），使得整个合取范式取指为真。-SAT problem, also known as conjunctive normal to meet a conjunctive normal form: A1 ∧ A2 ∧ ... ∧ An clause Ai (1 ≤ i ≤ n) of the form: a1 ∨ a2 ∨ ... ∨ ak ai to the text, is a Boolean variable or non Boolean variables. SAT problem is: Is there a group assignment of all Boolean variable (TRUE or FALSE), and makes the whole conjunctive normal fetch is true.