S. Akshay

IJCAI Conference 2025 Conference Paper

LP-Based Weighted Model Integration over Non-Linear Real Arithmetic

• S. Akshay
• Supratik Chakraborty
• Soroush Farokhnia
• Amir Goharshady
• Harshit Jitendra Motwani
• Đorđe Žikelić

Weighted model integration (WMI) is a relatively recent formalism that has received significant interest as a technique for solving probabilistic inference tasks with complicated weight functions. Existing methods and tools are mostly focused on linear and polynomial functions and provide limited support for WMI of rational or radical functions, which naturally arise in several applications. In this work, we present a novel method for approximate WMI, which provides more effective support for the wide class of semi-algebraic functions that includes rational and radical functions, with literals defined over non-linear real arithmetic. Our algorithm leverages Farkas’ lemma and Handelman's theorem from real algebraic geometry to reduce WMI to solving a number of linear programming (LP) instances. The algorithm provides formal guarantees on the error bound of the obtained approximation and can reduce it to any user-defined value epsilon. Furthermore, our approach is perfectly parallelizable. Finally, we present extensive experimental results, demonstrating the superior performance of our method on a range of WMI tasks for rational and radical functions when compared to state-of-the-art tools for WMI, in terms of both applicability and tightness.

KR Conference 2025 Conference Paper

Presburger Functional Synthesis: Complexity and Tractable Normal Forms

• S. Akshay
• A. R. Balasubramanian
• Supratik Chakraborty
• Georg Zetzsche

Given a relational specification between inputs and outputs as a logic formula, the problem of functional synthesis is to automatically synthesize a function from inputs to outputs satisfying the relation. Recently, a rich line of work has emerged tackling this problem for specifications in different theories, from Boolean to general first-order logic. In this paper, we launch an investigation of this problem for the theory of Presburger Arithmetic, that we call Presburger Functional Synthesis (PFnS). We show that PFnS can be solved in EXPTIME and provide a matching exponential lower bound. This is unlike the case for Boolean functional synthesis (BFnS), where only conditional exponential lower bounds are known. Further, we show that PFnS for one input and one output variable is as hard as BFnS in general. We then identify a special normal form, called PSyNF, for the specification formula that guarantees poly-time and poly-size solvability of PFnS. We prove several properties of PSyNF, including how to check and compile to this form, and conditions under which any other form that guarantees poly-time solvability of PFnS can be compiled in poly-time to PSyNF. Finally, we identify a syntactic normal form that is easier to check but is exponentially less succinct than PSyNF.

AAAI Conference 2024 Conference Paper

Auditable Algorithms for Approximate Model Counting

• Kuldeep S. Meel
• Supratik Chakraborty
• S. Akshay

The problem of model counting, i.e., counting satisfying assignments of a Boolean formula, is a fundamental problem in computer science, with diverse applications. Given #P-hardness of the problem, many algorithms have been developed over the years to provide an approximate model count. Recently, building on the practical success of SAT-solvers used as NP oracles, the focus has shifted from theory to practical implementations of such algorithms. This has brought to focus new challenges. In this paper, we consider one such challenge – that of auditable deterministic approximate model counters wherein a counter should also generate a certificate, which allows a user (often with limited computational power) to independently audit whether the count returned by an invocation of the algorithm is indeed within the promised bounds. We start by examining a celebrated approximate model counting algorithm due to Stockmeyer that uses polynomially many calls to a \Sigma^2_P oracle, and show that it can be audited via a \Pi^2_P formula on (n^2 log^2 n) variables, where n is the number of variables in the original formula. Since n is often large (10’s to 100’s of thousands) for typical instances, we ask if the count of variables in the certificate formula can be reduced – a critical question towards potential implementation. We show that this improvement in certification can be achieved with a tradeoff in the counting algorithm’s complexity. Specifically, we develop new deterministic approximate model counting algorithms that invoke a \Sigma^3_P oracle, but can be certified using a \Pi^2_P formula on fewer variables: our final algorithm uses just (n log n) variables. Our study demonstrates that one can simplify certificate checking significantly if we allow the counting algorithm to access a slightly more powerful oracle. We believe this shows for the first time how the audit complexity can be traded for the complexity of approximate counting.

IJCAI Conference 2024 Conference Paper

Certified Policy Verification and Synthesis for MDPs under Distributional Reach-Avoidance Properties

• S. Akshay
• Krishnendu Chatterjee
• Tobias Meggendorfer
• Đorđe Žikelić

Markov Decision Processes (MDPs) are a classical model for decision making in the presence of uncertainty. Often they are viewed as state transformers with planning objectives defined with respect to paths over MDP states. An increasingly popular alternative is to view them as distribution transformers, giving rise to a sequence of probability distributions over MDP states. For instance, reachability and safety properties in modeling robot swarms or chemical reaction networks are naturally defined in terms of probability distributions over states. Verifying such distributional properties is known to be hard and often beyond the reach of classical state-based verification techniques. In this work, we consider the problems of certified policy (i. e. controller) verification and synthesis in MDPs under distributional reach-avoidance specifications. By certified we mean that, along with a policy, we also aim to synthesize a (checkable) certificate ensuring that the MDP indeed satisfies the property. Thus, given the target set of distributions and an unsafe set of distributions over MDP states, our goal is to either synthesize a certificate for a given policy or synthesize a policy along with a certificate, proving that the target distribution can be reached while avoiding unsafe distributions. To solve this problem, we introduce the novel notion of distributional reach-avoid certificates and present automated procedures for (1) synthesizing a certificate for a given policy, and (2) synthesizing a policy together with the certificate, both providing formal guarantees on certificate correctness. Our experimental evaluation demonstrates the ability of our method to solve several non-trivial examples, including a multi-agent robot-swarm model, to synthesize certified policies and to certify existing policies.

Highlights Conference 2022 Conference Abstract

Boolean Functional Synthesis: A View from Theory and Practice

• S. Akshay

It is often easy to write down the specification of a system as a relation between inputs and outputs. But implementing it requires us to take a functional view, i. e. , to have functions that produce outputs from inputs. Can we automatically synthesize such functions from a given relational specification? In this tutorial, we focus on this question in the Boolean setting: given a relation between Boolean inputs and outputs as the specification, the Boolean functional synthesis problem asks to synthesize each output as a function of the inputs such that the specification is met. We start by showing the centrality of this problem via multiple examples and applications in a variety of domains ranging from program synthesis to planning. We then look at theoretical hardness results and survey some of the algorithmic techniques that have been developed in recent years to tackle this problem, remarking on their surprising practical performance. This leads us to examine the structure of specification in more depth and doing so we develop a theory of knowledge representations and new algorithmic directions. We end with several open questions and avenues for future work.

Highlights Conference 2021 Conference Abstract

Knowledge Representations for Efficient Boolean Functional Synthesis

• S. Akshay

Given a relational specification between Boolean inputs and outputs, the goal of Boolean functional synthesis is to synthesize each output as a function of the inputs such that the specification is satisfied. More precisely, given a Boolean formula F (X, I), where X is a vector of outputs and I is a vector of inputs, the Boolean Skolem function synthesis problem (BFnS) asks to compute a Skolem function vector G(I) such that F (G(I), I) holds whenever ∃X F (X, I) holds. This problem has a wide variety of applications ranging from cryptanalysis to certified QBF solving to reactive synthesis. In general, this problem is known to be hard: indeed complexity-theoretic hardness results show polysized and polytime computable Skolem functions are unlikely to exist always. However, algorithms developed using different techniques seem to perform surprisingly well on a wide set of benchmarks. This motivates us to ask if there is structure in the input representation that allows for efficient computation of Skolem functions. This investigation leads us down a rabbithole of knowledge representations, which enable efficient (in size and time) synthesis of Skolem functions. First, it is easy to see that well-known normal forms like BDDs, DNNFs permit efficient synthesis. But we can go significantly beyond this and obtain a semantic (checkable with a SAT solver!) condition on the specification that also allows for efficient Skolem function synthesis. This results in a normal form that is exponentially more succinct than the previous ones and yet permits efficient Skolem function synthesis. Finally, we ask if we may precisely characterize polytime and polysized Skolem function synthesis. Surprisingly, the answer is yes! We develop a normal form that captures exactly this requirement and examine its many properties and possible implications. This work is based on papers presented in FMCAD’2019 and a very recent work accepted at LICS’2021. [LICS’2021] A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis. Long version available at ArXiv: https: //arxiv. org/abs/2104. 14098[FMCAD’2019] Knowledge Compilation for Boolean Functional Synthesis. Long version available at ArXiv: https: //arxiv. org/abs/1908. 06275[Coauthors: All this work is joint with Supratik Chakraborty of IIT Bombay. The LICS’21 paper is also with Preey Shah and Aman Bansal, while FMCAD’19 was jointly done with Jatin Arora, Divya Raghunathan, Shetal Shah and S. Krishna. All authors are from IIT Bombay or were at IIT Bombay when a bulk of the work was carried out. ]

TCS Journal 2015 Journal Article

Checking conformance for time-constrained scenario-based specifications

• S. Akshay
• Paul Gastin
• Madhavan Mukund
• K. Narayan Kumar