generally, these class of constraint satisfaction problems fall under the "zebra puzzle" (or einstein puzzle) umbrella [1]. They are interesting because they posit a world with some axioms, and inference procedures, and ask if a certain statement result from them. LLMs as-is (without provers or tool usage) would have a difficult time with these constraint-satisfaction puzzles. 3-sat is a corner-case of these puzzles, and if LLMs could solve them in P time, then we have found a constructive proof of P=NP lol !
Comments
generally, these class of constraint satisfaction problems fall under the "zebra puzzle" (or einstein puzzle) umbrella [1]. They are interesting because they posit a world with some axioms, and inference procedures, and ask if a certain statement result from them. LLMs as-is (without provers or tool usage) would have a difficult time with these constraint-satisfaction puzzles. 3-sat is a corner-case of these puzzles, and if LLMs could solve them in P time, then we have found a constructive proof of P=NP lol !
[1] https://en.wikipedia.org/wiki/Zebra_Puzzle