化简子句集入门——预处理和求解中某些特定时间节点用到的技术环节

A. Clause Database Simplification

The clause database simplification technique is a technique that is effective but does not have to exist in the mainstream solver. It can improve the speed of unit propagation by deleting clauses that have already been satisfied and judging whether clauses have errors.

After a period of search in bfSAT, the simplification of the clause database will begin. When simplification, the solver should be in the decision layer. It will traverse all the clauses and learning clauses, and delete the dummy variables. Delete the clauses that have been returned, and delete the watches of the literals corresponding to the variables in the zero layer, and correspondingly clear some of the deleted clauses left in the watches. It will improve the efficiency of the solution to some extent and save the memory overhead. But determining the point in time to optimize the technique is a problem that needs to be judged by a large number of experiments.