Parameterised MDL cost function

[sfluegel05]

closes #143

This PR adds 3 command line parameters to Popper that are only relevant if the --noisy flag is set:

• size-weight increases the impact of program size on the total cost
• fp-weight increases the impact of false positives
• fn-weight increases the impact of false negatives

I also tried to adjust the various heuristics that are influenced by the weights, but I am not sure if I got all of them right.

Potential issues

Heuristic in tester.py

The tester has some condition based on the number of TPs vs. program size. This should probably get weighted, but I'm not sure what the intention of this condition is:

Popper/popper/tester.py

Lines 161 to 166 in a4f3eb1

	if tp > prog_size:
	# maximum size of specialisations allowed
	max_k_neg1 = min(settings.max_body - (prog_size - 1), self.state.max_literals - prog_size)
	# conditions which determine whether a program can be part of a solution
	max_k_neg2 = min(self.state.best_hypothesis_mdl - prog_size, tp - prog_size)
	max_k_neg = max(max_k_neg1, max_k_neg2)

Timeout in combiner_mdl.py

The combiner only applies the anytime timeout if last_combine_stage is false. This leads to Popper not terminating properly if fn-weight is set. My understanding is that the solver suddenly has to look at far larger rules to determine whether they make a minimal improvement in the number of FNs.

Popper/popper/combiner_mdl.py

Lines 441 to 444 in a4f3eb1

	if last_combine_stage or not self.settings.nuwls:
	_, model = maxsat.exact_maxsat_solve(encoding, soft_clauses, weights)
	else:
	_, model = maxsat.anytime_maxsat_solve(encoding, soft_clauses, weights, self.settings.anytime_timeout)

Popper/popper/combiner_mdl.py

Lines 491 to 492 in a4f3eb1

	if not last_combine_stage:
	solver.parameters.max_time_in_seconds = self.settings.anytime_timeout

I tested this for the noisy-zendo2-10 task with a timeout of 30 seconds. With NuWLS, Popper terminated after ~90s. With CPSAT, Popper didn't terminate within 400s. For now, I have removed the exemption for the last combine stage.

Results on noisy-zendo2-10

I tested this for the noisy-zendo2-10 example.
The results are as you would expect - size-weight gives you shorter rules, fp-weight gives you better precision, fn-weight better recall.

Below are the commands and solutions:
Standard MDL:

python popper.py examples/noisy-zendo2-10 --noisy --timeout 30 --nuwls 

40.5s ********** SOLUTION **********
40.5s Precision:0.90 Recall:0.91 TP:90 FN:9 TN:91 FP:10 Size:14 MDL:33
40.5s zendo(V0):- piece(V0,V1),green(V1),piece(V0,V2),blue(V2),piece(V0,V3),red(V3).
40.5s zendo(V0):- piece(V0,V1),green(V1),coord1(V1,V3),piece(V0,V2),lhs(V2),coord1(V2,V3).
40.5s ******************************

With size weight:

python popper.py examples/noisy-zendo2-10 --noisy --timeout 30 --nuwls --seize-weight 10

4.5s ********** SOLUTION **********
4.5s Precision:0.61 Recall:0.96 TP:95 FN:4 TN:40 FP:61 Size:3 MDL:95
4.5s zendo(V0):- piece(V0,V1),green(V1).
4.5s ******************************

With FP weight:

python popper.py examples/noisy-zendo2-10 --noisy --timeout 30 --nuwls --fp-weight 10

32.5s ********** SOLUTION **********
32.5s Precision:1.00 Recall:0.53 TP:52 FN:47 TN:101 FP:0 Size:23 MDL:70
32.5s zendo(V0):- piece(V0,V1),green(V1),rhs(V1),piece(V0,V2),lhs(V2),green(V2).
32.5s zendo(V0):- piece(V0,V1),red(V1),piece(V0,V2),blue(V2),piece(V0,V3),upright(V3),green(V3).
32.5s zendo(V0):- large(V3),piece(V0,V1),lhs(V1),size(V1,V3),piece(V0,V2),size(V2,V3),green(V2).
32.5s ******************************

With FN weight:

python popper.py examples/noisy-zendo2-10 --noisy --timeout 30 --nuwls --fn-weight 10

44.6s ********** SOLUTION **********
44.6s Precision:0.80 Recall:1.00 TP:99 FN:0 TN:77 FP:24 Size:33 MDL:57
44.6s zendo(V0):- medium(V2),piece(V0,V1),rhs(V1),blue(V1),size(V1,V2).
44.6s zendo(V0):- piece(V0,V1),upright(V1),piece(V0,V2),lhs(V2),red(V2).
44.6s zendo(V0):- piece(V0,V1),green(V1),coord1(V1,V3),piece(V0,V2),lhs(V2),coord1(V2,V3).
44.6s zendo(V0):- piece(V0,V1),strange(V1),coord1(V1,V3),size(V1,V3),piece(V0,V2),rhs(V2).
44.6s zendo(V0):- piece(V0,V1),green(V1),piece(V0,V2),red(V2),piece(V0,V3),blue(V3).
44.6s ******************************