Arotau

Back in action

Over the last couple of evenings I’ve finally managed to get back to work on my thesis again. If everything goes well, I should complete the second-to-last remaining technical chapter by the end of next week.

Chapter finished

Finished another thesis chapter today. Only a couple more of the technical chapters to go, and then the bulk of the work is completely finished.

NR experiments

Kicked off experiments for the final variant of NR during search.

Meeting

Met with Alan. He’s going to look at the HBR chapter by next Tuesday, and possibly the NR chapter as well if I can finish it in time for him.

I’m going to aim to finish the NR chapter by the end of Wednesday the 10th. To do that, I have to kick off the last two experiments this evening after football.

HBR chapter finished

At last I have finished off the HBR chapter. I had to rewrite a big section after examining some of my results a little more carefully, but it has worked out better than I expected.

Now back to the NR chapter…

HBR experiments

Now I’m repeating (2003-09-03-001) my earlier HBR heuristic visibility experiments (2003-01-23-001) but with a 20 minute timeout. Hopefully this will let Swan solve enough of the instances to make comparison with Chaff more reasonable.

The neighbour resolution experiments (2003-09-01-001) have finally finished. Looking at the results, implementing Alan’s suggestion with respect to approximating the top of the search tree could well be the icing on the empirical cake, so I’ll kick that off once the HBR experiments finish (hopefully by tomorrow morning).

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.

Meeting

Brief meeting with Alan again:

• Described my experimental woes over the weekend. He was as surprised as I was to discover that his machine has no swap.
• Alan suggested an even more improved NR idea: every decision node where the number of undef vars is > 90%, say. Much better than the very crude approximation for the top of the search space I currently have, which completely ignores the effect of unit propagation.
• Decided to set myself some serious deadlines: HBR chapter by tomorrow morning, and the NR chapter by Thursday morning.

Last few days

Since the last PhD entry:

• Met briefly with Alan on Thursday.
• In the AT-HBR completeness proof, need to check out the case when HBR produces the nucleus clause.
• Ditched the old NR chapter, and started again with a completely new outline. Copied and pasted various bits into the new chapter.
• Spent the weekend working on AT-HBR experiments. Finally managed to fix the last remaining bugs, but it all just runs too slowly. Figured out a faster method of eliminating trivial clauses, and some ideas for incremental updating of the AT.
• Realised on Monday that I needed to get back to the NR chapter if I was to get it finished by Tuesday. While working on the results sections, I decided that I needed more experiments, especially after finding that some of the earlier experiments had run out of memory on Alan’s machine (which only has 256MB of RAM). Now I need to rerun them on my machine (which has 1GB), but they will take on the order of 30 hours to run. This also means that I can’t run any more AT-HBR experiments until the NR ones have finished, as my machine is the only one with enough memory to mean that rerunning the experiments won’t be necessary.
• Still need to code up the code to fix the branch order, so as to replicate the heuristic interaction work from the HBR chapter.

Today's work

• Added lots of definitions, lemmas and a couple of proofs to the hyper-binary resolution and AT-HBR section.

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?

Experiments and proofs

• Neighbour resolution experiments are still running, but should be finished by tomorrow morning and cover all the remaining results I need.
• Restructured my thesis chapters.
• Got part way through doing the proofs relating AT and HBR.
• Kicked off another set of experiments, this time on binary equivalence finding.

Neighbour resolution

• Have a large set of neighbour resolution experiments running at the moment, after a time-consuming false start with the wrong set of benchmarks. This should form the last piece of experimental work needed for the relevant thesis chapter.
• Also updated my publications and presentations web pages, which had become horribly out of date.

More experiments

Today’s work includes:

• Started the first set of assignment table experiments again, this time with the buggy equivalence checking code disabled.
• Figured out the equivalence checking problem, and fixed the code.
• Added a first cut at the code to do hyper-binary resolution inference from the assignment table. Unfortunately, it seems to be generating multiple sets of each clause. It also needs to check whether the inferred clause already exists in the formula. This bit of code is likely to be very slow at first, even once I get it working.
• Kicked off the second set of assignment table experiments, with working equivalence checking code.

Today's work

• Dug up the old NR source code.
• Put my thesis into revision control - lets me automatically check on progress each day.
• Got all the citations in the interaction chapter sorted out.
• Went through the results of the most recent assignment table experiments, and found that the preprocessor was proving a number of satisfiable instances unsat. Eventually tracked it down to the equivalence checking code. My first guess was that the equivalence detection was OK, and that the replacement of one variable with another was flawed. However, it appears that the logic for finding the equivalences is incorrect, though I still haven’t figured out exactly why.

Assignment table experiments

• Ran a set of experiments on the structured SATLIB instances using the new assignment table preprocessor; some nice results, but also a rather serious bug that means that I need to rerun the experiments. Got this diary up and running.