Two Optimizations on the St\aa lmarck Procedure

Sergei Leonov, Liam Davis

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.

picture_as_pdf flag

Knowledge Graph

arrow_drop_up

Comments

Sign up or login to leave a comment