• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Procedia Computer Science >A parallel SAT solving algorithm based on improved handling of conflict clauses
【24h】

A parallel SAT solving algorithm based on improved handling of conflict clauses

机译：基于改进冲突条款处理的并行SAT求解算法

获取原文
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

In this study, a new parallel algorithm for solving Boolean satisfiability problem (SAT) is suggested. This algorithm is based on the Conflict Driven Clause Learning (CDCL) algorithm. Given an original SAT instance, CDCL is launched on it. Some types of conflict clauses, which are produced by CDCL, are collected. Then the collected clauses are employed to construct a family of different SAT instances. In particular, each SAT instance from a family is produced by adding some subset of the collected conflict clauses to an initial set of clauses (which belong to the original instance). In order to solve the original SAT instance, it is sufficient to solve at least one SAT instance from the constructed family. The proposed algorithm was implemented in the form of a parallel SAT solver. It was compared with two high ranked state-of-the-art parallel solvers. As a test set, we used SAT instances which encode cryptanalysis of three keystream generators: summation generator, threshold generator, and Gifford generator. According to computational experiments, our solver outperforms those two solvers.
机译：在这项研究中，提出了一种新的并行算法来解决布尔可满足性问题（SAT）。此算法基于冲突驱动子句学习（CDCL）算法。给定原始SAT实例，就可以在其上启动CDCL。收集CDCL生成的某些类型的冲突条款。然后，将收集的子句用于构造一系列不同的SAT实例。特别是，通过将收集到的冲突子句的某些子集添加到初始子句集（属于原始实例）中，来产生一个族的每个SAT实例。为了求解原始的SAT实例，解决至少一个来自构造族的SAT实例就足够了。该算法以并行SAT求解器的形式实现。将其与两个顶级高级并行求解器进行了比较。作为测试集，我们使用了SAT实例，该实例对三个密钥流生成器（求和生成器，阈值生成器和Gifford生成器）的密码分析进行编码。根据计算实验，我们的求解器优于这两个求解器。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号