Chennai Mathematical Institute

Seminars




2.00 pm, Seminar Hall
Counterexample guided Skolem Function Synthesis from Factored Specifications

Supratik Chakraborty
IIT Bombay.
02-09-16


Abstract

Given a propositional formula F(x,y), a Skolem function for x is a function \psi(y), such that substituting \psi(y) for x in F gives a formula semantically equivalent to \exists x F(x, y).

Automatically generating Skolem functions is of significant interest in several applications including certified QBF solving, finding strategies of players in games, synthesizing circuits and bit-vector programs from specifications, disjunctive decomposition of sequential circuits, etc.

In many such applications, F is given as a conjunction of factors, each of which depends on a small subset of variables. Existing algorithms for Skolem function generation ignore any such factored form and treat F as a monolithic function. This presents scalability hurdles in medium to large problem instances.

In this work, we argue that exploiting the factored form of F can give significant performance improvements in practice when computing Skolem functions. We present a new CEGAR style algorithm for generating Skolem functions from factored propositional formulas. In contrast to earlier work, our algorithm neither requires a proof of QBF satisfiability nor uses composition of monolithic conjunctions of factors. We show experimentally that our algorithm generates smaller Skolem functions and outperforms state-of-the-art approaches on several large benchmarks.

(Joint work with S. Akshay, Shetal Shah, Ajith John and Ashutosh Trivedi)