How to extract Herbrand functions?

[chrispvm]

The CAQE paper describes a procedure for extracting Herbrand functions for a QBF problem. How do we get the CAQE solver to give us these Herbrand functions?

[ltentrup]

That’s not possible in the current version of caqe

[chrispvm]

Thank you, To your knowledge, is there currently any QBF solver that can extract Herbrand/Skolem functions?

…

On Thu, Nov 2, 2023 at 3:07 PM Leander Tentrup ***@***.***> wrote: That’s not possible in the current version of caqe — Reply to this email directly, view it on GitHub <#18 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ALMDA4H3UBW7BML3VVYGOYTYCPVQ7AVCNFSM6AAAAAA63LGULWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTOOJRGM4TENZYHA> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[irfansha]

Basically you need to use tools like QBFcert to extract such functions.
You get a trace from solvers like DepQBF, then use such tools to extract the Skolem/Herbrand functions.

The easiest way is to use DQBDD solver
Although it is DQBF solver, you can run your QBF instance and ask for a certificate as an option.
This can be slow compared to DepQBF or CAQE.

Finally, I will leave you with a link to our paper for using such certificates for QBF validation
You can find relevant tools cited in the introduction.
You can also email me if you have more questions.

[alan23273850]

@ltentrup
Cursor told me that the old-style CAQE version 2 can extract Herbrand/Skolem functions. Is there any way to access that source code or executable? Thanks!

[ltentrup]

Unfortunately no, I don't have access to the source code anymore