The Unclear Impact

The Unclear Impact

@juliank A->B|...|Z looks suspiciously like a dual-Horn clause !A | B | ... | Z (although I don’t know what to make of A->!B, other than just !A | !B). but it’s defnitely no accident that your algorithm is pretty much DPLL, given that your input is already basically in CNF blobfoxscience

maybe this is a good time for CDCL?

@juliank ah, materializing further clauses sound reasonable, especially if solutions have a fairly regular structure. i guess your alternative would be to pull in clauses for all transitive dependencies, which sounds a lot more painful

a tricky thing is how to represent useful lemmas (CDCL-style) when some variables from the learned clause might not even be in the original problem (pulled in by a transitive dependency in your case).

the very least, i’m having a lot of trouble with that on the first-order model generator that we’re working on (i can’t even pull in all clauses eagerly in the beginning, because i don’t know the model size in advance and a FOL quantifier could match any model element)

2**32 levels of backtracking.

holy (super) cow! is that a state space of 2**(2**32)?

@juliank the tricky thing is what would happen if you backtrack and the clauses that were in conflict get removed (if you remove versions of packages you decide not necessarily to install on backtracking).

in this case the conflict cause would become useful once you decide to install the same package at some other branch of the search when the variables and clauses get added back again. until then, some variables would be “dangling” (appear in the lemma, but not in the problem proper)

but i guess this is not actually a problem if variables can be uniquely identified (so it is apparent when they are re-added to the problem) and you never branch on “dangling” variables blobfoxthinkgoogly

SAT solvers are weird, man