Evasiveness Through Binary Decision Diagrams

In this paper, we explore whether a data structure for representing Boolean functions (namely, Binary Decision Diagrams) can be useful to detect, in an efficient way, the acyclicity of simplicial complexes. This is approached by means of the concept of evasiveness, allowing us to study the relation with Alexander duality. Furthermore, as main result, we prove that the (depth) complexity of a kind of acyclic simplicial complexes (dismantlable complexes) can be determined by means of Reduced Ordered Binary Decision Diagrams. As the subject has shown itself error prone, we have carried out the proof by using the Isabelle proof assistant, providing a rewarding combination of informal and formal mathematics.