2-SAT问题
2015-06-07 20:38
239 查看
2-SAT问题
利用强连通分量分解，可以在布尔公式句数的线段时间内解决２－ＳＡＴ问题，
首先利用=>（蕴含）将每个子句（ＡvＢ）改写为等价形式（非Ａ=>Ｂ）＾（Ａ=>非 Ｂ）这样对每个布尔变量ｘ构造两个顶点分别代表Ｘ和非ｘ，以=>关系为边建立有向图，此时，如果图上的ａ点能够达到ｂ点的话，就表示ａ为真时ｂ一定为真．因此，该图中同一个强连通分量所含的所有文字的布尔值均相同．
如果存在非ｘ和ｘ在同一强连通分量中，则显然无法令整个布尔公式的值为真．
反之，如果不存在这样的布尔变量则可以对于每个布尔值赋值使得该公式为真
利用强连通分量分解，可以在布尔公式句数的线段时间内解决２－ＳＡＴ问题，
首先利用=>（蕴含）将每个子句（ＡvＢ）改写为等价形式（非Ａ=>Ｂ）＾（Ａ=>非 Ｂ）这样对每个布尔变量ｘ构造两个顶点分别代表Ｘ和非ｘ，以=>关系为边建立有向图，此时，如果图上的ａ点能够达到ｂ点的话，就表示ａ为真时ｂ一定为真．因此，该图中同一个强连通分量所含的所有文字的布尔值均相同．
如果存在非ｘ和ｘ在同一强连通分量中，则显然无法令整个布尔公式的值为真．
反之，如果不存在这样的布尔变量则可以对于每个布尔值赋值使得该公式为真
内容来自用户分享和网络整理，不保证内容的准确性，如有侵权内容，可联系管理员处理 
相关文章推荐
- redis:hash数据类型与操作
- Markdown学习（四）
- QString转char*
- SQL数据库基本操作语句 详解及用途
- 数学模板
- 收藏的学习地址
- Data API
- Android内核开发：图解Android系统的启动过程
- Android内核开发：图解Android系统的启动过程
- 为什么我希望用C而不是C++来实现ZeroMQ
- Redis 起步
- 理解 HTTPS 协议
- JAVA类的序列化
- 强连通分量分解
- C++实现反射机制(二)
- Android应用AsyncTask处理机制详解及源码分析
- java中的IO流（2）----读取文本数据
- 团队组建及项目启动（项目一补发）
- 团队作业-第三周-设计类图
- varnish及其应用（二）