Set of arrays?

[anchpop]

I'm having some trouble with formalizing something, and I think a set of arrays would help. I have some possible killers, who each can kill only certain victims. I'm trying to find the set of killers such that there's exactly one mapping from victim to who killed them, with the requirement that everyone in the set must have killed a victim.

For example, if we have three killers killer1 killer2 and killer3, where killer1 can kill victims {A, B}, killer2 can kill victims {A, B}, and killer3 can kill victims {B}, then {killer1, killer3} is a valid set of killers because we know for them both to have killed someone, killer1 must have killed A and killer2 must have killed B.

I think the natural way to model this with a SSet Name set of killers, and a SSet (SArray Name Name) mapping from victims to who killed them (if anyone). Then we could require that the latter set only have one element, which would force the former set to have the set of killers that results in a unique mapping from victim to killer. But an SSet can't contain a SArray because there's no Ord instance for SAarray. But actually, a set of arrays seems like overkill for this anyway. How would you solve this?

[LeventErkok]

You can't have a set of arrays in SBV; I'm not even sure if z3 would support it actually.

It's hard to opine without seeing some code; but if the set of killers/victims etc. are drawn from a fixed set, then you should simply be able to model them with a boolean attached to say which ones are related. Take a look at https://hackage.haskell.org/package/sbv-8.17/docs/Documentation-SBV-Examples-Puzzles-Murder.html, perhaps that'll provide some intuition?

[anchpop]

Thanks @LeventErkok. The killers/victims etc. are drawn from a fixed set, and what you describe is what I have right now but I can't figure out how to express exactly what I need. The problem is that, among the possible killers, I'm looking for the set of "true killers" (people who kill at least one person) such that knowledge of the set of true killers gives exact knowledge of who killed each victim.

My first thought was to find the set of killers such that there's exactly one person who could have killed each victim. But that's overly restrictive. If those who died were {A, B, C}, and you could kill {A, B, C} and I could kill {C}, then you and I together would still be a valid set of true killers because anyone who knew that both of us were true killers would know that I must have killed C and you must have killed A and B. That is to say, I'm looking for the set of "true killers" such that there's a unique mapping from victims to those that killed them and every true killer kills at least one victim.

With just a boolean to see who's related, I don't know how to enforce this constraint.

[LeventErkok]

It's hard to follow all the details of the problem you're trying to solve unfortunately. You might also want to look at https://hackage.haskell.org/package/sbv-8.17/docs/Documentation-SBV-Examples-Puzzles-Birthday.html, which deals with knowledge you can gain when you learn something about what other people can or cannot deduce. Perhaps the modeling idea there can help.

If not, can you point me to the description of the problem itself. I can have a go at it.

[anchpop]

@LeventErkok sorry for the late reply. The problem is here https://docs.google.com/document/d/14QN2NuCTMQZEr1I9iG_cab3plNpUbOJdPQKkNDj0AzA/edit and my progress towards it is here https://github.com/anchpop/a-purple-reunion-solution (although it doesn't give the correct answer and probably won't be very useful).

The meat is at the end:

room 1: Wolfgang, Lance, Princessa
Gizmo and Hattie guarantee their alibis.
Vince and Alouette guarantee their alibis.
Grincella and Frendley guarantee their alibis.
Hattie checks Wolfgang’s body.
Alouette checks Lance’s body.
Grincella checks Princessa’s body.

Alouette says that Lance said in purple that none of the women could’ve killed any of the men, throughout the whole story.

room 2: Hattie, Vince
Simone, Grincella, and Alouette guarantee their alibis.
Gizmo and Frendley guarantee their alibis.
Gizmo checks Hattie’s body.
Frendley checks Vince’s body.
Gizmo says Vince did not kill Hattie.
Vince says Wolfgang did not kill him.

room 3: Alouette
Simone and Frendley guarantee their alibis.
Grincella and Gizmo guarantee their alibis.
Simone checks Alouette’s body.

The tricky part is here:

JUST FROM THE FACTS GIVEN SO FAR, IF I TOLD THE READER THE COMPLETE LIST OF EVERYONE WHO IS A CULPRIT IN THE STORY, THEY WOULD BE ABLE TO DEDUCE WITHOUT FAIL, EXACTLY WHICH CULPRIT KILLED EACH AND EVERY PERSON WHO DIED.

I originally interpreted this as an incidental/redundant fact about the set of culprits, but really it's a huge restriction on the set of culprits.

[LeventErkok]

Wow, that’s a really long and complicated story. I’m afraid I’m neither very good at these things nor have the bandwidth to look into it in any detail.

I’m going to close this ticket as I don’t see any actionable items for SBV here. The issue tracker is more suitable for tracking bugs/feature requests etc. If you do run into an SBV bug feel free to file a new ticket. Best of luck with the puzzle!