Arotau

HBR chapter

Worked until midnight on this, then again from 7am. Almost everything is done, though I have decided to rerun some experiments before finishing the chapter off. I also have some irritating formatting issues to sort out, and BiBTeX is seriously misbehaving on two (correct) citations. Still to go:

• Check my de Kleer ATMS citation, and make sure I’ve got it right.
• Check definition of hyper-resolution.
• Figure out what HBR does on the support encoding.
• Make the figures not all appear on separate float pages at the end of the chapter.
• Do a table to summarise HBR preproc performance on all the DIMACS classes tested, in response to irritating reviewer comments on this not applying to other problem classes.
• Do a table to summarise the number of implied clause conflicts out of the total conflicts.