On Enumerating Short Projected Models

Sibylle Möhle, Roberto Sebastiani, Armin Biere

Propositional model enumeration, or All-SAT, is the task to record all models of a propositional formula. It is a key task in software and hardware verification, system engineering…