CAREER: Solving Beyond-NP Satisfiability Modulo Counting Problems with Guarantees Using NP Oracles

Many real-world problems involve planning and decision-making. For example, during natural disasters, city planners must secure multiple paths to emergency shelters for their residents in case of natural disasters. Other examples can be found in disaster preparation, bio-diversity protection and secure energy supply. Another example in machine learning is that of confirming beyond doubt that a drug has a positive effect on a disease. This proposal introduces novel algorithms for such solving complex problems. This research will have a large impact on AI for social good and for science by solving real-world complex problems that require planning and decision-making. The developed algorithms will provide useful diagnosis tools for explainable AI and will have the potential to accelerate the learning of physics models in AI for science. The project will unite symbolic and statistical inference by introducing Satisfiability Modulo Counting (SMC). SMC unites the two types of inference because satisfiability solvers are one of the most widely used symbolic reasoning tools, and weighted model counting subsumes statistical inference. The investigator will design new algorithms with tighter guarantees than previous approaches for SMC. These algorithms will enable solving otherwise beyond reach tasks in statistical inference, structured learning, game theory, operational research, and inverse reinforcement learning. The investigator also intends to grow the field of symbolic and statistical AI integration via SMC solving, further extending the current community effort and bridging satisfiability and algorithmic research with applied AI and machine learning research. This will be achieved via: (1) demonstrating the efficacy of the developed algorithms in solving important real-world SMC problems in AI for social good and for science; (2) nurturing an eco-system of SMC benchmark creation, solver development, and idea communications via hosting SMC competitions; (3) developing workshops, courses and talk series. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.