C coder needed
$30-5000 USD
Paid on delivery
minisat (attached) is a very powerful open source software used to solve pseudo-boolean problems (see the attached examples)
However while working with it I found a bug.
I could isolate 1 very long inequality that makes minisat hang.
The line is attached (see file [url removed, login to view]).
Even if the inequality can be easily solved by setting all variables to 0, minisat starts and gets no solution after many minutes.
You can try it by writing
minisat [url removed, login to view]
The problem seems to be with the line size: If I cut the line in half, the problem is solved in a flash (as expected, as the problem is trivial).
Unfortunately I cannot cut the current problem in half :)
I need to write lines as huge as the current one.
Can you fix the problem ?
I suggest you trace the code by using the BIG line split in half and see how a solution is reached.
Than you trace the code by using the full BIG line and see where it hangs.
Please be sure to sign with your name and date the lines you change.
Project ID: #2880991