danbryce
commented
1 month ago 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
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!!!