If you're gonna formulate this conversation as a satisfiability problem you should be aware that this is an NP-complete problem (and actually working on that problem is the source of the insight that there is such as thing as NP-completeness).