形式系统(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

相关文章

Redis 热 key 和大 key 问题小结

《Redis热key和大key问题小结》:本文主要介绍Redis热key和大key问题小结,本文给大家介绍的非常详细,对大家的学习或工作具有一定的参考借鉴价值,需要的朋友参考下吧... 目录一、什么是 Redis 热 key?热 key(Hot Key)定义: 热 key 常见表现:热 key 的风险:二、

IntelliJ IDEA 中配置 Spring MVC 环境的详细步骤及问题解决

《IntelliJIDEA中配置SpringMVC环境的详细步骤及问题解决》:本文主要介绍IntelliJIDEA中配置SpringMVC环境的详细步骤及问题解决,本文分步骤结合实例给大... 目录步骤 1:创建 Maven Web 项目步骤 2:添加 Spring MVC 依赖1、保存后执行2、将新的依赖

Spring 中的循环引用问题解决方法

《Spring中的循环引用问题解决方法》:本文主要介绍Spring中的循环引用问题解决方法,本文给大家介绍的非常详细,对大家的学习或工作具有一定的参考借鉴价值,需要的朋友参考下吧... 目录什么是循环引用?循环依赖三级缓存解决循环依赖二级缓存三级缓存本章来聊聊Spring 中的循环引用问题该如何解决。这里聊

Spring Boot中JSON数值溢出问题从报错到优雅解决办法

《SpringBoot中JSON数值溢出问题从报错到优雅解决办法》:本文主要介绍SpringBoot中JSON数值溢出问题从报错到优雅的解决办法,通过修改字段类型为Long、添加全局异常处理和... 目录一、问题背景:为什么我的接口突然报错了?二、为什么会发生这个错误?1. Java 数据类型的“容量”限制

关于MongoDB图片URL存储异常问题以及解决

《关于MongoDB图片URL存储异常问题以及解决》:本文主要介绍关于MongoDB图片URL存储异常问题以及解决方案,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐... 目录MongoDB图片URL存储异常问题项目场景问题描述原因分析解决方案预防措施js总结MongoDB图

SpringBoot项目中报错The field screenShot exceeds its maximum permitted size of 1048576 bytes.的问题及解决

《SpringBoot项目中报错ThefieldscreenShotexceedsitsmaximumpermittedsizeof1048576bytes.的问题及解决》这篇文章... 目录项目场景问题描述原因分析解决方案总结项目场景javascript提示:项目相关背景:项目场景:基于Spring

解决Maven项目idea找不到本地仓库jar包问题以及使用mvn install:install-file

《解决Maven项目idea找不到本地仓库jar包问题以及使用mvninstall:install-file》:本文主要介绍解决Maven项目idea找不到本地仓库jar包问题以及使用mvnin... 目录Maven项目idea找不到本地仓库jar包以及使用mvn install:install-file基

usb接口驱动异常问题常用解决方案

《usb接口驱动异常问题常用解决方案》当遇到USB接口驱动异常时,可以通过多种方法来解决,其中主要就包括重装USB控制器、禁用USB选择性暂停设置、更新或安装新的主板驱动等... usb接口驱动异常怎么办,USB接口驱动异常是常见问题,通常由驱动损坏、系统更新冲突、硬件故障或电源管理设置导致。以下是常用解决

Mysql如何解决死锁问题

《Mysql如何解决死锁问题》:本文主要介绍Mysql如何解决死锁问题,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,望不吝赐教... 目录【一】mysql中锁分类和加锁情况【1】按锁的粒度分类全局锁表级锁行级锁【2】按锁的模式分类【二】加锁方式的影响因素【三】Mysql的死锁情况【1

SpringBoot内嵌Tomcat临时目录问题及解决

《SpringBoot内嵌Tomcat临时目录问题及解决》:本文主要介绍SpringBoot内嵌Tomcat临时目录问题及解决,具有很好的参考价值,希望对大家有所帮助,如有错误或未考虑完全的地方,... 目录SprinjavascriptgBoot内嵌Tomcat临时目录问题1.背景2.方案3.代码中配置t