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*1 kaj ne(*x*2) estas literaloj, la unua *pozitiva* literalo kaj la dua *negativa* literalo. Se ni AŬ-as kune grupon de literaloj, ni ricevas *propozicion*, kiel (*x*1 *aŭ* ne(*x*2)). 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*11 AŬ *x*12 AŬ *x*13) KAJ
:(*x*21 AŬ *x*22 AŬ *x*23) KAJ
:(*x*31 AŬ *x*32 AŬ *x*33) 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 
* http://www.satlive.org/index.jsp 
* Fortigitaj plenumeblaj SAT etalonoj 
* http://www.satisfiability.org
* Ĵurnalo pri SAT, bulea modelado kaj kalkulado 
* Formalaj kontrolaj SAT etalonoj de IBM 
* Katastra disvastigo 

## Referencoj 
* A9.1: LO1–LO7, pp.259–260.

Kategorio:Komputiko
Kategorio:Matematika logiko