4.7 Article

Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions

期刊

ARTIFICIAL INTELLIGENCE
卷 299, 期 -, 页码 -

出版社

ELSEVIER
DOI: 10.1016/j.artint.2021.103559

关键词

SAT solving; Multilinear optimization; Fourier analysis on Boolean functions; Walsh-Hadamard transform

资金

  1. NSF [IIS-1527668, CCF-1704883, IIS-1830549, CCF-1907936, CNS-2003137]
  2. DoD MURI [N00014-20-1-2787]
  3. Maryland Procurement Office

向作者/读者索取更多资源

The Boolean SATisfiability problem is crucial in computer science, and recent progress in SAT solvers, particularly in Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers, has been notable. However, there is still a lack of general approach for handling non-CNF constraints. The designed FouriersAT solver utilizes Fourier Analysis to address systems with different types of constraints, leveraging gradient information for local improvements, demonstrating effectiveness on certain benchmarks.
The Boolean SATisfiability problem (SAT) is of central importance in computer science. Although SAT is known to be NP-complete, progress on the engineering side-especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers-has been remarkable. Yet, while SAT solvers, aimed at solving industrial-scale benchmarks in Conjunctive Normal Form (cNF), have become quite mature, SAT solvers that are effective on other types of constraints (e.g., cardinality constraints and xoFs) are less well-studied; a general approach to handling non-CNF constraints is still lacking. To address the issue above, we design FouriersAT,(1) an incomplete SAT solver based on Fourier Analysis (also known as Walsh-Fourier Transform) of Boolean functions, a technique to represent Boolean functions by multilinear polynomials. By such a reduction to continuous optimization, we propose an algebraic framework for solving systems consisting of different types of constraints. The idea is to leverage gradient information to guide the search process in the direction of local improvements. We show this reduction enjoys interesting theoretical properties. Empirical results demonstrate that FourierSAT can be a useful complement to other solvers on certain classes of benchmarks. (C) 2021 Elsevier B.V. All rights reserved.

作者

我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。

评论

主要评分

4.7
评分不足

次要评分

新颖性
-
重要性
-
科学严谨性
-
评价这篇论文

推荐

暂无数据
暂无数据