Compactly generating all satisfying truth assignments of a Horn formula

TL;DR

This paper introduces an algorithm that efficiently generates all satisfying truth assignments of a Horn formula without enumerating each one individually, and extends the method to generate models of specific weights.

Contribution

It presents a novel exclusion-based algorithm for compactly generating all models of a Horn formula, including models of a given weight, and compares it with existing methods.

Findings

Efficient generation of all models of a Horn formula.

Extension to generate models of specific weight k.

Comparison with constraint programming, integer programming, and decision diagrams.

Abstract

As instance of an overarching principle of exclusion an algorithm is presented that compactly (thus not one by one) generates all models of a Horn formula. The principle of exclusion can be adapted to generate only the models of weight $k$. We compare and contrast it with constraint programming, $0,1$ integer programming, and binary decision diagrams.