search

tcvdijk / story-bc

Optimal block crossings in Storyline Visualisation: efficient fixed parameter tractable algorithm and SAT-solved based solution.
0 stars 1 forks source link

UNSAT on the examples #1

Open yuya737 opened 2 months ago

yuya737 commented 2 months ago

I've obtained and built minisat from https://github.com/agurfinkel/minisat (I don't spot any breaking changes, and the original repo didn't compile on my machine).

However running python main.py examples/{inception,star_wars,the_matrix}.pcsv, I yield a UNSAT from minisat.

Can you confirm which exact variant of minisat for which I can run this code?

tcvdijk commented 2 months ago

Hi, thank you for your interest in our code. I don't necessarily recommend running executables from strangers on the internet, but the download at the following address has the exact windows executable that we used. That page also deeplinks the minisat code we based it on (and our patch). These links still work for me.

https://www1.pub.informatik.uni-wuerzburg.de/pub/data/storylines/

Hope this helps!

Regards, tvd

yuya737 commented 2 months ago

I really appreciate your response! Thanks for that link as well.

Wanted to confirm that the output from solver.py that writes into the tmp/miniSATInput.sat is in standard DIMACS format. I mention this because I've put the same file through some online SAT solvers and they report that it's not satisfiable. Would it be possible for you to share the DIMACS CNF formulation for, say, examples/inception.pcsv?

I must be missing something - thanks again