AG 1, AG 2, AG 3, INET, AG 4, AG 5, D6, SWS, RG1, MMCI   Info

AG Audience

English

-- Not specified --

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

Zoom

passcode not visible

logged in users only