摘要翻译：
本文的工作重点是改进现有的随机局部搜索(SLS)方法，以解决实际工业SAT应用领域中的布尔可满足性(SAT)实例。最近引入的SLS方法CRSat在求解此类实际情况时，通过将基于对等的局部搜索与布尔电路的非小句公式表示形式上的有限布尔约束传播相结合，显着地改进了以前提出的SLS方法。在这项工作中，我们研究了通过利用电路级结构知识来开发新的CRSat搜索启发式来进一步提高CRSat性能的可能性。为此，我们介绍和实验评估了各种搜索启发式，其中许多是由电路级启发式驱动的，这些启发式最初是在完全不同的环境中开发的，例如用于电子设计自动化应用。据我们所知，大多数启发式在SAT的SLS和更一般的约束满足问题的SLS中都是新颖的。
---
英文标题：
《Structure-Based Local Search Heuristics for Circuit-Level Boolean
  Satisfiability》
---
作者：
Anton Belov and Matti J\"arvisalo
---
最新提交年份：
2011
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Artificial Intelligence        人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--

---
英文摘要：
  This work focuses on improving state-of-the-art in stochastic local search (SLS) for solving Boolean satisfiability (SAT) instances arising from real-world industrial SAT application domains. The recently introduced SLS method CRSat has been shown to noticeably improve on previously suggested SLS techniques in solving such real-world instances by combining justification-based local search with limited Boolean constraint propagation on the non-clausal formula representation form of Boolean circuits. In this work, we study possibilities of further improving the performance of CRSat by exploiting circuit-level structural knowledge for developing new search heuristics for CRSat. To this end, we introduce and experimentally evaluate a variety of search heuristics, many of which are motivated by circuit-level heuristics originally developed in completely different contexts, e.g., for electronic design automation applications. To the best of our knowledge, most of the heuristics are novel in the context of SLS for SAT and, more generally, SLS for constraint satisfaction problems.
---
PDF链接：
https://arxiv.org/pdf/1109.2049