Seguem algumas reflexões sobre "Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer", cujo resumo diz que: "…Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proofs of SAT solvers, we produced and verified a proof in the DRAT format, which is almost 200 terabytes in size. From this we extracted and made available a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the DRAT proof for checking." (Incluindo comentários especiais sobre a variante do método de resolução denominada "Deletion Resolution Asymmetric Tautology".)
"A new longest computer proof makes us wonder about things from security to the Exponential Time Hypothesis" https://rjlipton.wordpress.com/2016/09/04/how-hard-really-is-sat/ JM -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para postar neste grupo, envie um e-mail para [email protected]. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_Lim9TrqpvVoM14VGszbtX_UUN-JOZO1GPZZadXebXjQLg%40mail.gmail.com.
