Two Optimizations on the St\aa lmarck Procedure

In this paper, we introduce StalmarckSAT, the a modern re-implementation of the St\aa lmarck Procedure for SAT solving, and present two novel strategies to improve the Procedure, Cardinality Driven Branching (CDB) and Deductive Priority Ordering (DPO). CDB is a heuristic to improve branching with the dilemma rule, and DPO intelligently orders simple rules based on their deductive potential. Our results demonstrate improved solve times with both strategies.