Формал логикадағы Horn қанағаттандырылатындығы мәселесі
Horn-satisfiability
Формалды логикадағы HORNSAT мәселесі – Horn қалауларының қанағаттандырылуын анықтау. P-толық проблемасы, Alfred Horn атымен аталған, полиномдық уақытта шешіледі.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Формальды логикада Хорн қанағаттандырылатындығы немесе HORNSAT – берілген ұсыныс Хорн клаузалары жиыны қанағаттандырыла ма, қанағаттандырылмай ма екенін анықтау мәселесі. Хорн қанағаттандырылатындығы және Хорн клаузалары Альфред Хорнның есімімен аталады. Хорн клаузасы – клаузаның басында бір оң литерал, ал клаузаның денесін құрайтын кез келген санға теріс литералдар бар клауза. Хорн формуласы – Хорн клаузаларының конъюнкциясы арқылы құрылған ұсыныс формуласы. Хорн қанағаттандырылатындығы – бұл полиномиалдық уақытта есептелетіні белгілі, "қиын" немесе "көрнекті" проблемалардың бірі, яғни P-толық проблема. Хорн қанағаттандырылатындығы мәселесі көпмәнді логикалар үшін де қойылуы мүмкін. Алгоритмдер көбінесе сызықтық емес, бірақ кейбіреулері полиномиалды; толық шолу үшін Hähnle (2001 немесе 2003) еңбегіне қараңыз.
In formal logic, Horn satisfiability, or HORNSAT, is the problem of deciding whether a given set of propositional Horn clauses is satisfiable or not. Horn satisfiability and Horn clauses are named after Alfred Horn. A Horn clause is a clause with at most one positive literal, called the head of the clause, and any number of negative literals, forming the body of the clause. A Horn formula is a propositional formula formed by conjunction of Horn clauses. Horn satisfiability is actually one of the "hardest" or "most expressive" problems which is known to be computable in polynomial time, in the sense that it is a P complete problem. The Horn satisfiability problem can also be asked for propositional many valued logics. The algorithms are not usually linear, but some are polynomial; see Hähnle (2001 or 2003) for a survey.
Жалпылау
Хорн формулалары классының кеңейтілген түрі – қайта аттауға болатын Хорн формулалары, яғни кейбір айнымалыларын тиісті инверсияларымен алмастыру арқылы Хорн түріне келтірілетін формулалар жиыны. Мұндай алмастырудың болуын сызықтық уақытта тексеруге болады; демек, мұндай формулалардың қанағаттандырылуы P класына жатады, себебі оларды алдымен осы алмастыруды жасап, содан кейін нәтижедегі Хорн формуласының қанағаттандырылуын тексеру арқылы шешуге болады. Хорн формулаларының қанағаттандырылуы және қайта аттауға болатын Хорн формулаларының қанағаттандырылуы – полиномиалдық уақытта шешілетін қанағаттандырылудың екі маңызды кіші классының бірі; екінші кіші класс – 2 қанағаттандырылуы.
A generalization of the class of Horn formulae is that of renamable Horn formulae, which is the set of formulae that can be placed in Horn form by replacing some variables with their respective negation. Checking the existence of such a replacement can be done in linear time; therefore, the satisfiability of such formulae is in P as it can be solved by first performing this replacement and then checking the satisfiability of the resulting Horn formula. Horn satisfiability and renamable Horn satisfiability provide one of two important subclasses of satisfiability that are solvable in polynomial time; the other such subclass is 2 satisfiability.
Екі мүйізді SAT
Horn SAT-тың екі нұсқасы – Dual Horn SAT, онда әрбір клаузада ең көп дегенде бір теріс литерал болады. Барлық айнымалыларды жоққа шығару Dual Horn SAT мысалын Horn SAT-қа түрлендіреді. Хорн 1951 жылы Dual Horn SAT-тың P класында екенін дәлелдеді.
A dual variant of Horn SAT is Dual Horn SAT, in which each clause has at most one negative literal. Negating all variables transforms an instance of Dual Horn SAT into Horn SAT. It was proven in 1951 by Horn that Dual Horn SAT is in P.