2020SAT竞赛综述解读2——文献学习Relaxed Backtracking with Rephasing_求解器Relaxed LCMDCBDL系列

Abstract—A novel relaxing CDCL method and a new probability based phase saving technology are described.

译文：介绍了一种新的弛豫CDCL方法和一种新的基于概率的相位节约技术。

Based on this method, we develop three solvers called Relaxed LCMDCBDL, Relaxed LCMDCBDL noTimeParam and Relaxed LCMDCBDL newTech, which are based on MapleLCMDistChronoBT-DL.

We improve the relaxing CDCL method [3] using the information in CCAnr [2] this year.

By using some full assignments (also named phases) with certain probability before each inprocessing, the performance of solvers on satisfiable instances are improved.

译文：通过在每次处理前使用一定概率的完全赋值(也称为相位)，提高了求解器在可满足实例上的性能。

The idea is to relax the backtracking process for protecting promising partial assignment, where a promising assignment is defined according to its consistency (no conflict) and length.

译文：其思想是放松回溯过程，以保护有希望的部分分配，其中有希望的分配是根据其一致性(无冲突)和长度定义的。

When the CDCL process reaches a node with some conditions, the algorithm enters a non-backtracking phase until it gets a full assignment.

译文：当CDCL进程到达具有某些条件的节点时，算法进入一个非回溯阶段，直到它获得一个完整的赋值.

Then Local search process is then called to seek for a model near.

译文：然后调用局部搜索过程来寻找附近的模型.

If the local search fails to find a model within certain limits, then the algorithm goes back to the normal CDCL search from the node where it was interrupted.

译文：如果本地搜索在一定范围内无法找到模型，那么算法从被中断的节点返回到正常的CDCL搜索.

For a given conjunctive normal formula (CNF) with V variables, |V| denotes the number of variables.

And for a partial assignment α in CDCL process without conflicts, |α| is the number of assigned variables in α, then we name the max number of |α| in CDCL history as max trail.

Here we control the entrance of local search process by p, q and c, where p, q presents |α|/|V | and |α|/max trail.

And c presents the inprocessing times between two local search process.

Phase saving is a well-known technique which saves the
assignment of variables when traceback and uses the assignment
when variables are selected as decision variables. Like
the rephase technique in CaDiCaL [1], we use vectors to save
different phases, the difference is that we use probability to
select which phase to use after each restart. The probability
of each phase is shown in “Table. I”

TABLE I
PROBABILITY OF EACH PHASE

Relaxed LCMDCBD use both methods mentioned above and for the relaxing method, algorithms call local search process when p ≥0.4 or q ≥ 0.9 and c≥400.
MapleLCMDistChronoBT-DL [4] is the base of the other solvers.

We find there is a switch in MapleLCMDistChronoBT-DL
between VSIDS and CHB when the time reach 2500 seconds,
this method will make the results unstable when tested on
different clusters, or even on the same clusters but at different
times. For the stableness, we replace the time based switch
with a restart based switch, i.e., every n inprocessing, the
algorithm will switch the branching algorithm once between
VSIDS and LRB. For our solvers, n = 500.

For better utilize the information in Local Search process,
we use a vector occ_num to record the number of occurrences
of variables in unsat clauses after each flip. And we see one
percent of occurrences as one conflict in CDCL process.

For example, there is a CNF with two clauses
{v1, x2}, {v2, v3}, which show up in the unsat clauses 10
and 20 times respectively. Assume the Local Search process
conducts 100 flips, then occ num[v1] = 10, occ num[v2] =
30, occ num[v3] = 20, and v1, v2, v3 are considered as
encountering 10, 30 and 20 conflicts respectively. When the Local Search process ends, the branching heuristic algorithm will utilize the information.

Relaxed LCMDCBDL newTech adjusts the local search entrance condition to c ≥ 300 in order to adapt the local search information.

[1] A. Biere. Cadical at the sat race 2019. SAT RACE 2019, page 8.

[2] S. Cai, C. Luo, and K. Su. CCAnr: A configuration checking based local search solver for non-random satisfiability. In International Conference on Theory and Applications of Satisfiability Testing, pages 1–8, 2015.

[3] S. Cai and X. Zhang. Four relaxed cdcl solvers. SAT RACE 2019, page 35.

[4] S. Kochemazov, O. Zaikin, V. Kondratiev, and A. Semenov.  Maplelcmdistchronobt-dl, duplicate learnts heuristic-aided solvers at the sat race 2019. SAT RACE 2019, page 24.