$\begingroup$
I found the Satisfiable assignment to one of the UNSAT [SATLIB benchmark][1] instance, specifically uuf50-01.cnf as below answer:
[1, 2, 3, 4, -5, -6, -7, -8, 9, 10, -11, 12, 13, 14, -15, -16, 17, 18, 19, 20, 21, 22, 23, 24, -25, 26, 27, 28, 29, -30, 31, 32, 33, -34, 35, -36, -37, 38, 39, 40, 41, 42, 43, 44, -45, -46, -47, -48, -49, -50]
No matter how hard I try I can't find a clause that is unsatisfiable with above answer. Am I wrong somewhere :) How can I report this if I am right?
Even on cryptosat minisat in your browser tool, it shows as UNSAT only.
TIA
$\endgroup$
I found the Satisfiable assignment to one of the UNSAT [SATLIB benchmark][1] instance, specifically uuf50-01.cnf as below answer:
[1, 2, 3, 4, -5, -6, -7, -8, 9, 10, -11, 12, 13, 14, -15, -16, 17, 18, 19, 20, 21, 22, 23, 24, -25, 26, 27, 28, 29, -30, 31, 32, 33, -34, 35, -36, -37, 38, 39, 40, 41, 42, 43, 44, -45, -46, -47, -48, -49, -50]
No matter how hard I try I can't find a clause that is unsatisfiable with above answer. Am I wrong somewhere :) How can I report this if I am right?
Even on cryptosat minisat in your browser tool, it shows as UNSAT only.
TIA
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
1
This clause is unsatisfied by the assignment in the question: -24 8 -27
-
3$\begingroup$ actually, even the very first clause in the benchmark "-3 36 7" is not satisfied by your assignment. Anyway, your question is off topic here. Better contact the maintainer of SATLIB next time (after a thorough check of course). $\endgroup$– holfNov 29, 2022 at 18:54