Tie-break heuristic overflow

[S-Mazigh]

Hello, first of all I'd like to congratulate you on your excellent work. I'm currently studying your implementation to integrate it into the Painless framework and I've noted some remarks that I'd like your opinion on. While testing with the instance "0336f81b60baac5b8f481dd3c32861a5-mod4block_2vars_10gates_u2_autoenc-sc2009" of the SAT2023 competition I noticed that the calculation of the tie-break heuristic value overflows to the negative numbers. It would make more sense to use an unsigned (maybe a ulong to less likely hit 0) as the return type, wouldn't it?

On another note, I'd like to know if the addition of the current variable is redundant given that it is surely present in the listUpdate set.

That's it, normally I've covered everything I wanted your opinion on.

Best regards.

[ndrewh]

I noticed that the calculation of the tie-break heuristic value overflows to the negative numbers. It would make more sense to use an unsigned (maybe a ulong to less likely hit 0) as the return type, wouldn't it?

Yeah, that makes sense. However, I just tried this change out on a branch and it is very detrimental to the instance you mentioned (5 sec CaDiCaL on master 22668af, ... more than 120 sec CaDiCaL on heuristic_ulong branch f82e759). I didn't have time to look into it further, so it could be I just missed something in the implementation... or it could be that this is a case where our heuristic tiebreaking is actually detrimental for some reason.

On another note, I'd like to know if the addition of the current variable is redundant given that it is surely present in the listUpdate set.

Here? I think I agree, it should already be in lits_to_update.

SBVA/sbva.cc

Lines 826 to 830 in 22668af

	// Q.push(var);
	pq.push(make_pair(
	(*lit_to_clauses)[lit_index(var)].size() + (*lit_count_adjust)[lit_index(var)],
	var
	));

[S-Mazigh]

Yeah, that makes sense. However, I just tried this change out on a branch and it is very detrimental to the instance you mentioned (5 sec CaDiCaL on master 22668af, ... more than 120 sec CaDiCaL on heuristic_ulong branch f82e759). I didn't have time to look into it further, so it could be I just missed something in the implementation... or it could be that this is a case where our heuristic tiebreaking is actually detrimental for some reason.

Changing to long or unsigned will result in a different formula compared to int , since the tie-break will likely choose another variable. For the instance in question, we directly see a difference in the number of added variables without having to diff the two output cnf files.

So, as you said, maybe for this given instance the heuristic is detrimental. I think it would be interesting to have different tie-breaking heuristics (a portfolio), however it is difficult to judge which reduced formula is better, the number of deleted clauses ? Launching a solver for each and see who advances faster ? I tested with local search, but the randomness makes the conclusion not reliable.

• master:

[AFTER PARSE] num_vars: 479, num_clauses: 123509, deleted: 720
[END] num_vars: 673, num_clauses: 125117, deleted: 3902

• heuristic_long:

[AFTER PARSE] num_vars: 479, num_clauses: 123509, deleted: 720
[END] num_vars: 670, num_clauses: 125104, deleted: 3884

Here? I think I agree, it should already be in lits_to_update.

SBVA/sbva.cc

Lines 826 to 830 in 22668af

	// Q.push(var);
	pq.push(make_pair(
	(*lit_to_clauses)[lit_index(var)].size() + (*lit_count_adjust)[lit_index(var)],
	var
	));

Yes, I was talking about this code. I apologize, I forgot to cite it. I think that this loop should have already added the variable in question since we delete clauses containing it.

SBVA/sbva.cc

Lines 803 to 808 in 22668af

	for (auto lit : lits_to_update) {
	// Q.push(lit);
	pq.push(make_pair(
	real_lit_count(lit),
	lit
	));