SAT solver gives different result with the same input #4196
Unanswered
brucefeng10
asked this question in
CP-SAT questions
Replies: 2 comments 2 replies
-
So I agree the solver is non deterministic. |
Beta Was this translation helpful? Give feedback.
1 reply
-
by default, in parallel, cp-sat is non deterministic.
If you use runtime, the amount of work you can do depends on the load of
the machine.
no other termination parameters in parallel.
Laurent Perron | Operations Research | ***@***.*** | (33) 1 42 68 53
00
Le mar. 23 avr. 2024 à 09:25, Bruce Feng ***@***.***> a
écrit :
… It's non deterministic, i've just tried v9.9.
1. "with time limit, you can never be truly be deterministic", do you
mean the model has not converged to a stabe status? If i set the time limit
longer, the nondeterminacy should relieve?
2. Are there any running termination parameters other than time limit?
—
Reply to this email directly, view it on GitHub
<#4196 (reply in thread)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/ACUPL3K5VFSSHPQKO3RGAITY6YEGFAVCNFSM6AAAAABGUI2CJCVHI2DSMVQWIX3LMV43SRDJONRXK43TNFXW4Q3PNVWWK3TUHM4TCOJXGQZTO>
.
You are receiving this because you commented.Message ID:
***@***.***>
|
Beta Was this translation helpful? Give feedback.
1 reply
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
What version of OR-Tools and what language are you using?
Version: v8.2
Language: Java
Which solver are you using
CP-SAT
What operating system (Linux, Windows, ...) and version?
macOS 13.5.1
What did you do?
I'm solving a complex pure Integer Problem, and i use CP-SAT solver, which performs much much better than SCIP. Since it's hard to solve the model to optimal, I set the solving time to 3 minutes. Part of my codes:
What did you see instead?
However, everytime i run the problem with the same input, the result is different. I mean the objective value is different, sometimes it varies much.
Anything else we should know about your project / environment
I also tried to change the solver to "SCIP", the 3min result is always the same, though the result is much worse than "CP-SAT".
The model file is attached.
file.txt
Beta Was this translation helpful? Give feedback.
All reactions