Campus Event Calendar

Event Entry

What and Who

Proofs and Dependency Schemes for Stochastic Quantified Satisfiability

Yun-Rong Luo
National Taiwan University
PhD Application Talk
AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI  
AG Audience

Date, Time and Location

Monday, 23 January 2023
-- Not specified --
Virtual talk


Boolean satisfiability (SAT) solvers have been successfully applied in various areas such as artificial intelligence, model checking, electronic design automation, and combinatorics. The success of SAT solvers has motivated the studies of more expressive logical formalisms such as quantified Boolean formula (QBF), dependency quantified Boolean formula (DQBF), and their respective stochastic variants stochastic Boolean satisfiability (SSAT) and dependency stochastic Boolean satisfiability (DSSAT). This talk will introduce my graduate research on certification and dependency theory for SSAT/DSSAT and discuss our current plans of applying the theories to practical solver processing techniques and validation. The talk is divided into the following parts. The first part introduces our proposed first sound and complete resolution proof system for DSSAT. With favorable properties such as generating polynomial-time verifiable proofs and allowing local pruning, the proposed DSSAT proof system may serve as a theoretical foundation for future solver development and certification. The second part presents the preliminary results of lifting the QBF dependency schemes theory to SSAT, which enables safe quantifier reordering techniques in SSAT solving. We are planning to develop SSAT pre-processing or in-processing techniques based on SSAT dependency schemes. The talk will be concluded with a summary of our contribution to SSAT/DSSAT proof systems and dependency schemes theory as well as possible future research direction towards solver validation.


Jennifer Gerling
+49 681 9325 1801
--email hidden

Virtual Meeting Details

passcode not visible
logged in users only

Jennifer Gerling, 01/22/2023 17:48 -- Created document.