Optimizations on the Stalmarck Procedure

Mar 1, 2024·
Liam Davis
Liam Davis
· 1 min read
Abstract
The Stålmarck procedure is a method for checking tautologies in propositional logic, known for its industrial applications in hardware verification. Despite its theoretical importance, the practical implementation of the algorithm presents significant optimization challenges. This paper explores enhancements to the Stålmarck procedure by integrating modern SAT solving techniques.
Type

We make optimizations in the form of clause learning and directional heuristics on the Stålmarck procedure for boolean satisfiability. This research explores how modern SAT solving techniques can enhance the classical Stålmarck algorithm, making it more practical for industry applications.