SeedSMT
可满足性模理论求解器
可满足性模理论（Satisfiability Modulo Theories，简称 SMT）是在布尔可满足性问题（SAT）基础上的扩展，允许在 “布尔逻辑” 之外引入整数、实数、数组、字符串等特定领域的理论（如算术理论、数组理论），是计算机科学领域形式化方法与自动推理方向的关键技术。
晞德所研发的SeedSMT求解器是专门用于判定这类复杂约束问题是否可满足的工具，在软件工程领域和电子设计自动化（EDA）领域都有重要应用。
产品功能
FUNCTIONS AND FEATURES
对于可满足性模理论（SMT）公式：
对于可满足的公式，输出满足公式的赋值。
1
对于不可满足的公式，证明公式不可满足。
2
对于带硬约束和软约束的SMT公式，找到满足所有硬约束，并且满足最多软约束的赋值。
3
产品性能
PERFORMANCE
1.面对SMT-LIB（算术理论和位向量理论）国际权威测试集：
a.平均求解速度较主流开源求解器提升30%；
b.成功求解 SMT-LIB 中大量（约1/5至1/3）主流开源求解器无法解决的实例。
2.相比主流开源采样工具，仅需一半数量的测试用例，即可达到相同覆盖率。
