Semantics for "(set-info :status sat/unsat")

18 views
Skip to first unread message

Mikoláš Janota

unread,
Mar 27, 2024, 2:53:26 PM3/27/24
to SMT-LIB
Hi 

Is there a differentiation between a problem being SAT and UNSAT because there is a solver that has solved the problem and between the author of the problem believing it has a particular status?

Both the author and the solver can be wrong but we would hope that the chances of the solver being wrong are lower :) Hence the difference.

Cheers
-Mikolas

Clark Barrett

unread,
Mar 27, 2024, 11:33:58 PM3/27/24
to smt...@googlegroups.com
We have not made this distinction.  We allow both, but periodically do try to confirm as many as possible by solving with multiple solvers and long time limits.  Thus, it is possible that some difficult problems that no solver can solve might be mislabeled by the author.  So far, this has happened only very rarely.

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/1263dff4-8aff-4ab7-a276-0e1ffb99c372n%40googlegroups.com.
Reply all
Reply to author
Forward
0 new messages