Dichotomy theorem for the generalized unique satisfiability problem
Identifieur interne :
000D82 ( PascalFrancis/Curation );
précédent :
000D81;
suivant :
000D83
Dichotomy theorem for the generalized unique satisfiability problem
Auteurs : L. Juban [
France]
Source :
-
Lecture notes in computer science [ 0302-9743 ] ; 1999.
RBID : Pascal:99-0527417
Descripteurs français
English descriptors
Abstract
The unique satisfiability problem, that asks whether there exists a unique solution to a given propositional formula, was extensively studied in the recent years. This paper presents a dichotomy theorem for the unique satisfiability problem, partitioning the instances of the problem between the polynomial-time solvable and coNP-hard cases. We notice that the additional knowledge of a model makes this problem coNP-complete. We compare the polynomial cases of unique satisfiability to the polynomial cases of the usual satisfiability problem and show that they are incomparable. This difference between the polynomial cases is partially due to the necessity to apply parsimonious reductions among the unique satisfiability problems to preserve the number of solutions. In particular, we notice that the unique not-all-equal satisfiability problem, where we ask whether there is a unique model such that each clause has at least one true literal and one false literal, is solvable in polynomial time.
pA |
A01 | 01 | 1 | | @0 0302-9743 |
---|
A05 | | | | @2 1684 |
---|
A08 | 01 | 1 | ENG | @1 Dichotomy theorem for the generalized unique satisfiability problem |
---|
A09 | 01 | 1 | ENG | @1 FCT '99 : fundamentals of computation theory : Iasi, 30 August - 3 september 1999 |
---|
A11 | 01 | 1 | | @1 JUBAN (L.) |
---|
A12 | 01 | 1 | | @1 CIOBANU (Gabriel) @9 ed. |
---|
A12 | 02 | 1 | | @1 PAUN (Gheorghe) @9 ed. |
---|
A14 | 01 | | | @1 LORIA (Université Henri Poincaré Nancy 1), BP 239 @2 54506 Vandœuvre-lès-Nancy @3 FRA @Z 1 aut. |
---|
A20 | | | | @1 327-337 |
---|
A21 | | | | @1 1999 |
---|
A23 | 01 | | | @0 ENG |
---|
A26 | 01 | | | @0 3-540-66412-2 |
---|
A43 | 01 | | | @1 INIST @2 16343 @5 354000084584580270 |
---|
A44 | | | | @0 0000 @1 © 1999 INIST-CNRS. All rights reserved. |
---|
A45 | | | | @0 13 ref. |
---|
A47 | 01 | 1 | | @0 99-0527417 |
---|
A60 | | | | @1 P @2 C |
---|
A61 | | | | @0 A |
---|
A64 | 01 | 1 | | @0 Lecture notes in computer science |
---|
A66 | 01 | | | @0 DEU |
---|
C01 | 01 | | ENG | @0 The unique satisfiability problem, that asks whether there exists a unique solution to a given propositional formula, was extensively studied in the recent years. This paper presents a dichotomy theorem for the unique satisfiability problem, partitioning the instances of the problem between the polynomial-time solvable and coNP-hard cases. We notice that the additional knowledge of a model makes this problem coNP-complete. We compare the polynomial cases of unique satisfiability to the polynomial cases of the usual satisfiability problem and show that they are incomparable. This difference between the polynomial cases is partially due to the necessity to apply parsimonious reductions among the unique satisfiability problems to preserve the number of solutions. In particular, we notice that the unique not-all-equal satisfiability problem, where we ask whether there is a unique model such that each clause has at least one true literal and one false literal, is solvable in polynomial time. |
---|
C02 | 01 | X | | @0 001D02A07 |
---|
C03 | 01 | X | FRE | @0 Dichotomie @5 01 |
---|
C03 | 01 | X | ENG | @0 Dichotomy @5 01 |
---|
C03 | 01 | X | SPA | @0 Dicotomía @5 01 |
---|
C03 | 02 | X | FRE | @0 Temps polynomial @5 02 |
---|
C03 | 02 | X | ENG | @0 Polynomial time @5 02 |
---|
C03 | 02 | X | SPA | @0 Tiempo polinomial @5 02 |
---|
C03 | 03 | X | FRE | @0 Problème NP complet @5 03 |
---|
C03 | 03 | X | ENG | @0 NP complete problem @5 03 |
---|
C03 | 03 | X | SPA | @0 Problema NP completo @5 03 |
---|
C03 | 04 | X | FRE | @0 Unicité solution @5 04 |
---|
C03 | 04 | X | ENG | @0 Solution uniqueness @5 04 |
---|
C03 | 04 | X | SPA | @0 Unicidad solución @5 04 |
---|
C03 | 05 | X | FRE | @0 Problème NP difficile @5 05 |
---|
C03 | 05 | X | ENG | @0 NP hard problem @5 05 |
---|
C03 | 05 | X | SPA | @0 Problema NP duro @5 05 |
---|
C03 | 06 | X | FRE | @0 Etude comparative @5 06 |
---|
C03 | 06 | X | ENG | @0 Comparative study @5 06 |
---|
C03 | 06 | X | SPA | @0 Estudio comparativo @5 06 |
---|
C03 | 07 | X | FRE | @0 Logique propositionnelle @5 07 |
---|
C03 | 07 | X | ENG | @0 Propositional logic @5 07 |
---|
C03 | 07 | X | SPA | @0 Lógica proposicional @5 07 |
---|
C03 | 08 | X | FRE | @0 Résolution problème @5 08 |
---|
C03 | 08 | X | ENG | @0 Problem solving @5 08 |
---|
C03 | 08 | X | SPA | @0 Resolución problema @5 08 |
---|
C03 | 09 | X | FRE | @0 Problème satisfiabilité unique @4 INC @5 72 |
---|
C03 | 10 | X | FRE | @0 Satisfiabilité @4 CD @5 96 |
---|
C03 | 10 | X | ENG | @0 Satisfiability @4 CD @5 96 |
---|
N21 | | | | @1 340 |
---|
|
pR |
A30 | 01 | 1 | ENG | @1 Fundamentals of computation theory. International symposium @2 12 @3 Iasi ROM @4 1999-08-30 |
---|
|
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000A88
Links to Exploration step
Pascal:99-0527417
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Dichotomy theorem for the generalized unique satisfiability problem</title>
<author><name sortKey="Juban, L" sort="Juban, L" uniqKey="Juban L" first="L." last="Juban">L. Juban</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA (Université Henri Poincaré Nancy 1), BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>France</country>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">99-0527417</idno>
<date when="1999">1999</date>
<idno type="stanalyst">PASCAL 99-0527417 INIST</idno>
<idno type="RBID">Pascal:99-0527417</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000A88</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000D82</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Dichotomy theorem for the generalized unique satisfiability problem</title>
<author><name sortKey="Juban, L" sort="Juban, L" uniqKey="Juban L" first="L." last="Juban">L. Juban</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA (Université Henri Poincaré Nancy 1), BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>France</country>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="1999">1999</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Comparative study</term>
<term>Dichotomy</term>
<term>NP complete problem</term>
<term>NP hard problem</term>
<term>Polynomial time</term>
<term>Problem solving</term>
<term>Propositional logic</term>
<term>Satisfiability</term>
<term>Solution uniqueness</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Dichotomie</term>
<term>Temps polynomial</term>
<term>Problème NP complet</term>
<term>Unicité solution</term>
<term>Problème NP difficile</term>
<term>Etude comparative</term>
<term>Logique propositionnelle</term>
<term>Résolution problème</term>
<term>Problème satisfiabilité unique</term>
<term>Satisfiabilité</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">The unique satisfiability problem, that asks whether there exists a unique solution to a given propositional formula, was extensively studied in the recent years. This paper presents a dichotomy theorem for the unique satisfiability problem, partitioning the instances of the problem between the polynomial-time solvable and coNP-hard cases. We notice that the additional knowledge of a model makes this problem coNP-complete. We compare the polynomial cases of unique satisfiability to the polynomial cases of the usual satisfiability problem and show that they are incomparable. This difference between the polynomial cases is partially due to the necessity to apply parsimonious reductions among the unique satisfiability problems to preserve the number of solutions. In particular, we notice that the unique not-all-equal satisfiability problem, where we ask whether there is a unique model such that each clause has at least one true literal and one false literal, is solvable in polynomial time.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01>
<fA05><s2>1684</s2>
</fA05>
<fA08 i1="01" i2="1" l="ENG"><s1>Dichotomy theorem for the generalized unique satisfiability problem</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG"><s1>FCT '99 : fundamentals of computation theory : Iasi, 30 August - 3 september 1999</s1>
</fA09>
<fA11 i1="01" i2="1"><s1>JUBAN (L.)</s1>
</fA11>
<fA12 i1="01" i2="1"><s1>CIOBANU (Gabriel)</s1>
<s9>ed.</s9>
</fA12>
<fA12 i1="02" i2="1"><s1>PAUN (Gheorghe)</s1>
<s9>ed.</s9>
</fA12>
<fA14 i1="01"><s1>LORIA (Université Henri Poincaré Nancy 1), BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA14>
<fA20><s1>327-337</s1>
</fA20>
<fA21><s1>1999</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA26 i1="01"><s0>3-540-66412-2</s0>
</fA26>
<fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000084584580270</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 1999 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>13 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>99-0527417</s0>
</fA47>
<fA60><s1>P</s1>
<s2>C</s2>
</fA60>
<fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0>
</fA64>
<fA66 i1="01"><s0>DEU</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>The unique satisfiability problem, that asks whether there exists a unique solution to a given propositional formula, was extensively studied in the recent years. This paper presents a dichotomy theorem for the unique satisfiability problem, partitioning the instances of the problem between the polynomial-time solvable and coNP-hard cases. We notice that the additional knowledge of a model makes this problem coNP-complete. We compare the polynomial cases of unique satisfiability to the polynomial cases of the usual satisfiability problem and show that they are incomparable. This difference between the polynomial cases is partially due to the necessity to apply parsimonious reductions among the unique satisfiability problems to preserve the number of solutions. In particular, we notice that the unique not-all-equal satisfiability problem, where we ask whether there is a unique model such that each clause has at least one true literal and one false literal, is solvable in polynomial time.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D02A07</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Dichotomie</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Dichotomy</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Dicotomía</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Temps polynomial</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Polynomial time</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Tiempo polinomial</s0>
<s5>02</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Problème NP complet</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>NP complete problem</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Problema NP completo</s0>
<s5>03</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Unicité solution</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Solution uniqueness</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Unicidad solución</s0>
<s5>04</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Problème NP difficile</s0>
<s5>05</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>NP hard problem</s0>
<s5>05</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Problema NP duro</s0>
<s5>05</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Etude comparative</s0>
<s5>06</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Comparative study</s0>
<s5>06</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA"><s0>Estudio comparativo</s0>
<s5>06</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Logique propositionnelle</s0>
<s5>07</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG"><s0>Propositional logic</s0>
<s5>07</s5>
</fC03>
<fC03 i1="07" i2="X" l="SPA"><s0>Lógica proposicional</s0>
<s5>07</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Résolution problème</s0>
<s5>08</s5>
</fC03>
<fC03 i1="08" i2="X" l="ENG"><s0>Problem solving</s0>
<s5>08</s5>
</fC03>
<fC03 i1="08" i2="X" l="SPA"><s0>Resolución problema</s0>
<s5>08</s5>
</fC03>
<fC03 i1="09" i2="X" l="FRE"><s0>Problème satisfiabilité unique</s0>
<s4>INC</s4>
<s5>72</s5>
</fC03>
<fC03 i1="10" i2="X" l="FRE"><s0>Satisfiabilité</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="10" i2="X" l="ENG"><s0>Satisfiability</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fN21><s1>340</s1>
</fN21>
</pA>
<pR><fA30 i1="01" i2="1" l="ENG"><s1>Fundamentals of computation theory. International symposium</s1>
<s2>12</s2>
<s3>Iasi ROM</s3>
<s4>1999-08-30</s4>
</fA30>
</pR>
</standard>
</inist>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000D82 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Curation/biblio.hfd -nk 000D82 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Curation
|type= RBID
|clé= Pascal:99-0527417
|texte= Dichotomy theorem for the generalized unique satisfiability problem
}}
| This area was generated with Dilib version V0.6.33. Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022 | |