-
Notifications
You must be signed in to change notification settings - Fork 6
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
How to extract Herbrand functions? #18
Comments
That’s not possible in the current version of caqe |
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:
***@***.***>
|
Basically you need to use tools like QBFcert to extract such functions. The easiest way is to use DQBDD solver Finally, I will leave you with a link to our paper for using such certificates for QBF validation |
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?
The text was updated successfully, but these errors were encountered: