Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
https://arxiv.org/abs/1605.00723

{1,…,n}を2つに分割するときに、a²+b²=c²を満たすa,b,cが同じ集合に入らないような分割ができるか?、 という boolean Pythagorean triples 問題をSATで解いたという話。 n=7824まではそういう分割が可能で、n=7825でそういう分割が不可能(UNSAT)になる。 後者のUNSATの証明が200TBほどになるということで、そのような巨大な証明をどう考えるべきかみたいな話もあって、その辺りを膨らませて一般向けに書かれた記事として最近[1]が出ている。

また、そこで使われたUNSATのcertificationに関する技術で、DRATとかあまりちゃんと理解できていなかったのを理解できたのと、あと How Hard, Really, is SAT? [2] を読んで以来ずっと気になっていたCube-and-Conquerが理解できてよかった。

DRATに関しては、融合原理(resolution)による証明だと確かに論理的に含意される制約しか追加していけないけれど、symmetry-breaking や https://plus.google.com/+MasahiroSakai/posts/QqSNefFQc5E のような、論理的には含意されないけれど充足可能性を保存するような制約の追加を許そうと思うと、たしかにこういうのが必要になるし、またそれを現実的にチェックできるようになっていて面白いとと思った。

Cube-and-Conquerについては、要はlook-aheadに基づいて解空間を分割して、それぞれを別のSATソルバインスタンスに解かせるというアプローチ。 cubeはリテラルのconjunctionのこと。 昔SATの並列化について調べた時には、解空間の分割はあまりうまく行っていなくて、どちらかというとソルバをポートフォリオ化して補題を交換する的なアプローチの方が上手くいっていた気がするが、これはlook-aheadに基づく分割戦略やプラクティカルな実装がうまく行っているのかな。

また、余談ながら、形式的証明とどうあるべきかみたいな話については、[3][4][5]や[6]のような話を思い出した。 ちょっと違う話ではあるけれど。

[1] The science of brute force
http://dl.acm.org/citation.cfm?doid=3127343.3107239

[2] How Hard, Really, is SAT?
https://rjlipton.wordpress.com/2016/09/04/how-hard-really-is-sat/
https://plus.google.com/+MasahiroSakai/posts/GC9EsEMXpyb

[3] What is a Formal Proof? | The n-Category Café
https://golem.ph.utexas.edu/category/2016/08/what_is_a_formal_proof.html

[4] What is a formal proof? | Mathematics and Computation
http://math.andrej.com/2016/08/09/what-is-a-formal-proof/
https://plus.google.com/+MasahiroSakai/posts/fFqpsGnJ9Dt

[5] Formal proofs are not just deduction steps | Mathematics and Computation
http://math.andrej.com/2016/08/30/formal-proofs-are-not-just-deduction-steps/

[6] Proving Without Explaining, and Verifying Without Understanding
http://www.scottaaronson.com/blog/?p=1170
http://www.scottaaronson.com/talks/proofs.ppt