This study presents a novel heuristic algorithm called the "Minimal Positive
Negative Product Strategy" to guide the CDCL algorithm in solving the Boolean
satisfiability problem. It provides a mathematical explanation for the
superiority of this algorithm over widely used heuristics such as the Dynamic
Largest Individual Sum (DLIS) and the Variable State Independent Decaying Sum
(VSIDS). Experimental results further confirm the effectiveness of this
heuristic strategy in problem-solving.

本研究提出了一种名为 “Minimal Positive Negative Product Strategy” 的新型启发式算法，用于指导 CDCL 算法解决布尔可满足性问题，它通过数学解释阐明了该算法相对于动态最大个体和变量状态独立衰减和求和等广泛使用的启发式算法的优势，实验结果进一步证实这种启发式策略在问题求解中的有效性。

新的布尔可满足性问题启发式策略：最小正负乘积策略

New Boolean satisfiability problem heuristic strategy: Minimal Positive  Negative Product Strategy

The past three decades have witnessed notable success in designing efficient
SAT solvers, with modern solvers capable of solving industrial benchmarks
containing millions of variables in just a few seconds. The success of modern
SAT solvers owes to the widely-used CDCL algorithm, which lacks comprehensive
theoretical investigation. Furthermore, it has been observed that CDCL solvers
still struggle to deal with specific classes of benchmarks comprising only
hundreds of variables, which contrasts with their widespread use in real-world
applications. Consequently, there is an urgent need to uncover the inner
workings of these seemingly weak yet powerful black boxes.
In this paper, we present a first step towards this goal by introducing an
approach called CausalSAT, which employs causal reasoning to gain insights into
the functioning of modern SAT solvers. CausalSAT initially generates
observational data from the execution of SAT solvers and learns a structured
graph representing the causal relationships between the components of a SAT
solver. Subsequently, given a query such as whether a clause with low literals
blocks distance (LBD) has a higher clause utility, CausalSAT calculates the
causal effect of LBD on clause utility and provides an answer to the question.
We use CausalSAT to quantitatively verify hypotheses previously regarded as
"rules of thumb" or empirical findings such as the query above. Moreover,
CausalSAT can address previously unexplored questions, like which branching
heuristic leads to greater clause utility in order to study the relationship
between branching and clause management. Experimental evaluations using
practical benchmarks demonstrate that CausalSAT effectively fits the data,
verifies four "rules of thumb", and provides answers to three questions closely
related to implementing modern solvers.

本文介绍了使用因果推理探究 SAT 求解器内在工作机制的方法 CausalSAT，并通过实验验证了其中四条经验法则和三个与现代 SAT 求解器实现密切相关的问题。

利用因果推理解释 SAT 求解

Explaining SAT Solving Using Causal Reasoning

The CDCL algorithm is the leading solution adopted by state-of-the-art
solvers for SAT, SMT, ASP, and others. Experiments show that the performance of
CDCL solvers can be significantly boosted by embedding domain-specific
heuristics, especially on large real-world problems. However, a proper
integration of such criteria in off-the-shelf CDCL implementations is not
obvious. In this paper, we distill the key ingredients that drive the search of
CDCL solvers, and propose a general framework for designing and implementing
new heuristics. We implemented our strategy in an ASP solver, and we
experimented on two industrial domains. On hard problem instances,
state-of-the-art implementations fail to find any solution in acceptable time,
whereas our implementation is very successful and finds all solutions.

通过嵌入特定领域的启发式方法来提高 CDCL 算法的性能并不容易，本文提出了一种通用框架来设计和实现新的启发式方法，并在两个工业领域实验中取得成功。