Talk:Solve a Hidato puzzle: Difference between revisions
→Any good general algorithm?
Line 80:
:: My glpsol version string is <code>GLPSOL: GLPK LP/MIP Solver, v4.45</code>, which might be why it doesn't have <code>--minisat</code>. Examples were run without it, not sure if that switch was crucial or not. --[[User:Ledrug|Ledrug]] 19:53, 4 May 2012 (UTC)
:::The no feasible solution error implies that the data file you created contained an error, as there is a feasible solution to a correct data file. The --minisat is needed to avoid the numerical instability with a correct data file.--[[User:Nigel Galloway|Nigel Galloway]] 13:26, 5 May 2012 (UTC)
:::For an explanation of minisat you may wish to see http://en.wikipedia.org/wiki/Tseitin-Transformation briefly summized
::::The Tseitin Transformation is used to produce a boolean equation in conjunctive normal form (CNF) from a combinatorial logic circuit so that it may be solved by a SAT solver. The naive approach is to write the circuit as an equation, and use De Morgan's law and distribution. However, this can result in an exponential increase in equation size. The Tseitin Transformation outputs an equation whose size has grown linearly relative to the input circuit's.
:::Exponential increase is bad when you increase the problems size, so we avoid it --[[User:Nigel Galloway|Nigel Galloway]] 13:47, 5 May 2012 (UTC)
:::I have added an example in Ruby which shows that no time problem exists if the path length between hints is reasonable. The new C version could check the length of the path it is looking for and not adopt the new strategy if it is reasonably short, hence not slowing down normal puzzles.--[[User:Nigel Galloway|Nigel Galloway]] 13:26, 5 May 2012 (UTC)
:::The following graph shows an example where if the path 1 2 5 6 etc is chosen, everything thinks it has reasonable connectivity, but they are kidding themselves. Graphs like this have efficient general solutions, they occur for instance in garbage collectors and glpk.--[[User:Nigel Galloway|Nigel Galloway]] 13:26, 5 May 2012 (UTC)
| |||