Project Solving Satisfiability Modulo Counting Problems with Guarantees Program Science Term Academic Year 2024 Status Accepted Research Area Logic, Constraint Satisfaction, Artificial Intelligence, Machine Learning Description Symbolic and statistical approaches are two fundamental driving forces of Artificial Intelligence (AI). Symbolic AI, exemplified by SATisfiability (SAT), finds solutions satisfying constraints but requires rigid formulations and is difficult to include probabilities. Statistical AI captures uncertainty but often lacks constraint satisfaction. Integrating symbolic and statistical AI remains an open field and has gained research attention recently. Satisfiability Modulo Counting (SMC) encompasses problems that require both symbolic decision-making and statistical reasoning. Informally, an SMC problem encompasses problems that carry out satisfiability (symbolic decision-making) with constraints involving model counting (statistical reasoning) to be satisfied. Its general formulation captures many real-world problems. For example, supply chain design in facing stochastic demand, biodiversity protection, internet resilience, social influence maximization, energy security, etc. However, solving SMC is challenging because of its highly intractable nature. Research on solving SMC generally follows two approaches: approximate and exact solvers. Many of these approaches lack provable guarantees and/or suffer from suboptimal empirical performance. This project focuses on exploring and understanding the latest advancements in SMC problem-solving. Our aim is to review current research in the field, identifying both the innovative aspects and the areas that need improvement. By summarizing these findings, we intend to foster a deeper understanding of SMC solving and potentially develop new solvers for problems intersecting symbolic and statistical AI. Supervisor Yexiang Xue Mentor Type of work required The project is set to improve Symbolic and Statistical Reasoning in AI, starting with
tackling Satisfiability Modulo Counting (SMC) problems. We’ll start by examining recent research and
replicating the most up-to-date methods in this field. Throughout this process, we anticipate that students
will gain knowledge about the latest advancements and offer new ideas from these discussions and hands-on
experiences. Any new contributions are expected to benefit the research area as a whole. Specifically, our
expected objectives are:

- conduct a comprehensive review of state-of-the-art SMC-solving techniques.
- identify and summarize the novel contributions and limitations of recent studies.
- replicate existing methods and apply them to practical, real-world scenarios.
- encourage the development of new ideas and solvers that can advance the field of SMC problem-solving. Websites Qualifications The students would be required to know C/C++ and Python programming. The students would need to understand some basic concepts in algorithm design and artificial intelligence. The students need to conduct paper reading and presentation and code implementation. Credit Hours 3 Weekly Hours 5 (estimated)