Caching for BDDs Enabled Although Documented as Erroneous

[pmbittner]

Hi @ckaestne and TypeChef devs,

on the master branch, in the SATBDDSolver the CACHING is activated although there is a comment indicating that this may yield incorrect results:

TypeChef/FeatureExprLib/src/main/scala/de/fosd/typechef/featureexpr/bdd/SatBDDSolver.scala

Lines 78 to 83 in fb4d7ad

	/**
	* caching can reuse SAT solver instances, but experience
	* has shown that it can lead to incorrect results,
	* hence caching is currently disabled
	*/
	val CACHING = true

So I wonder if caching shouldn't be deactivated here as stated by the comment?
Could I obtain wrong results when running TypeChef and having CACHING set to true here?

Thanks for any help!

[ckaestne]

Sorry, this has been too long. I vaguely remember that there were some issues, but I suspect that it has been fixed and the comment is outdated. I think this was a weird nondeterministic problem but unloading clauses from the solver in early attempts to use it.

[pmbittner]

Ok, thank you very much for the fast reply! I will leave this set to true then.

Interestingly, the CACHING is deactivated for the SatSolver (for propositional formulas instead of BDDs) with the very same comment:

TypeChef/FeatureExprLib/src/main/scala/de/fosd/typechef/featureexpr/sat/SatSolver.scala

Lines 18 to 23 in fb4d7ad

	/**
	* caching can reuse SAT solver instances, but experience
	* has shown that it can lead to incorrect results,
	* hence caching is currently disabled
	*/
	val CACHING = false

So maybe this should be activated then, too.

[ckaestne]

So this is way too long ago to trust anything that I say (and I don't even remember how much of it I wrote myself), but:

The implementation of how constraints are removed differ slightly:

TypeChef/FeatureExprLib/src/main/scala/de/fosd/typechef/featureexpr/bdd/SatBDDSolver.scala

Lines 221 to 230 in fb4d7ad

	for (constr <- constraintGroup.filter(_ != null)) {
	try {
	val succeeded = solver.removeConstr(constr)
	if (!succeeded)
	invalidateCache()
	} catch {
	case e: AssertionError => invalidateCache()
	case e: NullPointerException => invalidateCache()
	}
	}

vs

TypeChef/FeatureExprLib/src/main/scala/de/fosd/typechef/featureexpr/sat/SatSolver.scala

Lines 203 to 204 in fb4d7ad

	for (constr <- constraintGroup)
	assert(solver.removeConstr(constr))

which may very well be responsible for this differences. It could be that one is fixed for an issue in the other.

The key idea of caching is to add all clauses from the feature model only once and then add and remove the clauses from the individual expressions on every satisfiability check. At some point there were issues that removing clauses didn't work as intended. I don't remember whether and how it got fixed, but I assume it works as in the repo. It may work with caching in the Sat implementation or not or only after adding and removing clauses the same way.

Sorry to not be of more help and good luck!

[pmbittner]

Interesting and sounds reasonable. This is already a big help, thank you! We will leave things as is then for now.