Abstract

Many heuristics, such as decision, restart, and clause reduction heuristics, are incorporated in CDCL solvers in order to improve performance. In this paper, we focus on learnt clause reduction heuristics, which are used to suppress memory consumption and sustain propagation speed. The reduction heuristics consist of evaluation criteria, for measuring the usefulness of learnt clauses, and a reduction strategy in order to select clauses to be removed based on the criteria. LBD (literals blocks distance) is used as the evaluation criteria in many solvers. For the reduction strategy, we propose a new concise schema based on the coverage ratio of used LBDs. The experimental results show that the proposed strategy can achieve higher coverage than the conventional strategy and improve the performance for both SAT and UNSAT instances.

归约试探法由评估标准和归约策略组成，评估标准用于衡量学习到的子句的有用性，归约策略用于根据标准选择要删除的子句。

注意：heuristics涵盖几个部分，其中包括strategy。

对于归约策略，我们提出了一个新的基于已用lbd覆盖率的简洁模式。

1 Introduction

In this paper, we propose a new reduction strategy based on the coverage of used LBDs, which dynamically computes an appropriate LBD threshold in order to cover most propagations and conflicts.

在本文中，我们提出了一种新的基于已用LBD覆盖的约简策略，该策略动态地计算适当的LBD阈值以覆盖大多数传播和冲突。实验结果表明，我们的模式有效地维护了已使用的子句，并在SAT和UNSAT实例上实现了性能提升。

The rest of this paper is organized as follows: Sect. 2 reviews clause reduction heuristics used in CDCL solvers. In Sects. 3 and 4, we provide experimental results, in order to clarify the property of LBD, and to point out some issues in the LBD-based reduction strategy, respectively. Our proposed reduction strategy is described in Sect. 5. Section 6 shows the experimental results and Sect. 7 concludes this paper.

2 Clause Reduction Heuristics