The course project for this semester focuses on Boolean satisfiability (SAT) and satisfiability modulo theories (SMT) solvers, covered in Module 3. The project can be in one of the following tracks:

1. Application: This track invites you to explore the practical use of solvers within your chosen domain, such as domain-specific automated reasoning, software verification, program synthesis, or optimization. You will model the problem in an appropriate theory, set up a framework to solve it, and demonstrate the solver's effectiveness in addressing complex problems.
2. Integration: This track challenges you to connect solvers with other cutting-edge technologies such as large language models, cloud services, or other advanced systems. You will design and implement interfaces that allow seamless communication between the solver and the chosen technology.
3. Development: This track is for those interested in the creation and enhancement of the solvers themselves. You will delve into the internal workings of solvers, identify areas for improvement, and either extend current solvers or develop new ones from scratch. This track involves implementation, testing on benchmark problems, and optimizing performance.

The project topic must be approved by the instructor. The project can be completed individually or in pairs. Collaboration with individuals from different majors or backgrounds is strongly encouraged.

A project proposal is due by September 28. The proposal should include the chosen domain, the specific problem to be solved, a brief outline of the approach, and expected outcomes. Throughout the project duration, two check-ins are required via brief emails summarizing the project status, progress, and any challenges faced. The check-in dates are October 19 and November 9.

The final submission consists of three main components: a short write-up, codebase, and a poster. The write-up should summarize the approach and outcomes, including an introduction to the problem, methodology, results and analysis, and conclusions. It should not exceed 5 pages. The codebase should be available on Github as a public repository with appropriate documentation and commit history. The poster should visually summarize the project, including the key problem statement, main steps of the approach, significant results, and relevant visual aids. Find some guidelines and a sample here. Both of these are due by November 20. The class on November 28 will be used for project presentations. This 10 to 15 minute presentation should cover an introduction to the chosen domain and problem, a brief explanation of SAT/SMT solvers and how they were applied, the methodology used, key results and findings, challenges faced and how they were overcome, and conclusions drawn from the project.

The project will be evaluated based on the originality and relevance of the chosen problem, appropriate application of SAT/SMT solvers, depth of analysis, quality of results, and the clarity and effectiveness of the final submission and presentation.

Date	Description
September 28	Project Proposal
October 19	Project Check-in I
November 9	Project Check-in II
November 20	Project Submission
November 28	Project Presentation