2-SAT问题(白书)
1. 定义
给定一个布尔方程,判断是否存在一组布尔变量的真值指派使整个方程为真的问题,被称为布尔方程的可满足性问题(SAT)。SAT问题是NP完全的,但对于满足一定限制条件的SAT问题,还是能够有效求解的。
如果合取范式的每一个子句中的文字个数不超过两个,那么对应的SAT问题可以称为2-SAT问题。
(a∨b)∧¬a" role="presentation" style="position: relative;">(a∨b)∧¬a(a∨b)∧¬a 令a为假而b为真,则可以满足
(a∨¬b)∧(b∨c)∧(¬c∨¬a)" role="presentation" style="position: relative;">(a∨¬b)∧(b∨c)∧(¬c∨¬a)(a∨¬b)∧(b∨c)∧(¬c∨¬a) 令a和b为真,而c为假,则可以满足
利用强联通分量分解,可以在布尔公式子句数的线性时间内解决2-SAT问题
首先利用⇒" role="presentation" style="position: relative;">⇒⇒(蕴含)将每一个子句(a∨b)" role="presentation" style="position: relative;">(a∨b)(a∨b) 改写成等价的(¬a⇒b)∧(¬b⇒a)" role="presentation" style="position: relative;">(¬a⇒b)∧(¬b⇒a)(¬a⇒b)∧(¬b⇒a)
对于每个布尔变量x,构造两个顶点分别代表x和¬x" role="presentation" style="position: relative;">¬x¬x,以⇒" role="presentation" style="position: relative;">⇒⇒关系为有向边,建立有向图。此时,如果a点能够到达b点,就表示当a为真时b也为真。因此图中的同一个强联通分量中的所有布尔值均相同。
如果存在某个布尔变量x,x和¬x" role="presentation" style="position: relative;">x和¬xx和¬x均在同一个强联通分量中,则显然无法令整个布尔公式的值为真。反之,如果不存在这样的布尔变量,那么对于每个布尔变量x,让
x所在的强联通分量的拓扑序在¬x所在的强联通分量之后⇔x为真" role="presentation" style="position: relative;">x所在的强联通分量的拓扑序在¬x所在的强联通分量之后⇔x为真x所在的强联通分量的拓扑序在¬x所在的强联通分量之后⇔x为真
就是使得该公式的值为真的一组适合的布尔变量赋值。
2. 题目讲解
(1)POJ 3683
最新文章
- SMART Goals
- ssh 命令
- 使用qmake生成Makefile
- redo和undo的区别
- Smarty笔记 和20个常用的变量操作符
- HDU 5857 Median (推导)
- Ubuntu 12.04下虚拟磁带库mhvtl的安装和使用
- MFC/VC CxImage 简单配置与使用 (完整版)
- Quartz总结(四):动态修改定时器二
- entityframework单例模式泛型用法
- python编程学习--Pygame - Python游戏编程入门(0)---转载
- ProcessingElement.h
- 视觉机器学习------KNN学习
- React componentDidMount
- jquery的json对象与字符串之间转换
- Python_oldboy_自动化运维之路_socket编程(十)
- oracle 两个逗号分割的字符串 如何判断是否其中有相同值
- 关于PKCS的文档资料
- python3.4学习笔记(十) 常用操作符,条件分支和循环实例
- 铁乐学python_Day39_多进程和multiprocess模块2