Enumerating all solutions of a Boolean CSP by non-decreasing weight

Abstract

We address the problem of enumerating all models of Boolean formulæ in order of non-decreasing weight in Schaefer's framework. The weight of a model is the number of variables assigned to 1. Tractability in this context amounts to enumerating all models one after the other in sorted order, with polynomial delay between two successive outputs. The question of model-enumeration has already been studied in Schaefer's framework, but without imposing a specific order. The order of non-decreasing weight changes the complexity considerably. We obtain a new dichotomous complexity classification. On the one hand, we develop new polynomial delay algorithms for Horn and 2-XOR-formulæ to enumerate the models by non-decreasing weight. On the other hand, we prove that in all other cases such a polynomial delay algorithm does not exist, unless P=NP. © 2011 Springer-Verlag.