Proof checker?

[DustinWehr]

I used dReal for a computer-assisted proof of a surprisingly hard recreational geometry problem, first posed over 50 years ago. If you're curious, all the relevant details are in the abstract and introduction of this writeup.

Last time I tried dReal4 in 2022, output of unsat witnesses wasn't implemented yet, so I used dReal3 to generate them after verifying unsat with dReal4.

Q1: Has there been any work on dReal4 certificates since then?
Q2: Is there any (perhaps nasty and unpublished) code for translating the dReal3 certificates to an easier-to-parse and check form?

Ideally I would generate proofs in a proof assistant from them, but I'd also be happy just putting the certificates in a form that a short script I write can parse and check with arbitrary precision arithmetic. My instances are large sets of quadratic constraints over 10 real variables. No special functions used.

Thanks for any help you can offer!!!

[danbryce]

I have a fork at: https://github.com/danbryce/dreal4 that will generate unsat cores. I changed the build flags for picosat to generate unsat cores, which was disabled in the main dreal4 repository. I also added a dreal flag -c to generate the core. If there is an unsat core, then it is output to a file core.dimacs (by picosat IIRC, in the DIMACS format) and to a file unsat.core in an infix CNF formula over both the theory literals and the Tseitin literals. I also added it to the Python API.

My fork needs to merge some of the updates from the main repository, but I think this feature is relatively isolated from my other changes.

[DustinWehr]

That sounds promising! I guess I will have to wait for the build to be fixed before trying it. Unless you have a ubuntu 22.04 compatible binary of your fork?

[DustinWehr]

Or a binary of your fork that I can run on any system? I'm confused about how the CI pipeline could be broken for 5 months unless the repo is just abandoned. @soonhokong are you looking for a new maintainer?

[danbryce]

I have a Docker build that first builds ibex and then dreal. It is based on Ubuntu 20.04. The build is somewhat bespoke for another project depending on dreal, but the relevant dreal part starts with this target: https://github.com/siftech/funman/blob/71d6de14f55763fe60f9bd159459a1e5bd44b433/Makefile#L35 I am not sure how much work is needed to update the ubuntu version of the base image. My recollection is that ibex is the hard part to build.

…

On Aug 6, 2024, at 10:08 AM, Dustin Wehr ***@***.***> wrote: Or a binary of your fork that I can run on any system? I'm confused about how the CI pipeline could be broken for 5 months unless the repo is just abandoned. @soonhokong are you looking for a new maintainer? Is AWS crushing your soul? — Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you commented.Message ID: ***@***.***>

[DustinWehr]

Thank you I will try it!

…

On Tue, Aug 6, 2024, 11:57 AM Daniel Bryce ***@***.***> wrote: I have a Docker build that first builds ibex and then dreal. It is based on Ubuntu 20.04. The build is somewhat bespoke for another project depending on dreal, but the relevant dreal part starts with this target: https://github.com/siftech/funman/blob/71d6de14f55763fe60f9bd159459a1e5bd44b433/Makefile#L35 I am not sure how much work is needed to update the ubuntu version of the base image. My recollection is that ibex is the hard part to build. > On Aug 6, 2024, at 10:08 AM, Dustin Wehr ***@***.***> wrote: > > > Or a binary of your fork that I can run on any system? I'm confused about how the CI pipeline could be broken for 5 months unless the repo is just abandoned. @soonhokong are you looking for a new maintainer? Is AWS crushing your soul? > — > Reply to this email directly, view it on GitHub, or unsubscribe. > You are receiving this because you commented.Message ID: ***@***.***> — Reply to this email directly, view it on GitHub <#316 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAMML3VS23DMC6UHQDI3NALZQDW73AVCNFSM6AAAAABMAWTBKSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDENZRGYZDQOJXHE> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[DustinWehr]

@danbryce do the dreal4 unsat witnesses still cite (sometimes) reduced-precision versions of the constraints given in the smt2 instance?