Notes on "Bounds on BDD-Based Bucket Elimination”
share
This paper concerns Boolean satisfiability (SAT) solvers based on Ordered Binary Decision Diagrams (BDDs), especially those that can generate proofs of unsatisfiability. Mengel (arXiv:2306.00886) has presented a theoretical analysis that a BDD-based SAT solver can generate a proof of unsatisfiability for the pigeonhole problem (PHP_n) in polynomial time, even when the problem is encoded in the standard “direct” form. His approach is based on bucket elimination, using different orderings for the variables in the BDDs than in the buckets. We show experimentally that these proofs scale as O(n^5). We also confirm the exponential scaling that occurs when the same variable ordering is used for the BDDs as for the buckets.
READ FULL TEXT