Abstract
Branching (case analysis) on variables is a profoundly entrenched technique in automated reasoning, being a basis for SAT solvers, resolution and the Shannon/Boole expansion. This is to be contrasted with branching on formulas where one performs case analysis on the truth of a formula instead of the state of a variable. In this talk, I will discuss the limitations of branching on variables using tools from the field of knowledge compilation (which aims to compile formulas into tractable circuit representations), showing how branching on formulas can be exponentially more efficient. I will portray this separation from several theoretical and practical angles, and then provide an outlook on how branching on formulas can be exploited further, practically and more broadly.