Heuristics are crucial in SAT solvers, while no heuristic rules are suitable
for all problem instances. Therefore, it typically requires to refine specific
solvers for specific problem instances. In this context, we present AutoSAT, a
novel framework for automatically optimizing heuristics in SAT solvers. AutoSAT
is based on Large Large Models (LLMs) which is able to autonomously generate
code, conduct evaluation, then utilize the feedback to further optimize
heuristics, thereby reducing human intervention and enhancing solver
capabilities. AutoSAT operates on a plug-and-play basis, eliminating the need
for extensive preliminary setup and model training, and fosters a Chain of
Thought collaborative process with fault-tolerance, ensuring robust heuristic
optimization. Extensive experiments on a Conflict-Driven Clause Learning (CDCL)
solver demonstrates the overall superior performance of AutoSAT, especially in
solving some specific SAT problem instances.

AutoSAT 是一种自动优化 SAT 解算器中启发式算法的新框架，基于大型模型（LLMs），它能够自主生成代码、进行评估，并利用反馈进一步优化启发式算法，从而减少人工干预并增强解算器的能力。AutoSAT 在插拔式基础上操作，不需要广泛的预备设置和模型训练，促进了具有容错性的思维链的合作过程，确保了强大的启发式优化。对 Conflict-Driven Clause Learning (CDCL) 解算器进行的大量实验证明了 AutoSAT 的整体优异性能，特别是在解决一些特定的 SAT 问题实例中。

AutoSAT: 通过大型语言模型自动优化 SAT 求解器

AutoSAT: Automatically Optimize SAT Solvers via Large Language Models

Benchmarking is an important tool for assessing the relative performance of
alternative solving approaches. However, the utility of benchmarking is limited
by the quantity and quality of the available problem instances. Modern
constraint programming languages typically allow the specification of a
class-level model that is parameterised over instance data. This separation
presents an opportunity for automated approaches to generate instance data that
define instances that are graded (solvable at a certain difficulty level for a
solver) or can discriminate between two solving approaches. In this paper, we
introduce a framework that combines these two properties to generate a large
number of benchmark instances, purposely generated for effective and
informative benchmarking. We use five problems that were used in the MiniZinc
competition to demonstrate the usage of our framework. In addition to producing
a ranking among solvers, our framework gives a broader understanding of the
behaviour of each solver for the whole instance space; for example by finding
subsets of instances where the solver performance significantly varies from its
average performance.

本文介绍了一种利用现代约束编程语言中的类级别模型自动生成基准实例数据，以重点生成有效和有信息量的基准实例的框架，可评估可行解决方案的相对性能。使用此框架对五个问题进行研究，不仅排名解算器，还通过查找解算器表现显著变化的实例子集，为我们提供了一个更完整的解算器行为理解。

生成富有信息的基准示例的框架

A Framework for Generating Informative Benchmark Instances

Simultaneously utilizing several complementary solvers is a simple yet
effective strategy for solving computationally hard problems. However, manually
building such solver portfolios typically requires considerable domain
knowledge and plenty of human effort. As an alternative, automatic construction
of parallel portfolios (ACPP) aims at automatically building effective parallel
portfolios based on a given problem instance set and a given rich design space.
One promising way to solve the ACPP problem is to explicitly group the
instances into different subsets and promote a component solver to handle each
of them.This paper investigates solving ACPP from this perspective, and
especially studies how to obtain a good instance grouping.The experimental
results showed that the parallel portfolios constructed by the proposed method
could achieve consistently superior performances to the ones constructed by the
state-of-the-art ACPP methods,and could even rival sophisticated hand-designed
parallel solvers.

本文研究从不同的集合中获取实例，然后搭建自动构造的并行处理程序，而且结果已经表明该方法可以达到设计良好的对手方法所实现的结果。