마린 흘레

Marijn Heule
마린 흘레
태어난 (1979-03-12) 1979년 3월 12일 (43세)
네덜란드 옌스부르크
직종.부교수
고용주카네기 멜론 대학교
로 알려져 있다SAT 해결사를 사용하여 수학적 추측을 해결하다

Marienus Johannes Hendrikus Heule(마리에누스 요하네스 헨드리쿠스 휼레, 1979년 3월 12일 ~ [1][2])는 네덜란드의 카네기 멜론 대학교 컴퓨터 과학자입니다.훌레는 부울 피타고라스 3배 문제, 슈어의 정리 5번, 켈러의 7차원 추측 등 수학 문제를 풀기 위한 SAT 풀이를 개발했다.

직업

피타고라스 3중 문제 해결의 시각화

Heule은 2008년 네덜란드 델프트 공과대학에서 박사학위를 받았으며 오스틴 텍사스대학 연구조교수와 카네기 멜론대학 [3][4]컴퓨터과학부 부교수를 역임했습니다.

2016년 5월, 그는 올리버 쿨만, 빅터 W.[5][6] 마렉과 함께 컴퓨터 지원 증명인 SAT 해답을 통해 부울 피타고라스의 3중 문제를 풀었습니다.증명된 정리 서술은

정리 - 집합 {1, . . . , 7824}은 두 부분으로 분할할 수 있으며, {1, . . . . , 7825}[7]에는 불가능한 부분이 없습니다.

최대 7825의 숫자에 대해 2⁄3.63×10의2355 색상 조합을 사용할7825 수 있습니다.이러한 가능한 색칠은 1조 개의 서브 케이스로 분할되어 각각 부울 만족도 솔버로 해결되었습니다.Texas Advanced Computing Center에 있는 Stampede 슈퍼컴퓨터에서 이틀 동안 CPU 연산을 약 4년간 실시하여 200테라바이트의 명제 증명을 생성했으며, 이를 68기가바이트로 [7][clarification needed]압축했습니다.

그 증거를 설명하는 논문은 SAT 2016 [7]컨퍼런스에서 발표되었고, 최고의 논문상을 [7]수상했습니다.1980년대에 Ronald Graham은 문제 해결에 100달러의 상금을 내걸었고, Heule은 [5]이 상금을 받았다.

그는 2017년 슈어 5번, 2020년 [6][8]켈러의 추측 7차원을 푸는 데 SAT 풀이 전산증명 기법을 활용하기도 했다.

2018년 Heule과 Scott Aaronson은 국립과학재단으로부터 SAT 해법을 콜라츠 [8]추측에 적용하기 위한 자금을 받았다.

레퍼런스

  1. ^ "Marijn J.H. Heule" (PDF). Year of birth. Retrieved May 11, 2021.
  2. ^ Heule, Marijn (August 20, 2019). "Marijn J.H. Heule" (PDF). www.cs.cmu.edu. Retrieved June 15, 2021.{{cite web}}: CS1 maint :url-status (링크)
  3. ^ "Marijn J.H. Heule". cs.utexas.edu. Retrieved March 8, 2021.
  4. ^ "Marijn J.H. Heule". cs.cmu.edu. Retrieved March 8, 2021.
  5. ^ a b Lamb, Evelyn (May 26, 2016). "Two-hundred-terabyte maths proof is largest ever". Nature. 534 (7605): 17–18. Bibcode:2016Natur.534...17L. doi:10.1038/nature.2016.19990. PMID 27251254.
  6. ^ a b Hartnett, Kevin. "Computer Scientists Attempt to Corner the Collatz Conjecture". Quanta Magazine. Retrieved March 8, 2021.{{cite web}}: CS1 maint :url-status (링크)
  7. ^ a b c d Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016). "Solving and Verifying the Boolean Pythagorean Triples problem via Cube-and-Conquer". In Creignou, Nadia; Le Berre, Daniel (eds.). Theory and Applications of Satisfiability Testing – SAT 2016: 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings. Lecture Notes in Computer Science. Vol. 9710. pp. 228–245. arXiv:1605.00723. doi:10.1007/978-3-319-40970-2_15.
  8. ^ a b Hartnett, Kevin. "Computer Search Settles 90-Year-Old Math Problem". Quanta Magazine. Retrieved March 8, 2021.{{cite web}}: CS1 maint :url-status (링크)