Preparing NOJ

3SAT问题

1000ms 65536K

Description:

 

SAT的一个实例是k个布尔变量1 x ,…, k x m个布尔表达式1 A ,…, m A 。若存在各布尔变量i x (1ik)01 赋值,使每个布尔表达式i A (1im)都取值1,则称布尔表达式1 A 2 A m A 是可满足的。

★ 合取范式的可满足性问题CNF-SAT

如果一个布尔表达式是一些因子和之积,则称之为合取范式,简称CNF(ConjunctiveNormal Form)。这里的因子是变量xx。例如( )( )( ) 1 2 2 3 1 2 3 x + x x + x x + x + x 就是一个合取范式,而1 2 3 x x + x 就不是合取范式。

k-SAT

如果一个布尔合取范式的每个乘积项最多是k个因子的析取式,就称之为k元合取范式,简记为k-CNF。一个k-SAT问题是判定一个k-CNF是否可满足。特别地,当k=3 时,3-SAT问题在NP完全问题树中具有重要地位。

MAX-SAT

给定k个布尔变量1 x ,…, k x m个布尔表达式1 A ,…, m A ,求各布尔变量i x (1ik)01 赋值,使尽可能多的布尔表达式i A 取值1

Weighted-MAX-SAT

给定k个布尔变量1 x ,…, k x m个布尔表达式1 A ,…, m A ,每个布尔表达式i A 都有一个权值wi,求各布尔变量i x (1ik)01赋值,使取值1 的布尔表达式权值之和达到最大

对于给定的带权3-CNF,设计一个蒙特卡罗算法,使其权值之和尽可能大。

Input:

 输入数据的第一行有2个正整数km,分别表示变量数和布尔表

达式数。接下来的m行中,每行有5 个整数w,i,j,k,0,表示相应表达式的权值为w,表达式含的变量下标分别为i,j,k,行末以0 结尾。下标为负数时,表示相应的变量为取反变量。

Output:

 输出计算出的最大权值

Sample Input:

5 3
9 3 1 4 0
9 1 -5 3 0
8 2 -5 1 0

Sample Output:

26

Note:

 

本题由旧版NOJ导入,来源:算法设计与实验题解

Info

NOJ

Provider NOJ

Code NOJ1343

Tags

Submitted 0

Passed 0

AC Rate 0%

Date 04/20/2019 10:03:10

Related

Nothing Yet