Support for answer tuples
logicReasoner opened this issue · 4 comments
Hello,
I noticed that there is a very old branch with support for answer tuples ( https://github.com/sneeuwballen/zipperposition/tree/answer-tuples )
@c-cube , are there any plans to make that functionality work with the current state of Zipperposition?
An example problem to test against:
https://www.tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=PUZ&File=PUZ081^3.p
Currently the prover correctly returns SZS status Theorem but how could I extract any valid answers?
Thanks!
hi, I don't think there's any particular plan to reimplement/adapt this. I don't remember if it worked well back then, there's a few subtleties around weight/precedence of the fake answer literal in clauses.
I see. What do you mean with subtleties?
If I give it a shot to try to adapt the old changes from the old answer-tuples branch into master, is there a high chance that it would work? I can't program in OCaml BTW but have some programming experience :)
If memory serves, the way this is implemented is by creating a symbol $answer(X,Y,Z) when the question ?[X,Y,Z]: foo is asked, and solving the CNF of foo(X,Y,Z) => $answer(X,Y,Z), but where a clause only containing $answer(a,b,c) is considered as actually empty (and you just read the arguments to find the answer X := a, Y := b, Z := c). The problem with that is that it impacts all the heuristics about unit clauses (clauses with 1 literal), literal counts, size of clauses, weight of clauses, etc. unless you make really sure that $answer(…) is invisible to all of these.
You can give it a shot, but there's been quite a lot of changes since then so it might be a significant amount of work :/
That sounds like a daunting task. Perhaps, I'll give it a shot next time when I have a weekend to spare.
Thanks for the info 👍