How Hard, Really, is SAT?

20 views

Skip to first unread message

Joao Marcos

unread,

Sep 7, 2016, 8:36:13 PM9/7/16

to Lista acadêmica brasileira dos profissionais e estudantes da área de LOGICA

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

Francisco Antonio Doria

unread,

Sep 8, 2016, 6:48:54 AM9/8/16

to logi...@dimap.ufrn.br

Se vc considera as linguagens Sat, existe um algoritmo trivial que resolve Sat em tempo polinomial. As linguagens Sat são genéricas na medida para esse algoritmo.

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 logica-l+unsubscribe@dimap.ufrn.br.
Para postar neste grupo, envie um e-mail para logi...@dimap.ufrn.br.
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.