Require multiple keys to open a door isn't sufficient for key logic

[aspiwack]

Let's imagine a dungeon. You have one chest available in the front. It's necessarily a key. But then you have two doors.

If you say that the doors are accessible with a single key, then a player may take “the wrong door”, and lock all the keys in the dungeon behind the other door, that they can't open. The current engine considers this as correct.

If, on the other hand, you require two keys to open the door, then, well, there is never a solution. So there is 0 valid shuffles.

Instead, we need to be able to take into account that some keys can be locked behind doors, and that, in fact, when multiple doors are available in parallel, it may be necessary that these doors have keys behind them, in order to be able to open the other doors.

This problem shows up in full in Palace of Darkness, in Alttpr: it has a lot of parallel doors.

[aspiwack]

My current thoughts are as follows:

• We need to forget about monotonicity, and make it possible to spend a key (I use a key, I don't have it anymore). This is not a huge modification of the Provability module (though it will deserve a change of name). This loses some connection with modal logic which I had hoped could help improve efficiency later.
• Change the SAT program from “reach the goal” to “not reach a position where you can't reach the goal”. It may be that it's a much harder program.

An alternative would be to introduce some conjunctions in a smart way where they matter.

The benefit of these approaches is clear: key logic becomes very easy as each door simply consume one key.