This Core First Unit Propagation.

Posted 2021-03-02 yuweng1689

This is a new heuristic which is called Core First Unit Propagation in MapleLCMdistCBTcoreFirst  sat solver .

 CFUP ( Core First Unit Propagation) heuristic is proposed by Jingchao Chen 在2019年SAT竞赛上。

The basic idea of CFUP ( Core First Unit Propagation) is to prefer core clauses over non-core ones during unit propagation. This can be done by moving core clauses ahead of non-core clauses.

 译文：核心优先单位传播(Core First Unit Propagation)的基本思想是在单位传播中优先使用核心子句，而不是非核心子句。这可以通过将核心子句移到非核心子句之前来实现。

实现步骤：

（1）

The pseudo-code of CFUP shown in Algorithm 2 assumes that a full literal watch scheme (a full occurrence list of all clauses) is used, If using a two literal watch scheme [7], The statement “Append W[l] − C to the end of C ” in Algorithm 2 can be replaced with the code of Algorithm 1.

 

 

（2）

A general CDCL solver has two watchlists: binary and non binary. We adopt the core priority strategy only on a non-binary watchlist. By our empirical observation, adopting always the core priority strategy is not good choice. A better policy is that when the number of conflicts is less than 2×10 6 , CFUP is called, Otherwise, BCP is called. The high-level algorithm CDCL combining CFUP and BCP are shown in Algorithm 3. 

 

 

译文：

一个通用的CDCL解决方案有两个观察列表:二进制的和非二进制的。我们只在非二进制观察列表中蚕蛹优先策略。

求解过程从始至终总是采用核心优先战略不是一个好的选择。设置冲突数界限值θ（依据经验设置 θ=2×10 6）。冲突次数小于2×10 6的阶段阶段采用CFUP,之后还采用原来默认的BCP方法。