Implementing Modal Tableaux Using Sentential Decision Diagrams

A Sentential Decision Diagram (SDD) is a novel representation of a boolean function which contains a Binary Decision Diagram (BDD) as a subclass. Previous research suggests that BDDs are effective in implementing tableaux-based automated theorem provers. We investigate whether SDDs can offer improved efficiency when used in the same capacity. Preliminarily, we found that SDDs compile faster than BDDs only on large CNF formulae. In general, we found the BDD-based modal theorem prover still outperforms our SDD-based modal theorem prover. However, the SDD-based approach excels over the BDD-based approach in a select subset of benchmarks that have large sizes and modalities that are less nested or fewer in number.