Evaluating logic gate constraints in local search for structured satisfiability problems

摘要

Conjunctive normal forms (CNF) of structured satisfiability problems contain logic gate patterns. So Boolean circuits (BC) by and large can be obtained from them and thus structural information that is lost in the CNF can be recovered. However, it is not known which logic gates are useful for local search on BCs or which logic gates in particular help local search the most and why. In this article, we empirically show that exploitation of xor, xnor, eq, and not gates is a key factor behind the performance of local search algorithms using single variable flips when adapted to logic gate constraints. Moreover, controlled experiments and investigations into the variables selected for flipping further elucidates these findings. To achieve these conclusions, we have adapted the AdaptNovelty+ and CCANr algorithms to cope with logic gate-based constraint models. These are two prominent families of local search algorithms for satisfiability. We performed our experiments using a large set of benchmark instances from SATLib, SAT2014, and SAT2020. We have also presented techniques to eliminate cycles among logic gates that are detected from CNF and to propagate equivalence of variables statically through the logic gate dependency relationships.