SAT问题

《实验二SAT问题 》实验报告 题目 SAT问题 姓名及分工 日期 2012/11/23 问题描述 SAT问题也称为合取范式的可满足问题，一个合取范式形如：A1∧A2∧…∧An，子句Ai（1≤i≤n）形如：a1∨a2∨…∨ak，其中，ai称为文字，为某一布尔变量或该布尔变量的非。SAT问题是指：是否存在一组对所有布尔变量的赋值（TRUE或FALSE），使得整个合取范式取值为真。 2. 实验目的 （1）掌握NP完全问题的特点； （2）理解这样一个观点：NP完全问题的算法具有指数时间，而指数时间算法的计算时间随着问题规模的增长而快速增长。 3. 实验要求 （1）设计算法求解SAT问题； （2）设定问题规模为3、5、10、20、50，设计实验程序考察算法的时间性能。 算法思路 1.将一个长度为n的二进制串s初始化为00…0； 2.循环直到串s为11…1 2.1 将二进制串s代入给定的合取范式中； 2.2 若合取范式取值为TRUE，则将串s作为结果输出，算法结束； 2.3 否则，将串s加1； 3. 输出“无解” (对于合取范式，可以手工输入，也可以在程序开