2015/08/22 by Ajith K. John, Shetal Shah, John, Ajith K. +7 · 3 citations
Computer Science · #Logic, programming, and type systems #Formal Methods in Verification #Logic, Reasoning, and Knowledge
paper · pdf · doi:10.48550/arxiv.1508.05497
Given a propositional formula F(x,y), a Skolem function for x is a function Ψ(y), such that substituting Ψ(y) for x in F gives a formula semantically equivalent to ∃ F. Automatically generating Skolem functions is of significant interest in several applications including certified QBF solving, finding strategies of players in games, synthesising 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 paper, 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.