SUPRA: Satisfiability UPon GeneRAlization beyond SAT

• Applicant: Professor Dr.-Ing. Christoph Scholl
• Subject Area: Security and Dependability, Operating-, Communication- and Distributed Systems ; Computer Architecture, Embedded and Massively Parallel Systems ; Theoretical Computer Science
• Term: since 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 508508079

The goal of the project is to advance satisfiability technologies beyond propositional SAT which has become a mature technology that has gained high industrial relevance and has been pervasively applied in various application domains, such as artificial intelligence (AI), electronic design automation (EDA), and (hardware and software) verification.Motivated by practically relevant applications that require extended formalisms to allow natural and compact formulations, we extend the consideration of propositional SAT along four dimensions: quantification, partial information, uncertainty, and non-boolean domains.We look into Quantified Boolean Formulas (QBFs) containing universal and existential quantifiers as well as Dependency Quantified Boolean Formulas (DQBFs) enabling existential quantification with partial information.In this field, we look in particular into open challenges in certification, which provides additional information (besides a yes / no answer), allowing us to check the solver answer without considering the implementation of the solver itself.Since the nature of more and more applications is probabilistic, we also look into extending SAT solving to Stochastic SAT (SSAT) that computes/estimates satisfying *probabilities*.Our goals in this context are to improve on the efficiency of existing prototype SSAT solvers as well as to integrate certification into SSAT solvers. Combining uncertainty with partial information, we arrive at an extension of SSAT to Dependency Stochastic SAT (DSSAT).Finally, since many applications (especially in software and hybrid systems analysis) require an extension of the Boolean domain by various theories reasoning over non-Boolean domains, we will transfer ideas from the design of modern QBF and DQBF solvers into the field of `SAT modulo theories.'In summary, we will develop new concepts, algorithms and tools for generalized decision procedures beyond propositional SAT,taking another large step towards applicability to real-world problems. The following applications in AI, EDA, and system verification may (among others) profit from the developed tools:the verification of certain classes of partial digital circuits, the synthesis of topologically constrained logical circuits,the analysis of noncooperative games with incomplete information, the synthesis of safe controllers for discrete systems and hybrid systems,various AI planning problems like multi-agent planning and probabilistic planning,formal verification of probabilistic designs (taking the probabilistic behavior of modern nano-scale designs into account),the analysis of Partially Observable Markov Decision Processes (POMDP) and Decentralized Partially Observable Markov Decision Processes (Dec-POMDP), and the analysis of software security.

• DFG Programme: Research Grants
• International Connection: Taiwan
• Partner Organisation: National Science and Technology Council (NSTC)
• Cooperation Partner: Professor Jie-Hong Roland Jiang, Ph.D.