The ND Procedure

My research involves development of a method to solve propositional reasoning problems. Currently, I am focusing on Crossword Puzzle Construction problems. I am working on the ND procedure, which uses solutions to a related "subproblem" to guide the search for a solution to the main problem.

CPC involves a grid with word slots, and a solution to the problem is an assignment of words to slots such that two slots that intersect have the same letter in the square where they meet. Open CPC is CPC restricted to an n by m rectangular grid. Square Open CPC (where n=m) can be easily decomposed by choosing a square subboard centered on the downward sloping diagonal, and suitably truncating the word set.

SD, the first attempt, first solves the subproblem for all possible solutions, and then iterates through them one by one, asserting each one as unit clauses in the superproblem (after some sort of constant-time transformation to rename atoms), and then solves the resulting clause set.

ND solves the subproblem for all possible solutions, and differs from SD by taking groups of "subsolutions" and asserting them all at once in the superproblem. Because fewer repetitions are necessary, ND has been able to outperform SATO, albeit at a loss of correctness (as explained in the first paper.)

NDS processes subsolutions as they are found, and this method for the most part outperforms ND. At the underconstrained end of the problem spectrum, finding all possible subsolutions is very time consuming, this variation removes that problem. However, ND is able to better coordinate how many subsolutions to use in a block, as it has access to all possible subsolutions. In addition, ND is more efficient at processing subsolutions, as it is possible to sort the subsolutions such that there is a "cohesion" between subsolutions processed in a block, that there are common atoms between the subsolutions processed at a time. This improves processing efficiency, at the cost of having to find a large number of subsolutions.

Currently in testing is a combination of DS and ND, that solves for a large block of subsolutions, sorts the large block, and then processes smaller blocks out of that larger block in order to improve cohesion. By tuning the sizes of the small and large blocks, I hope that a performance gain over ND will result.

    Papers about ND:
  1. The original ND paper, presented at the 2000 First Order Theorem Proving Conference. By James J. Lu, Jeffrey S. Rosenthal, and Andrew Shaffer
  2. Results of experiments on NDS that I did for my CS473 Practicum project.

Note that there is a measurement inaccuracy in the NDS vs. ND experiments, in that I neglected to incorporate into NDS' running time the computation involved in encoding the puzzles. I am not sure about the effect that this will have on the results, although it should be no more than half a second. Since it is a constant factor for a given word set size on average, it should leave the fitted equations intact.

Contact Information:
Andrew Shaffer
aes47 (at) cornell.edu
jepigar (at) sunlink.net