Bulea plenumebloproblemo

Kontentigeblo estas la problemo decidi ĉu la variabloj de donita bulea formulo povas esti asignitaj vervaloroj (VERO aŭ FALSO) tiamaniere, ke la tuta formulo valoriĝas VERA. Egale gravas decidi, ke tia asignado ne ekzistas, implicante ke la funkcio esprimata de la formulo estas FALSA por ĉiaj asignadoj variablaj. En la lasta kazo oni diras, ke la funkcio estas nekontentigebla; alie ĝi estas kontentigebla. Por emfazi la duuma naturo de tiu problemo oni nomas ĝin kiel bulea aŭ propozicia kontentigeblo. Subkomprenate estas ke la funkcio kaj ĉiuj ties variabloj estas duum-valoraj.

Bazaj difinoj, terminologio, kaj apliko

La bulea plenumebloproblemo estas decida problemo konsiderata en komplikteorio. Apero de la problemo estas bulea esprimo skribita uzanta nur operaciojn KAJ, AŬ, NE, variablojn kaj krampojn. La demando estas: donita la esprimo, ĉu estas iu asigno de la valoroj VERO kaj FALSO al la variabloj, kiu farus la tutan esprimon vera?

En matematiko, formulo de propona logiko estas dirita esti kontentigebla, se vero-valoroj povas esti asignitaj al ĝia variabloj tiel, ke la formulo iĝas vera. La klaso de kontentigeblaj propoziciaj formuloj estas NP-kompleta. La propozicia kontentigeblo-problemo, kiu decidas, ĉu donita propozicia formulo estas kontentiga, estas de centra graveco en diversaj areoj de komputiko, inkluzivantaj teorian komputikon, algoritmetikon, artefarita intelekto, aparatara dizajno kaj priprograma pruv(ad)o.

La problemo povas esti grave limigita dum ankoraŭ cetera NP-kompleteco. Per apliko de Demorganaj leĝoj, ni povas alpreni ke NE-operatoroj estas nur aplikitaj rekte al variabloj, ne esprimoj; ni nomas ĉu variablon aŭ ĝian negon literalo. Ekzemple, kaj x₁ kaj ne(x₂) estas literaloj, la unua pozitiva literalo kaj la dua negativa literalo. Se ni AŬ-as kune grupon de literaloj, ni ricevas propozicion, kiel (x₁ aŭ ne(x₂)). Fine, ni konsideru formulojn, kiuj estas konjunkcio (KAJ) de subpropozicioj. Ni nomu ĉi tiun formon norma formo kaja. Difinado, ĉu formulo en ĉi tiu formo estas kontentiga estas ankoraŭ NP-plena, eĉ se ĉiu propozicio estas limigita al maksimume tri literaloj. Ĉi tiu lasta problemo estas nomita 3CNFSAT, 3SAT, aŭ 3-kontentigeblo.

Aliflanke, se ni limigas ĉiun propozicion al maksimume du literaloj, la rezulta problemo, 2SAT, estas en P. La samo validas, se ĉiu propozicio estas Horn-a propozicio; tio estas, ĝi enhavas maksimume unu pozitivan literalon.

Alte teknika pruvo, ke Bulea plenumebloproblemo estas NP-kompleta estas havebla.

Komplikeco kaj limigoj de SAT

NP-Kompeteco

SAT estas NP-plena. Fakte, ĝi estis la unue sciata NP-kompleteca problemo, kiel pruvita far Stephen Cook en 1971 (vidu teoremo de Cook por la pruvo). Ĝis tiu tempo, estis ne sciate, ke, problemoj de NP-pleneco eĉ ekzistis. La problemo restas NP-kompleta eĉ se ĉiuj esprimoj estas skribitaj en norma formo kaja kun 3 variabloj por propozicio (3-CNF), liveranta la problemon 3SAT. Ĉi tio signifas, ke la esprimo havas la formon:

(x₁₁ AŬ x₁₂ AŬ x₁₃) KAJ

(x₂₁ AŬ x₂₂ AŬ x₂₃) KAJ

(x₃₁ AŬ x₃₂ AŬ x₃₃) KAJ ...

kie ĉiu x estas variablo aŭ nego de variablo, kaj ĉiu variablo povas aperi multajn fojojn en la esprimo.

Utila propraĵo de la malpligrandiĝo de Cook estas, ke ĝi konservas la kvanton de akceptantaj respondoj. Ekzemple, se grafeo havas 17 validajn 3-kolorigadoj, la formulo SAT produktita de la malpligrandiĝo havos 17 kontentigantajn asignojn.

2-kontenigebleco

SAT estas pli simpla se la formuloj estas limigitaj al tiuj en norma formo aŭa, tio estas, ili estas aŭo (AŬ) de termoj, kie ĉiu termo estas kajo (KAJ) de literaloj (eble neigitaj variabloj). Tia formulo estas ja kontentigebla se kaj nur se iu el ĝiaj termoj estas kontentiga, kaj termo estas kontentiga se kaj nur se ĝi ne enhavas kaj x kaj NE x por iu variablo x. Ĉi tio povas esti kontrolata en polinoma tempo.

SAT estas ankaŭ pli simpla, se la kvanto de literaloj en propozicio estas limigita al 2, en kiu okazo la problemo estas nomata kiel 2SAT. Ankaŭ ĉi tiu problemo povas esti solvata en polinoma tempo, kaj fakte estas kompleta por la klaso NL. Simile, se ni limigas la kvanton de literaloj por propozicio al 2 kaj ŝanĝas la KAJ operaciojn al ekskluzivAŬ operacioj, la rezulto estas ekskluzivAŬe 2-kontentigebla, problemo kompleta por SL = L klaso.

Unu el la plej gravaj limigoj de SAT estas HORNSAT, kie la formulo estas aŭo de Korno-propozicioj. Ĉi tiu problemo estas solvata per la polinomo-tempa algoritmo de Horno-kontentigeblo, kaj estas fakte P-plena. Ĝi povas vidiĝi kiel versio (de P) de la bulea plenumebloproblemo.

Se la komplikecaj klasoj P kaj NP estas ne egalaj, neniu el ĉi tiuj limigoj estas NP-plena, malverŝajne SAT. La premiso, ke P kaj NP estas ne egalaj, estas ne nun pruvita.

Eksteraj ligiloj

• http://www.satlib.org Arkivigite je 2021-02-11 per la retarkivo Wayback Machine
• http://www.satlive.org/index.jsp Arkivigite je 2006-05-30 per la retarkivo Wayback Machine
• Fortigitaj plenumeblaj SAT etalonoj Arkivigite je 2021-01-25 per la retarkivo Wayback Machine
• http://www.satisfiability.org
• Ĵurnalo pri SAT, bulea modelado kaj kalkulado Arkivigite je 2006-02-19 per la retarkivo Wayback Machine
• Formalaj kontrolaj SAT etalonoj de IBM Arkivigite je 2007-07-17 per la retarkivo Wayback Machine
• Katastra disvastigo Arkivigite je 2006-02-10 per la retarkivo Wayback Machine

Referencoj

• A9.1: LO1–LO7, pp.259–260.