• 首页
  • 晞德求解器
    • SeedSAT/SeedMaxSAT求解器
    • SeedSMT求解器
    • SeedKC知识编译器
    • SeedHyPart超图划分求解器
    • SeedMIP混合整数规划求解器
  • AI产品
    • SeedModeler自动数学建模平台
    • SeedTuner高性能算法配置平台
  • 场景案例
    • 芯片设计EDA
    • 工业制造
  • 公司动态
  • 关于我们
免费试用 >

SeedSAT

布尔可满足性求解器

SeedSAT是晞德求索针对大规模布尔可满足性问题（Propositional Satisfiability Problem，简称 SAT）研发的一款高效求解器，支持SAT问题及SAT问题的增量式求解，支持计算不可满足核（UNSAT Core）。借助SeedSAT，企业可实现大规模逻辑约束问题的快速求解，为电子设计自动化 (EDA)、工业制造、密码学、软件验证及测试等领域应用场景提供核心计算引擎

SeedMaxSAT求解器是晞德求索针对最大布尔可满足性问题（Maximum Satisfiability Problem，简称 MaxSAT） 研发的一款商业级求解器。对于带硬约束和软约束的布尔逻辑公式，SeedMaxSAT求解器支持找到满足所有硬约束、并且满足最多软约束的赋值。

最大可满足性求解器

SeedMaxSAT

免费试用 >
넳 넲

  • 大规模

    支持亿级变量问题求解

  • 速度快

    在大规模问题上可快速求解

    国际SAT求解器比赛多次获得冠军 支持大规模并行、分布式求解

    支持大规模并行、分布式求解国际标准数据集多次刷新世界记录

  • 功能强大

    支持增量式求解

    支持不可满足核（UNSAT Core）的计算

    提供丰富易用的编程接口

  • 国产自主知识产权

    国内团队自主研发，拥有完全自主知识产权，保障芯片设计、工业制造、能源、军事等核心领域的数据及技术安全，为国家解决卡脖子问题提供支持

产品优势

ADVANTAGES

产品功能

FUNCTIONS AND FEATURES

对于布尔逻辑公式进行求解：

 

  • 对于可满足的公式，输出满足公式的赋值。

    1

  • 对于不可满足的公式，证明公式不可满足。

    2

  • 对于不可满足的公式，求出不可满足核。

    3

  • 对于可满足公式，进行解的随机采样。

    4

  • 对于带硬约束和软约束的布尔逻辑公式，找到满足所有硬约束、并且满足最多软约束的赋值。

    5