LogicalReasoning_LLMs

As part of my final year project, this application uses LLM's to convert constraint satisfaction problems like the Zebra Puzzle to input's for the Z3 SMT and use the output from the SMT to test and check the reasoning capabilities of these LLMs against the Z3 benchmark.

To run the project, simply type:

python main.py --puzzle_name --strategy --variant --llm

or

python main.py

for a default run.