pysat
pysat copied to clipboard
Skipping variable indices heavily impacts performance
I iteratively added clauses to an initially empty formula to be sat-solved with glucose3. For convenience, I translated between my 2D problem and the variable indices by multiplying the first coordinate with a large number, then adding the second one. It seems to be the case that the performance becomes (much!) worse the larger this number becomes. Maybe add an internal conversion so that no variables are skipped?
Sure, PRs are more than welcome! :)