买专利卖专利找龙图腾，真高效！ 查专利查商标用IPTOP,全免费！专利年费监控用IP管家,真方便！

龙图腾网获悉中国科学院软件研究所申请的专利一种基于组合与问题分解的SMT分布式求解方法和系统获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN119088548B 。

龙图腾网通过国家知识产权局官网在2025-07-15发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202411121141.9，技术领域涉及：G06F9/50；该发明授权一种基于组合与问题分解的SMT分布式求解方法和系统是由赵梦宇;蔡少伟设计研发完成，并于2024-08-15向国家知识产权局提交的专利申请。

本一种基于组合与问题分解的SMT分布式求解方法和系统在说明书摘要公布了：本发明属于计算机技术领域，涉及一种基于组合与问题分解的SMT分布式求解方法和系统。该方法包括：Leader进程为待求解的SMT问题分配Worker进程；Leader进程将原问题作为根节点加入划分树，并在求解过程中持续更新划分树的信息；Leader进程中的任务生成器产生任务并加入任务缓存队列，任务调度器对队列中的任务进行调度，向Worker进程分配任务，包括预处理化简任务、子节点生成任务和组合求解任务；Worker进程根据Leader进程的控制信号执行相关任务；Leader进程监听并收集来自各个Worker进程的任务运行结果，进而得到SMT问题的求解结果。本发明实现了高性能的分布式SMT求解器，具备普适性和高可扩展性，能最大限度地利用计算资源，提高求解效率。

本发明授权一种基于组合与问题分解的SMT分布式求解方法和系统在权利要求书中公布了：1.一种基于组合与问题分解的SMT分布式求解方法，其特征在于，包括以下步骤： Leader进程为待求解的SMT问题分配Worker进程； Leader进程将原问题作为根节点加入划分树，并在求解过程中持续更新划分树的信息；Leader进程中的任务生成器产生任务并加入任务缓存队列，任务调度器对队列中的任务进行调度，向Worker进程分配任务，包括预处理化简任务、子节点生成任务和组合求解任务； Worker进程根据Leader进程的控制信号执行相关任务； Leader进程监听并收集来自各个Worker进程的任务运行结果，进而得到SMT问题的求解结果； 所述任务生成器根据划分树的状态与求解信息，不断生成任务并加入任务缓存队列；对于所有子节点对应的子问题公式，所述任务生成器首先为其生成预处理化简任务，以提高后续求解以及子问题划分的效率和质量；然后，所述任务生成器根据当前的Leader进程的全局信息，为节点生成子节点生成任务和组合求解任务；所述子节点生成任务启发式地配置子节点生成数量和划分种类，所示组合求解任务启发式地配置串行求解器种类、参数和求解时长； 在初始阶段，一个节点只生成一个组合求解任务，随着求解进行，若遇到任务不饱和及Worker空闲率较高的情况，则适当增加同一个节点的组合求解任务数，以尽可能的避免计算资源的浪费；在任务不饱和时，任务调度器优先执行子节点生成任务，当没有待运行的子节点生成任务时，才将组合求解任务分配给Worker执行；所述Worker空闲率较高定义为，当空闲的Worker数量超过阈值pw的时长超过阈值Tw，并且子节点生成任务的平均运行时长超过阈值Tp时；当Leader进程发现Worker空闲率较高时，将子节点生成任务中的关键参数即每次划分所生成的子任务数量Np加一，并且将Tw设置为1.5×Tw，Leader将同一个节点的组合求解任务数Nport加一； 所述Worker进程包含预处理器、划分器和串行求解器，按照以下步骤执行相关任务： 预处理化简：调用预处理器对指定的任务进行化简，完成后将化简后的子问题传递给Leader进程，并加入任务缓冲队列；所述预处理化简包括：将给定任务对应的位向量公式解析并转化为DAG进行存储，在所维护的DAG上进行一系列约束传播，推理并维护变量的可行域与固定赋值，合并等价变量，并将原问题中的冗余语句进行剔除，从而减小问题规模，缩小搜索空间；所述预处理化简还包括：位向量算数等式处理、标准化、整数平展、三层重写、无约束变量消除、纯文字消除、等价子句替换； 子节点生成：调用划分器对指定任务按照术语级划分或变量级划分生成指定数量的子节点；所述术语级划分是指在SAT的布尔文字级别，通过指定不同的文字布尔赋值来进行问题划分；所述变量级划分是指深入到SMT的理论层面，通过对应理论下的约束传播技术，收集对应理论下的变量可行域，并在此基础上对理论变量进行启发式划分，从而产生子问题； 组合求解：调用指定的串行求解器并使用指定的策略求解指定任务； 任务终止：终止当前Worker进程目前进行的任务。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人中国科学院软件研究所，其通讯地址为：100190 北京市海淀区中关村南四街4号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。