coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Does someone have the SAT code from Stéphane Lescuyer?
Date: Thu, 10 May 2018 18:13:31 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f46.google.com
Ironport-phdr: 9a23:aBukax/I/7xuUP9uRHKM819IXTAuvvDOBiVQ1KB41eMcTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRxDmiCgFNzA3/mLZhNFugq1Hux+uvQBzzpTObY2JKPZzfKXQds4aS2pbWcZRUjRMDISmYIsTE+oBPedYoJfgp1ATsBW+AgitC/31xT9Vm3T72qg63P49EQHaxgMgGskDsHHOo9XpKKcdS+W1wLPPzTXZYPNbwDHw45XGfBAmpPGDR7NwcczJxEkgEAPFiVqQqYj7MD+PyusNtG2b4/JhVeKpl24otQVxriKyycgykoXJgpgVylHe+SV32oY4I8CzRk1jYdO8EpZduDuWO5ZoTs4iWW1luzg2xqcJtJO6eiUB1Y4pyATFa/OddoiF+hLjW/iVITd/nH9lfaiwhxe28US5xOz8U9W43E9EridKk9TArH8N1xvU6siITvty4F2t1iqI1wDW8u1EIEY0mrTHK5M5wLM9mYAfvVndEiL2gkn7j7Gael8r9+Wp8+jnZ6/ppp6YN496kAH+NaEul9S6AesiLggOQ2ib+eWi273+50H5W7JKj/wonabDrZDXPssbpqujDA9U1oYv8QqwDzCj0NgAh3kIMEpFeA6bj4juI1zBPPf4De6mj1uwlDdr2uvJM6b6ApTNK3jDiK3ucax8605a0gozzMpQ64haCrEbc7rPXRr6s8WdBRskOSS1xfzmAZNzzNAwQ2WKV4qQLL/SsFKVrtkoMeSFecdBvT/hN/Egz/vnkWMwnBkaZ6b/jshfU2yxAvkzexbRWnHrmNpUST5b7Dp7d/TjjRi5aRAWYn+zW6wm4TRiUdCpCI7CQsamh7nThX7nTK0TXXhPDxW3KVmtb5+NAq1ebSuOPsZk1DseWur5EtJz5VSVrAb/joFfAK/U9ykf78+x0dF046jMkEl3+2AqScua1G6JQid/mWZaHzI=

Hi,

I think there is a contrib (look for ergo or altergo maybe) which contains it.

Best,
— Matthieu

Le jeu. 10 mai 2018 à 14:21, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

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