Exploiting Dynamically Propositional Logic Structures in SAT

TL;DR

This paper introduces a dynamic structure extraction method for SAT solvers that effectively solves complex equivalence checking problems like hwb-n32, which have remained unsolvable for decades.

Contribution

It presents a novel dynamic extraction technique of propositional logic structures to enhance SAT solver capabilities for difficult problems.

Findings

Successfully solved the hwb-n32 problem within 3000 seconds

Enhanced SAT solving by extracting and utilizing dynamic propositional structures

Demonstrated the effectiveness of the method on longstanding unsolved problems

Abstract

The 32-bit hwb (hwb-n32 for short) problem is from equivalence checking that arises in combining two circuits computing the hidden weighted bit function. Since 2002, it remains still unsolvable in every SAT competition. This paper focuses on solving problems such as hwb-n32. Generally speaking, modern solvers can detect only XOR, AND, OR and ITE gates. Other non-clausal formulas (propositional logic structures) cannot be detected. To solve the hwb-n32 problem, we extract dynamically some special propositional logic structures, and then use a variant of DPLL-based solvers to solve the subproblem simplified by the extracted structure information. Using the dynamic extraction technique, we solved efficiently the hwb-n32 problem, even some of which were solved within 3000 seconds.