Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Enumerating all solutions of a Boolean CSP by non-decreasing weight
Laboratoire d'Informatique Fondamentale de Marseille, Aix-Marseille Université, France.
Laboratoire d'Informatique Fondamentale de Marseille, Aix-Marseille Université, France.
Laboratoire d'Informatique Fondamentale de Marseille, Aix-Marseille Université, France.
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, p. 120-133Conference paper, Published paper (Refereed)
Abstract [en]

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. p. 120-133
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 6695 LNCS
Keywords [en]
complexity, CSP, Enumeration, generalized satisfiability, polynomial delay, Successive outputs, Weight change, Algorithms, Formal logic, Polynomials, Boolean algebra
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:hj:diva-31623DOI: 10.1007/978-3-642-21581-0_11Scopus ID: 2-s2.0-79959409371ISBN: 9783642215803 (print)ISBN: 9783642215810 (print)OAI: oai:DiVA.org:hj-31623DiVA, id: diva2:957159
Conference
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
Available from: 2016-09-01 Created: 2016-09-01 Last updated: 2018-01-10Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records BETA

Schmidt, Johannes

Search in DiVA

By author/editor
Schmidt, Johannes
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 21 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf