sat-推理相关文献

Hantao Zhang:
SATO: An Efficient Propositional Prover. CADE 1997: 272-275

@inproceedings{DBLP:conf/cade/Zhang97,
  author       = {Hantao Zhang},
  editor       = {William McCune},
  title        = {{SATO:} An Efficient Propositional Prover},
  booktitle    = {Automated Deduction - CADE-14, 14th International Conference on Automated
                  Deduction, Townsville, North Queensland, Australia, July 13-17, 1997,
                  Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {1249},
  pages        = {272--275},
  publisher    = {Springer},
  year         = {1997},
  url          = {https://doi.org/10.1007/3-540-63104-6\_28},
  doi          = {10.1007/3-540-63104-6\_28},
  timestamp    = {Tue, 17 Jan 2023 12:12:52 +0100},
  biburl       = {https://dblp.org/rec/conf/cade/Zhang97.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Li00,
author = {Chu Min Li},
editor = {Henry A. Kautz and
Bruce W. Porter},
title = {Integrating Equivalency Reasoning into Davis-Putnam Procedure},
booktitle = {Proceedings of the Seventeenth National Conference on Artificial Intelligence
and Twelfth Conference on on Innovative Applications of Artificial
Intelligence, July 30 - August 3, 2000, Austin, Texas, {USA}},
pages = {291--296},
publisher = {{AAAI} Press / The {MIT} Press},
year = {2000},
url = {http://www.aaai.org/Library/AAAI/2000/aaai00-045.php},
timestamp = {Tue, 05 Sep 2023 09:10:47 +0200},
biburl = {https://dblp.org/rec/conf/aaai/Li00.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}

Abstract

Equivalency clauses (Xors or modulo 2 arithmetics) represent a common structure in the SAT-encoding of many hard real-world problems and constitute a major obstacle to DavisPutnam (DP) procedure. We propose a special look-ahead technique called equivalency reasoning to overcome the obstacle and report on the performance of an equivalency reasoning enhanced DP procedure on SAT instances containing equivalency clauses derived from problems in parity learning, cryptographic key search and model checking. Our results show that integrating equivalency reasoning renders easy many problems which were beyond DP’s reach. We also compare equivalency reasoning with general CSP look-back techniques on equivalency clauses.

译文：等价子句（Xors 或模 2 算术）代表了许多现实世界困难问题的 SAT 编码中的常见结构，并构成了 DavisPutnam （DP） 程序的主要障碍。我们提出了一种称为等价推理的特殊前瞻技术，以克服障碍并报告等价推理增强DP程序在SAT实例上的性能，该实例包含从奇偶校验学习、加密密钥搜索和模型检查中的问题派生的等价子句。我们的结果表明，整合等价推理可以解决许多DP无法解决的问题。我们还将等价推理与等价子句的一般 CSP 回溯技术进行了比较。

在这些问题上，DP程序效率低下的原因似乎是等效条款在整个解决过程中给出的单元子句很少，而在其他问题上，DP程序往往在一定程度上处理了许多单位条款。

另一方面，在等效子句中固定一个变量通常会产生许多等效文字，从中可以进行等效推理，以弥补单位传播的无效。

在本文中，我们展示了如何整合等价推理来解决包含等价子句(称为EQ部分)和其他CNF子句(称为CNF部分)的问题。