2509 7-6 3SAT问题
题目描述
SAT的一个实例是k个布尔变量 x 1，…， xk 的m个布尔表达式 A 1，…， Am 。若存在各布尔变量i x (1≤i≤k)的0，1 赋值，使每个布尔表达式i A (1≤i≤m)都取值1，则称布尔表达式 A1 A2 … Am 是可满足的。
★ 合取范式的可满足性问题CNF-SAT
如果一个布尔表达式是一些因子和之积，则称之为合取范式，简称CNF(Conjunctive Normal Form)。
★ k-SAT
如果一个布尔合取范式的每个乘积项最多是k个因子的析取式，就称之为k元合取范式，简记为k-CNF。一个k-SAT问题是判定一个k-CNF是否可满足。特别地，当k=3 时，3-SAT问题在NP完全问题树中具有重要地位。
★ MAX-SAT
给定k个布尔变量 x 1，…， xk的m个布尔表达式A1，…， Ak ，求各布尔变量xi (1≤i≤k)的0，1 赋值，使尽可能多的布尔表达式i A 取值1。
★ Weighted-MAX-SAT
给定k个布尔变量 x 1，…， xk的m个布尔表达式A1，…， Ak ，每个布尔表达式Ai 都有一个权值wi，求各布尔变量xi (1≤i≤k)的0，1赋值，使取值1 的布尔表达式权值之和达到最大。
对于给定的带权3-CNF，设计一个蒙特卡罗算法，使其权值之和尽可能大。
输入格式:
输入数据第一行有2个正整数k和m，分别表示变量数和布尔表达式数。接下来的m行中，每行有5 个整数w,i,j,k,0，表示相应表达式的权值为w，表达式含的变量下标分别为i,j,k，行末以0 结尾。下标为负数时，表示相应的变量为取反变量。
输出格式:
将计算出的最大权值输出
输入样例 复制
5 3 9 3 1 4 0 9 1 -5 3 0 8 2 -5 1 0
输出样例
复制
26
