形式系统(Formale System)-SAT问题

2024-03-26 12:48

本文主要是介绍形式系统(Formale System)-SAT问题,希望对大家解决编程问题提供一定的参考价值,需要的开发者们随着小编来一起学习吧!

什么是SAT问题

所谓SAT问题就是可实现性问题(Erfuellbarkeitsproblem)。即已知一个Formel F For0 ,问是否存在一个解释(Interpretation) I 使得 valI(F)=T
同时SAT问题也是一个NP完备性问题。也就是说假如存在一个确定的在多项式时间内完成的用于判定一个Formel是否可实现的的算法,那么同时也就可以得到NP=P,换言之,每一个非确定性的可于多项式时间内完成的判定问题同时也是确定性的可在多项式时间内完成的。//有点绕,总之就是说不存在咋能在多项式时间内完成的算法把???NP问题不懂啊

特定Formel的SAT问题复杂度

KNF3-KNF2-KNFDNFHorn-FormelNPNPNPO(nlogn)O(n^2)

//高项的KNF都可以通过转化化成3-KNF
//2-KNF也叫做Krom-Formel
//具体的数字不知道是怎么算出来的

Hron Formel

一个Formel A是Horn Formel,当且仅当:
1.A是KNF
2.A的每一个子项最多含有一个正的Literal

¬B1...¬BmA¬B1...¬BmAB1...BmAB1...Bm0(1)A

Hornformel可实现性测试

假如 C=D1..Dm 是一个Hornformel,那么可以通过以下算法,判定他是否可以实现:
0:假如 Di 中不存在单项式,那么算法结束,输出可实现。假如存在,那么标记所有的单项式
1:假如不存在 B1...BmK ,其中所有的 Bi 都已经标记过,那么输出可实现,算法停止
假如存在 B1...Bm0 ,并且其中的 Bi 都已经标记过,那么输出不可实现,算法停止
假如存在 B1...BmA ,并且其中的 Bi 都已经标记过,只有A还没有标记过,那么把A也给标记了,然后跳转到1
除了上述外的其他一切情况都输出可实现,然后算法停止

DPLL(Davis-Putnam-Logemann-Loveland)

补充知识

I 是Interpretation,S是Klausel的集合,C是Klausel,那么就有:
1.

valI(S)={TFCSvalI(C)=T

valI(C)={TFLC valI(L)=T

I( )=T // 表示S为空
I( )=F // 表示Klausel为空 恒假

算法

1.if S= then return 1;
2.if S then return 0;
3.if S contain singleklausel
then choose singleklausel {L} S
return DPLL( redL(S) );
else choose P atom(S)
return max{DPLL( SP ),DPLL( S¬P )}

其中:
red L (S)={red L (C)}C SLC
red L (C)=C\{ ¬L }
SP=S {{P}}
S¬P=S {{ ¬P }}

这篇关于形式系统(Formale System)-SAT问题的文章就介绍到这儿,希望我们推荐的文章对编程师们有所帮助!



http://www.chinasem.cn/article/848561

相关文章

springboot循环依赖问题案例代码及解决办法

《springboot循环依赖问题案例代码及解决办法》在SpringBoot中,如果两个或多个Bean之间存在循环依赖(即BeanA依赖BeanB,而BeanB又依赖BeanA),会导致Spring的... 目录1. 什么是循环依赖?2. 循环依赖的场景案例3. 解决循环依赖的常见方法方法 1:使用 @La

SpringBoot启动报错的11个高频问题排查与解决终极指南

《SpringBoot启动报错的11个高频问题排查与解决终极指南》这篇文章主要为大家详细介绍了SpringBoot启动报错的11个高频问题的排查与解决,文中的示例代码讲解详细,感兴趣的小伙伴可以了解一... 目录1. 依赖冲突:NoSuchMethodError 的终极解法2. Bean注入失败:No qu

MySQL新增字段后Java实体未更新的潜在问题与解决方案

《MySQL新增字段后Java实体未更新的潜在问题与解决方案》在Java+MySQL的开发中,我们通常使用ORM框架来映射数据库表与Java对象,但有时候,数据库表结构变更(如新增字段)后,开发人员可... 目录引言1. 问题背景:数据库与 Java 实体不同步1.1 常见场景1.2 示例代码2. 不同操作

如何解决mysql出现Incorrect string value for column ‘表项‘ at row 1错误问题

《如何解决mysql出现Incorrectstringvalueforcolumn‘表项‘atrow1错误问题》:本文主要介绍如何解决mysql出现Incorrectstringv... 目录mysql出现Incorrect string value for column ‘表项‘ at row 1错误报错

如何解决Spring MVC中响应乱码问题

《如何解决SpringMVC中响应乱码问题》:本文主要介绍如何解决SpringMVC中响应乱码问题,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录Spring MVC最新响应中乱码解决方式以前的解决办法这是比较通用的一种方法总结Spring MVC最新响应中乱码解

pip无法安装osgeo失败的问题解决

《pip无法安装osgeo失败的问题解决》本文主要介绍了pip无法安装osgeo失败的问题解决,文中通过示例代码介绍的非常详细,对大家的学习或者工作具有一定的参考学习价值,需要的朋友们下面随着小编来一... 进入官方提供的扩展包下载网站寻找版本适配的whl文件注意:要选择cp(python版本)和你py

解决Java中基于GeoTools的Shapefile读取乱码的问题

《解决Java中基于GeoTools的Shapefile读取乱码的问题》本文主要讨论了在使用Java编程语言进行地理信息数据解析时遇到的Shapefile属性信息乱码问题,以及根据不同的编码设置进行属... 目录前言1、Shapefile属性字段编码的情况:一、Shp文件常见的字符集编码1、System编码

Spring MVC使用视图解析的问题解读

《SpringMVC使用视图解析的问题解读》:本文主要介绍SpringMVC使用视图解析的问题解读,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录Spring MVC使用视图解析1. 会使用视图解析的情况2. 不会使用视图解析的情况总结Spring MVC使用视图

Redis解决缓存击穿问题的两种方法

《Redis解决缓存击穿问题的两种方法》缓存击穿问题也叫热点Key问题,就是⼀个被高并发访问并且缓存重建业务较复杂的key突然失效了,无数的请求访问会在瞬间给数据库带来巨大的冲击,本文给大家介绍了Re... 目录引言解决办法互斥锁(强一致,性能差)逻辑过期(高可用,性能优)设计逻辑过期时间引言缓存击穿:给

Java程序运行时出现乱码问题的排查与解决方法

《Java程序运行时出现乱码问题的排查与解决方法》本文主要介绍了Java程序运行时出现乱码问题的排查与解决方法,包括检查Java源文件编码、检查编译时的编码设置、检查运行时的编码设置、检查命令提示符的... 目录一、检查 Java 源文件编码二、检查编译时的编码设置三、检查运行时的编码设置四、检查命令提示符