Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Бульдік функциялардың стандартты түрі
Standard form of Boolean function
Бульдік логикада формула, егер ол бір немесе бірнеше клаузалардың конъюнкциясы болса, конъюнктивті қалыпты формада (КҚФ) немесе клаузалық қалыпты формада болады, мұнда клауза – литеральдардың дизъюнкциясы; яғни, бұл сомалардың көбейтіндісі немесе ОР-лардың АНД-ы. Канондық қалыпты форма ретінде, ол автоматтандырылған теореманы дәлелдеуде және схемалар теориясында пайдалы. Автоматтандырылған теореманы дәлелдеуде "клаузалық қалыпты форма" түсінігі көбінесе тар мағынада қолданылады, яғни КҚФ формуласының литеральдар жиындары түріндегі нақты бір бейнесін білдіреді.
In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a canonical normal form, it is useful in automated theorem proving and circuit theory. In automated theorem proving, the notion "clausal normal form" is often used in a narrower sense, meaning a particular representation of a CNF formula as a set of sets of literals.
ҚНҚ-ға айналдыру
Классикалық логикада кез келген логикалық формуланы эквивалентті CNF (конъюнктивтік нормалды форма) түріндегі формулаға түрлендіруге болады. Бұл түрлендіру логикалық эквиваленттіліктердің ережелеріне негізделген: қос жосық жою, Де Морган заңдары және тарату заңы.
In classical logic each propositional formula can be converted to an equivalent formula that is in CNF. This transformation is based on rules about logical equivalences: double negation elimination, De Morgan's laws, and the distributive law.
Есептеу күрделілігі
Есептеу күрделілігі мәселелерінің маңызды жиынтығы, конъюнктивті қалыпты түрінде (CNF) берілген буль формуласының айнымалыларына, формуланың шындыққа сай болатындай мәндерді тағайындауды қамтиды. k SAT мәселесі – CNF түрінде берілген буль формуласына қанағаттандыратын мәндерді табу мәселесі, мұнда әрбір дизъюнкцияда ең көп дегенде k айнымалы болады. 3 SAT NP-толық (k>2 кез келген басқа k SAT мәселесі сияқты), ал 2 SAT-тың полиномиалдық уақытта шешімі бар екені белгілі. Осының салдарынан, формуланы DNF-ке түрлендіру, қанағаттандырылуын сақтап, NP-қиын міндет болып табылады; сондай-ақ, CNF-ке түрлендіру, жарамдылығын сақтап, NP-қиын; демек, эквиваленттілікті сақтап DNF немесе CNF-ке түрлендіру де NP-қиын. Бұл жағдайдағы типовой мәселелер "3CNF" формулаларына қатысты: конъюнктивті қалыпты формада, әрбір конъюнкцияда үштен артық айнымалы болмайды. Мұндай формулалардың практикада кездесетін мысалдары өте үлкен болуы мүмкін, мысалы, 100 000 айнымалы және 1 000 000 конъюнкция. CNF формуласын "kCNF" (k≥3) эквисатисфакциялық формуласына түрлендіруге болады, о үшін k-дан артық айнымалы бар әрбір конъюнкцияны екі конъюнкциямен және Z жаңа айнымалысымен ауыстырып, қажет болған жағдайда осы әрекетті қайталап отыру керек.
An important set of problems in computational complexity involves finding assignments to the variables of a boolean formula expressed in conjunctive normal form, such that the formula is true. The k SAT problem is the problem of finding a satisfying assignment to a boolean formula expressed in CNF in which each disjunction contains at most k variables. 3 SAT is NP complete (like any other k SAT problem with k>2) while 2 SAT is known to have solutions in polynomial time. As a consequence, the task of converting a formula into a DNF, preserving satisfiability, is NP hard; dually, converting into CNF, preserving validity, is also NP hard; hence equivalence preserving conversion into DNF or CNF is again NP hard. Typical problems in this case involve formulas in "3CNF": conjunctive normal form with no more than three variables per conjunct. Examples of such formulas encountered in practice can be very large, for example with 100,000 variables and 1,000,000 conjuncts. A formula in CNF can be converted into an equisatisfiable formula in "kCNF" (for k≥3) by replacing each conjunct with more than k variables by two conjuncts and with Z a new variable, and repeating as often as necessary.