中文 英语
知识中心
导航
知识中心

坐在解算器

用来解决问题的算法
受欢迎程度

描述

SAT求解器接受一个布尔表达式,并找出变量是否可以替换为true或false,以便公式的计算结果为true。SAT是一个属于np完备类的问题,事实上,它是有史以来第一个被证明属于这类的问题。这意味着没有已知的算法可以有效且正确地求解所有可能的输入实例。实际上,这意味着不知道需要多长时间才能找到解决方案,但许多问题将在更短的时间内得到解决。

这种限制并没有阻止它被用于解决形式验证中的许多复杂问题,而是使用更有效的启发式方法。在EDA中,SAT求解器用于测试模式生成、电路延迟计算、逻辑优化、组合等价性检查、有界模型检查和功能测试向量生成等不同的任务。启发式方法利用了数字系统中常见的一些底层结构。

Baidu