2022竞赛新方法学习1--学习Proceedings of SAT Competition 2022 : Solver and Benchmark Descriptions

1. Armin Biere Mathias Fleury

弗莱堡大学，德国

GIMSATUL, ISASAT, KISSAT

GIMSATUL——2022年提交的多线程的求解器，参加parallel组。

ISASAT, KISSAT —— 2022年提交的顺序求解器，参加main组。

笔记：

（1-1）内部嵌入式SAT求解器KITTEN来查找从候选变量的环境子句及其邻近子句;用于find backbones and equivalent literals 。

version “KISSAT SC2021 SWEEP” submitted to the SAT Competition 2021——sweeping算法通过替换在扫描期间已经确定等价的字面量和更仔细地调度和重新调度候选变量，特别是在相同的扫描阶段，得到了改进。

（1-2） non-recursive model rotation

IMPROVED SWEEPING IN KISSAT is inspired by non-recursive model rotation [2] used in MUS extraction。

新的模型翻转尝试翻转KITTEN返回的最后一个模型中指定文字的值，如果结果的新赋值仍然满足公式，则成功。如果成功，则更新模型。否则，如果翻转使公式证伪，最后一个模型不被触及。

（2-1）2022年提交的“KISSAT SC2022 BULKY”版继承了2021年提交的“KISSAT SC2021 SWEEP版”[1]的大部分功能，但包括以下更改:

added ACIDS [3] branching variable heuristics (disabled)  添加ACIDS[3]分支变量启发式(禁用)
added CHB [4] variable branching heuristic (but disabled by default) inspired by the success of ’kissat mab’ [5]
faster randomization of phases in the Kitten sub-solver 在Kitten子求解器中更快的相位随机化
literal flipping for faster refinement during sweeping 字面翻转以在扫描期间更快地细化
disabled priority queue for variable elimination (elimination attempts follow the given fixed variable order)禁用变量消除优先队列
disabled by default reusing the trail during restarts 默认情况下禁用在重启期间重用跟踪
disabled by default hyper ternary resolution 默认禁用超三元分辨率
initial local search through propagation (similar to ”warmup” runs of Donald Knuth [6] and how local search is initialized in ”ReasonLS” solvers by Shaowei Cai [7]) 通过传播进行初始的本地搜索
actual watch replacement of true literals during unit propagation instead of just updating the blocking literal (as suggested by Norbert Manthey [8]) 在单元传播过程中替换真正的字面量，而不是仅仅更新阻塞字面量
fixed clause length and variable occurrences limits during variable elimination instead of dynamically increasing 固定子句长度和变量出现限制在变量消除而不是动态增加

（3-1）KISSAT SC2022 LIGHT AND KISSAT SC2022 HYPER

为了把重点放在KISSAT最重要的功能上，我们去掉了那些在最后三个比赛基准中没有显著提高表现的功能:

autarky reasoning 自给自足的推理
eager forward and backward subsumption during variable elimination (global forward subsumption only) 变量消去过程中的急切向前和向后包容
caching and reusing of minima during local search 在本地搜索中缓存和重用最小值
failed literal probing   文字failed的调查
transitive reduction of the binary implication graph 二值蕴涵图的传递约简
eager subsumption of recently learned clauses   急切地subsumption最近学过的从句
XOR gate extraction during variable elimination  变量消除过程中的异或门提取
delaying of inprocessing functions based on formula size 基于公式大小的延迟处理
vivification of irredundant clauses 非冗余从句的生动化
keeping untried elimination, backbone and vivification candidates for next inprocessing round (removed options) 子句删除策略改进时可以重点参考。
initial focused mode phase limited only by conflicts now (not as before also by ticks)  最初的集中模式阶段只受到现在冲突的限制
The light version also removes hyper binary resolution, enabling the use of more variables 轻版本还删除了超二进制分辨率，支持使用更多变量.

2. Watch Sat and LTO for CaDiCaL and Kissat

Norbert Manthey
nmanthey@conp-solutions.com      Dresden, Germany

CADICAL_watch-sat-flto

KISSAT_watch-sat-flto

笔记

（1）对编译过程进行了针对性设置与优化；

link time optimization (LTO)

LTO can be enabled by adding -flto to the compiler invocation.

（2）针对minisat和cadical观察体系在传播中的处理过程异同进行了对比叙述。

MINISAT 2.2 2.1 [2] started to use a blocking literal. When propagating a clause, first the truth value of the blocking literal is checked. In case the blocking literal is satisfied, the related clause is known to be satisfied. Therefore, the clause does not have to be processed further.   翻译： MINISAT 2.2 2.1[2]开始使用阻塞字面值。在传播子句时，首先检查阻塞字面值的真值。如果阻塞字面值被满足，则已知相关子句被满足。因此，该子句不需要进一步处理，Always Watching the Satisfied Literal。

One difference between CADICAL and MINISAT 2.2 based solvers is the way how they treat these satisfied clauses.

CADICAL skip updating watch lists. Instead, CADICAL implements further extensions, like memorizing the literal in a clause that was tested when last processing the clause [4]. 译文：CADICAL跳过更新监视列表。相反，CADICAL实现了进一步的扩展，比如记住上次处理子句[4]时测试的子句中的文字。

下面这段，基本内容没有搞明白：

Just Update the Blocking Literal: As an alternative,
CADICAL keep watching the current literal, which is now
falsified, but updates the blocking literal to the satisfied literal.
While this breaks the assumption that falsified literals are only
watched for conflict clauses or unit clauses, we still know that
the clause is satisfied. Hence, breaking this assumption does
not have consequences. The positive effect is that the clause
does not have to be removed from the current watch list. This
results in no cache miss, nor a TLB miss. However, when the
search progresses, after backtracking, the same clause might
need to be processed again. In case the satisfied literal is
still satisfied, only the blocking literal has to be processed.
Otherwise, backtracking also removed the assignment for the
blocking literal, so that the whole clause needs to be processed
again.

Preliminary testing with MERGESAT when just up-dating the blocking literal of a clause resulted in a performance
degradation. 在使用MERGESAT进行初步测试时，仅仅更新子句的阻塞文字就会导致性能下降。

（3）一句很重要的结论式表述：

Not processing a satisfied clause during propagation soon again can result in a different order of propagated literals,
as well as different conflicts, and consequently in different heuristic updates and many different follow-up search steps
of the solver. Hence, performance differences can not only be attributed to lower or higher compute resource utilization. 译文：在传播过程中没有很快处理一个满意的子句，可能会导致传播文字的顺序不同，以及不同的冲突，从而导致不同的启发式更新和求解器的许多不同的后续搜索步骤。因此，性能差异不仅可以归因于较低或较高的计算资源利用率。

3. SEQFROST at the SAT Race 2022

Sequential Formal ReasOning about SaTisfiability

译文：可满足性的顺序形式推理

SEQFROST is a new solver mostly rewritten from scratch based on our last year submission [1] with efficient data structures and many code optimizations.

This year, we observed a large amount of time is spent on function calls in Boolean Constraint Propagation (BCP) and data sorting especially in Multiple-Decision Making (MDM) and inprocessing.

主要技术改进：

（1）Thus, we resorted to inlined code and pointer prefetching in BCP and replaced the standard sort procedure with faster modern alternatives, e.g., pdqsort. 我们在BCP中使用内联代码和指针预取，并使用更快的现代替代方法(例如pdqsort)取代标准排序过程。

（2）Further, we augment the Multi-Arm Bandit (MAB) rewarding scheme as implemented in the last year winner KISSAT-MAB to MDM strategy [2], and implement functional dependency extraction to enhance the effectiveness of variable elimination.

译文：此外，我们增强了多臂强盗(MAB)奖励方案将去年获奖者KISSAT-MAB实施到MDM策略[2]，并实现功能依赖项提取，提高变量消除的有效性。

（3）Finally, we extend our elimination method eager redundancy elimination (ERE) [1], [3] with clause strengthening to remove redundant literals. 最后，我们扩展了我们的消除方法热切冗余消除(ERE)[1]，[3]与子句加强去除冗余字面量。

VARIABLE ELIMINATION

4. SLIME SAT Solver

1st Oscar Riveros
Santiago, Chile
oscar.riveros@gmail.com

（1）给出了一个结论：The DISTANCE heuristic is now parametric, on the experiments, DISTANCE work well with cryptographic instances, but not with generics.

（2）提出了HESS black-box algorithm算法--决策变元相位选择的一种策略：

5. new solvers Cadical ESA and Kissat MAB ESA

Cadical ESA

Kissat MAB ESA

分别从 Cadical and Kissat MAB进行的修改。

在变元消除方面进行了改进

variable elimination is essential for modern SAT solvers.

In MiniSat [1] and its derived solvers, variable elimination is used in preprocessing（预处理）, and in Kissat [2] and other Kissat-based solvers, it is used in inprocessing（制程巡检）.