Frontier-aware variable ordering for OBDD compilation from feature interaction graphs

Ordered binary decision diagrams (OBDDs) provide canonical Boolean representations whose size depends strongly on variable order. For conjunctive normal form (CNF) compilation, prefix-frontier width connects a linear order to the established pathwidth-based size bound. We develop frontier refinement on feature interaction graphs (FIGs): a bounded-insertion search that lexicographically improves the frontier profile and guarantees a maximum frontier no larger than that of its min-fill seed. On 120 independently sampled benchmark graphs with 10–20 variables, refinement reduces the mean gap to exact pathwidth from 6.69 to 0.38 and attains the optimum on 79 instances; on a 20-variable disjoint-edge formula, it reduces internal nodes from 2,046 to 20. Evaluations on tree-derived encodings and SATLIB quantify frontier certificates, diagram sizes, and computational cost, establishing frontier refinement as a structural ordering method for certificate-oriented compilation.