{"id":3374,"date":"2013-05-27T05:38:55","date_gmt":"2013-05-27T05:38:55","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3374"},"modified":"2013-05-27T05:38:55","modified_gmt":"2013-05-27T05:38:55","slug":"resena-mechanical-verification-of-sat-refutations-with-extended-resolution","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-mechanical-verification-of-sat-refutations-with-extended-resolution\/","title":{"rendered":"Rese\u00f1a: Mechanical verification of SAT refutations with extended resolution"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de verificaci\u00f3n formal en <a href=\"http:\/\/www.cs.utexas.edu\/~moore\/acl2\/\">ACL2<\/a> titulado <a href=\"http:\/\/www.cs.utexas.edu\/~nwetzler\/itp13\/itp13.pdf\">Mechanical verification of SAT refutations with extended resolution<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/www.cs.utexas.edu\/~nwetzler\">Nathan Wetzler<\/a>, <a href=\"http:\/\/www.cs.utexas.edu\/~marijn\/\">Marijn J. H. Heule<\/a> y <a href=\"http:\/\/www.cs.utexas.edu\/~hunt\/\">Warren A. Hunt Jr.<\/a><\/p>\n<p>El trabajo se presentar\u00e1 en julio en el <a href=\"http:\/\/itp2013.inria.fr\/\">ITP 2013<\/a> (<i>4th Conference on<br \/>\nInteractive Theorem Proving<\/i>).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nWe present a mechanically-verified proof checker developed with the ACL2 theorem-proving system that is general enough to support the growing variety of increasingly complex satisfiability (SAT) solver techniques, including those based on extended resolution. A common approach to assure the correctness of SAT solvers is to emit a proof of unsatisfiability when no solution is reported to exist. Contemporary proof checkers only check logical equivalence using resolution-style inference. However, some state-of-the-art, conflict-driven, clause-learning SAT solvers use preprocessing, inprocessing, and learning techniques, that cannot be checked solely by resolution-style inference. We have developed a mechanically-verified proof checker that assures refutation clauses preserve satisfiability. We believe our approach is sufficiently expressive to validate all known SAT-solver techniques.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de verificaci\u00f3n formal en ACL2 titulado Mechanical verification of SAT refutations with extended resolution. Sus autores son Nathan Wetzler, Marijn J. H. Heule y Warren A. Hunt Jr. El trabajo se presentar\u00e1 en julio en el ITP 2013 (4th Conference on Interactive Theorem Proving). Su resumen es We present a&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[49,285,110],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3374"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=3374"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3374\/revisions"}],"predecessor-version":[{"id":3375,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3374\/revisions\/3375"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3374"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3374"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3374"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}