Arotau

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.