标签：Applied Modulo Satisfiability 求解 encrypted SMT key message SAT

【Applied Algebra】可满足性模理论(Satisfiability Modulo Theories)入门

摘要:SMT问题是在特定理论下判定一阶逻辑公式可满足性问题.它在很多领域,尤其是形式验证、程序分析、软件测试等领域,都有重要的应用.本文介绍了SMT问题的基本概念、相关定义以及目前的主流理论.

从SAT到SMT

SAT(satisfiability)问题指的是命题逻辑公式的可满足性问题.随着研究的深人,人们发现SAT在表达能力上有很大的局限性,许多应用用SAT进行编码并不是很明智的选择,它们需要比SAT更强的表达方式.在这种形势下,将SAT问题扩展为SMT,经过扩展,SMT能比SAT更好地表达一些人工智能和形式化方法领域内的问题,比如在资源规划、时序推理、编译器优化等很多方面用到了SMT.

SMT的全称是Satisfiability Modulo Theories,可被翻译为"可满足性模理论",“多理论下的可满足性问题"或者"特定(背景)理论下的可满足性问题”,其判定算法被称为SMT求解器.简单地说,一个SMT公式是结合了理论背景的逻辑公式,其中的命题变量可以代表理论公式.对于SMT的研究起源于20世纪70年代末80年代初,当时的一些学者为形式化方法设计了一些判定算法,这些算法可以看作最早的SMT求解器;到了20世纪90年代,人们开始研究能处理大规模工业界问题的SMT求解技术.最近几年在工业界和学术界,这类技术均得到了迅猛的发展.而SMT求解器也被集成到一些大型工具中,比如HOL/Isabelle、ESC/Java2、ACL2、UCLID、BLAST、ureka,CUTE和PEX等.

SAT问题回答某个命题逻辑公式的可满足性,如:

A ∧ B ∨ ¬ C A \wedge B \vee \neg C A∧B∨¬C

但实际中的公式却往往是这样的(带有谓词,以表达更复杂的问题逻辑):

a + b < c ∧ f ( b ) > c ∨ c > 0 a+b<c \wedge f(b)>c \vee c>0 a+b<c∧f(b)>c∨c>0

SMT求解的过程就是探索如何判断这样公式的可满足性;从逻辑学角度来看, a + b < c a+b<c a+b<c或者

标签：Applied,Modulo,Satisfiability,求解,encrypted,SMT,key,message,SAT
来源： https://blog.csdn.net/hanss2/article/details/120980591

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。