coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Does someone have the SAT code from Stéphane Lescuyer?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Does someone have the SAT code from Stéphane Lescuyer?
Date: Thu, 10 May 2018 12:20:48 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga18.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.200.100
Ironport-phdr: 9a23:ZGYidxC2CJCMAP6+aJLuUyQJP3N1i/DPJgcQr6AfoPdwSPT9o8bcNUDSrc9gkEXOFd2Cra4c0KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUijexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzLisJ+j6xboQ6uqBNkzoHOfI2YMOBzcr/Bcd8HQ2dKQ8ZfVzZGAoO5d4YDAfcPPeFGoInyu1sOtxy+BRG0COjyzTFIh2P53a0g3Os/FQHK0hErEtULsHTVsNr1NL0dXv6xzKXS1jXDaO1Z2Tjh6IjSdRAhueqBXbN2ccrN10YvExnJgUmXqYzgJj6Y0PkGvWac7+plT+2vimgnphlwojip2scjlI3JipgIxV/a7Sl5xJw1JdyiRE51e96pFoZbuSKCN4ZuX88vTW5ltDwnxrAItpO3ZjUGxZomyhLFdvCLbYmF7gr+WOuQLzp0nnxodbylixqs/0WtzvfwWtS33VpXtiZJj9jBu3QX2xDN6sWKReFx8lm71TqR2A3e7udJKl0um6XBMZ4u2Lswm4ITsUvdGi/2n137jKqZdko+5+Sl6P7rYrTgpp+AKYB0jhvyPbgpmsy6Geg4Mw4OUHaH+emkybHu80L0TK9XgvA4naTVqo3WKMoaq6KjHgNZzIcu5w66Dzi80dQYmXcHLEhCeBKCl4XpPlDOL+z4DfilnVuslC1nx+vBPrL/DZXNMmLDkLD5fbtm6k5czhYzws5b555OFr4BJ/fzVlfrtNPEFh85LxC0w+H/Bdph0YMeQHuDDbOdMKPPqlCF/fkvIumJZI8NojnxMfkl5/j0jX84g1ARZ6ep3YFEIEy/S75tJFzcan7xiP8AF30Lt0wwVqai3FaFSHtYY2u4d6M6/DAyToy8W9TtXIeo1fa62yq0AodRfiQOL1GHEX7lc8/MD/INYyKbL8sniTsJWqS7TJcJ1BeyuQu8wL1ieLmHshYEvI7ugYAmr9bYkgs/oGQtXpatllqVRmQxpVsmAjo/3aRxu0t4kw7R0K5kjvgeHttWtaoQDlUKcKXExuk/MOjcHxrbd47QGlegXtiiRzo2S4BpmoJcUwNGA9ynyyv78W+qDrsSzuPZAZM9q/Ka3n7tKsI7wHHDhvEs

Dear Coq Users,

I wanted to have a look at the various approaches which have been tried so far to embed SAT in Coq. Unfortunately the Coq code from Stéphane Lescuyer et al mentioned in the papers “Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme” and “A Reflexive Formalization of a SAT Solver in Coq” which should be at:

http://www.lri.fr/~lescuyer/sat/unsat.tgz

seems to have been deleted and also waybackmachine doesn’t help. If you happen to have a copy of the file, I would appreciate it, if you could send it to me.

Thanks & best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Does someone have the SAT code from Stéphane Lescuyer?, Soegtrop, Michael, 05/10/2018
- Re: [Coq-Club] Does someone have the SAT code from Stéphane Lescuyer?, Matthieu Sozeau, 05/10/2018