Using Disjunctive Diagrams for Preprocessing of Conjunctive Normal Forms.

In this article, in the context of the Boolean satisfiability problem (SAT), the question of speeding up the SAT solvers on specific input formulas is considered. The speedup is achieved using the CNF preprocessing algorithm which is based on the use of decision diagrams of a special kind, called Disjunctive Diagrams. These diagrams allow one to naturally test some sets of partial variable assignments and add more stringent constraints to the original formula. Several families of SAT instances are considered and used to compare the solving time before and after preprocessing, including a selection of tests from the "SAT Competition 2021" and some tests related to the problem of checking the equivalence of Boolean circuits.Computational experiments have shown that for hard instances in more than half of the cases the proposed preprocessing algorithm can speed up the solving time of considered CNFs.