Arotau

Today's work

• Neighbour resolution (NR) and binary equivalence finding experiments have both finished.
• The NR experiments all seem to fit in with previous results, but I now have enough info to make the requisite graphs and tables to support my argument.
• The binary equivalence finding experiments were a bit more interesting: I expected it to mostly be useless, but on a couple of problem classes it was very effective. I now need to look at the encodings and see whether any general conclusion about the encoding can be drawn.
• Met with Alan: reviewed work since Friday; decided to add a section on heuristic & inference interaction in the introduction; set this coming Friday as the deadline for the neighbour resolution chapter, and the AT-HBR experiments; and Sunday as the deadline for the preproc resolution experiments.
• AT-HBR can infer unit clauses, whereas the strict definition of HBR can’t. Does AT-HBR infer any binary clauses that HBR cannot?