경음기 만족도

형식논리학에서는, Horn 만족도, 즉 HORNAST는 주어진 명제 Horn 조항의 세트가 만족스러운지 아닌지를 결정하는 문제다.혼 만족도와 혼 절은 알프레드 혼의 이름을 따서 명명되었다.

기본 정의 및 용어

혼 절은 절의 본문을 구성하는, 절의 머리라고 불리는, 최대 하나의 양의 리터럴을 가진 절이며, 임의의 수의 음의 리터럴을 가진 절이다.혼 공식은 혼 절의 결합에 의해 형성된 명제 공식이다.

Horn 만족도 문제는 선형적으로 해결할 수 있다.^[1]정량화된 혼 공식의 진리를 결정하는 문제는 다항식 시간에도 풀 수 있다.^[2]경음기 만족도에 대한 다항식 시간 알고리즘은 단위 전파 규칙에 기초한다: 공식에 단일 리터럴 l ${\displaystyle$ l $}($ 단위 절 자체를 제외한) $l$ 로 구성된 절이 포함된 경우 $l$ $l$ 을 포함하는 모든 절이 제거되고 $\neg l$ $\neg l$ ${\displays$ }을 포함하는 모든 절이 제거된다. $tyle \neg$ l $}$ 은(는) 이 문자 그대로를 제거했다 $\neg l$ .두 번째 규칙의 결과 자체는 같은 방식으로 전파되는 단위 조항이 될 수 있다.단위 절이 없는 경우 나머지 변수를 모두 음수로 설정하기만 하면 공식을 만족시킬 수 있다.이 변환으로 $l$ $l$ 과 $l$ $\neg l$ $\neg l$ $\neg l$ 의 반대 단위 절이 생성된다면 이 공식은 만족스럽지 못하다 $\neg l$ 경적 만족도는 사실상 다항식 시간에서 계산이 가능한 것으로 알려진 "가장 어려운" 또는 "가장 표현적인" 문제들 중 하나이다.^[3]

또한 이 알고리즘은 만족스러운 Horn 공식의 진실 할당을 결정할 수 있다: 단위 절에 포함된 모든 변수는 해당 단위 절을 만족하는 값으로 설정된다. 다른 모든 리터럴은 거짓으로 설정된다.결과 할당량은 Horn 공식의 최소 모델, 즉 true에 할당된 최소 변수 집합을 가진 할당이며, 여기서 설정된 격납을 사용하여 비교한다.

단위 전파를 위한 선형 알고리즘을 사용하여 알고리즘은 공식의 크기로 선형이다.

뿔풍뎅이 등급의 일반화는 개명식-호른풍뎅이로, 일부 변수를 각각의 부정으로 대체하여 뿔풍뎅이 형태로 배치할 수 있는 공식 집합이다.이러한 대체물의 존재 여부는 선형적인 시간에 확인할 수 있으므로, 이러한 공식의 만족도는 P에 있다. 이는 이 대체물을 먼저 수행한 다음 Horn 공식의 만족도를 확인하는 것으로 해결할 수 있기 때문이다.^[4]^[5]^[6]^[7]경음기 만족도와 명칭이 변경 가능한 경음기 만족도는 다항식 시간에 해결 가능한 두 가지 중요한 만족도 하위 클래스 중 하나를 제공한다. 다른 하위 클래스는 2-만족도다.

Horn 만족도 문제는 또한 제안할 만한 많은 가치의 로직들을 요구할 수 있다.알고리즘은 일반적으로 선형적이지 않지만 일부 다항식이다. 조사는 Hahnle(2001년 또는 2003년)을 참조한다.^[8]^[9]

듀얼 혼 SAT

Horn SAT의 이중 변형은 Dual-Horn SAT이며, 각 절에는 최대 하나의 음의 리터럴이 있다.모든 변수를 부정하면 Dual-Horn SAT의 인스턴스가 Horn SAT로 변환된다.1951년 혼에 의해 듀얼 혼 SAT가 P에 있다는 것이 증명되었다.

참고 항목

참조

^ Dowling, William F.; Gallier, Jean H. (1984), "Linear-time algorithms for testing the satisfiability of propositional Horn formulae", Journal of Logic Programming, 1 (3): 267–284, doi:10.1016/0743-1066(84)90014-1, MR 0770156
^ Buning, H.K.; Karpinski, Marek; Flogel, A. (1995). "Resolution for Quantified Boolean Formulas". Information and Computation. Elsevier. 117 (1): 12–18. doi:10.1006/inco.1995.1025.
^ Stephen Cook; Phuong Nguyen (2010). Logical foundations of proof complexity. Cambridge University Press. p. 224. ISBN 978-0-521-51729-4.
^ Lewis, Harry R. (1978). "Renaming a set of clauses as a Horn set". Journal of the ACM. 25 (1): 134–135. doi:10.1145/322047.322059. MR 0468315..
^ Aspvall, Bengt (1980). "Recognizing disguised NR(1) instances of the satisfiability problem". Journal of Algorithms. 1 (1): 97–103. doi:10.1016/0196-6774(80)90007-3. MR 0578079.
^ Hébrard, Jean-Jacques (1994). "A linear algorithm for renaming a set of clauses as a Horn set". Theoretical Computer Science. 124 (2): 343–350. doi:10.1016/0304-3975(94)90015-9. MR 1260003..
^ Chandru, Vijaya; Collette R. Coullard; Peter L. Hammer; Miguel Montañez; Xiaorong Sun (2005). "On renamable Horn and generalized Horn functions". Annals of Mathematics and Artificial Intelligence. 1 (1–4): 33–47. doi:10.1007/BF01531069.
^ Reiner Hähnle (2001). "Advanced many-valued logics". In Dov M. Gabbay, Franz Günthner (ed.). Handbook of philosophical logic. Vol. 2 (2nd ed.). Springer. p. 373. ISBN 978-0-7923-7126-7.
^ Reiner Hähnle (2003). "Complexity of Many-valued Logics". In Melvin Fitting, Ewa Orłowska (ed.). Beyond two: theory and applications of multiple-valued logic. Springer. ISBN 978-3-7908-1541-2.

추가 읽기

Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx; Spencer, Joel; Vardi, Moshe Y.; Venema, Yde; Weinstein, Scott (2007). Finite model theory and its applications. Texts in Theoretical Computer Science. An EATCS Series. Berlin: Springer-Verlag. ISBN 978-3-540-00428-8. Zbl 1133.03001.

[1] Dowling, William F.; Gallier, Jean H. (1984), "Linear-time algorithms for testing the satisfiability of propositional Horn formulae", Journal of Logic Programming, 1 (3): 267–284, doi:10.1016/0743-1066(84)90014-1, MR 0770156

[buningkarpinski-2] Buning, H.K.; Karpinski, Marek; Flogel, A. (1995). "Resolution for Quantified Boolean Formulas". Information and Computation. Elsevier. 117 (1): 12–18. doi:10.1006/inco.1995.1025.

[CookNguyen2010-3] Stephen Cook; Phuong Nguyen (2010). Logical foundations of proof complexity. Cambridge University Press. p. 224. ISBN 978-0-521-51729-4.

[4] Lewis, Harry R. (1978). "Renaming a set of clauses as a Horn set". Journal of the ACM. 25 (1): 134–135. doi:10.1145/322047.322059. MR 0468315..

[5] Aspvall, Bengt (1980). "Recognizing disguised NR(1) instances of the satisfiability problem". Journal of Algorithms. 1 (1): 97–103. doi:10.1016/0196-6774(80)90007-3. MR 0578079.

[6] Hébrard, Jean-Jacques (1994). "A linear algorithm for renaming a set of clauses as a Horn set". Theoretical Computer Science. 124 (2): 343–350. doi:10.1016/0304-3975(94)90015-9. MR 1260003..

[7] Chandru, Vijaya; Collette R. Coullard; Peter L. Hammer; Miguel Montañez; Xiaorong Sun (2005). "On renamable Horn and generalized Horn functions". Annals of Mathematics and Artificial Intelligence. 1 (1–4): 33–47. doi:10.1007/BF01531069.

[8] Reiner Hähnle (2001). "Advanced many-valued logics". In Dov M. Gabbay, Franz Günthner (ed.). Handbook of philosophical logic. Vol. 2 (2nd ed.). Springer. p. 373. ISBN 978-0-7923-7126-7.

[FittingOrlowska2003-9] Reiner Hähnle (2003). "Complexity of Many-valued Logics". In Melvin Fitting, Ewa Orłowska (ed.). Beyond two: theory and applications of multiple-valued logic. Springer. ISBN 978-3-7908-1541-2.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

Search

경음기 만족도

네임스페이스

더

목차

기본 정의 및 용어

듀얼 혼 SAT

참고 항목

참조

추가 읽기