Enumerating all solutions of a Boolean CSP by non-decreasing weight
2011 (English)In: Theory and applications of satisfiability testing - SAT 2011: 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings / [ed] Karem A. Sakallah, Laurent Simon, Berlin: Springer, 2011, 120-133 p.Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
Berlin: Springer, 2011. 120-133 p.
Lecture Notes in Computer Science, ISSN 0302-9743 ; 6695 LNCS
complexity, CSP, Enumeration, generalized satisfiability, polynomial delay, Successive outputs, Weight change, Algorithms, Formal logic, Polynomials, Boolean algebra
Computer and Information Science
IdentifiersURN: urn:nbn:se:hj:diva-31623DOI: 10.1007/978-3-642-21581-0_11ScopusID: 2-s2.0-79959409371ISBN: 9783642215803ISBN: 9783642215810OAI: oai:DiVA.org:hj-31623DiVA: diva2:957159
14th International Conference on Theory and Applications of Satisfiability Testing, SAT 2011; Ann Arbor, MI; United States; 19 June 2011 through 22 June 2011; Code 85244