BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Supratik Chakraborty

Supratik Chakraborty appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Logic in Computer ScienceArtificial IntelligenceFormal Languages and Automata Theorymath.LOData Structures and AlgorithmsProgramming LanguagesSoftware Engineering

Catalog footprint

What is connected

18works
7topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

18 published item(s)

preprint2022arXiv

On eventual non-negativity and positivity for the weighted sum of powers of matrices

The long run behaviour of linear dynamical systems is often studied by looking at eventual properties of matrices and recurrences that underlie the system. A basic problem that lies at the core of many questions in this setting is the following: given a set of pairs of rational weights and matrices {(w_1 , A_1 ), . . . , (w_m , A_m )}, we ask if the weighted sum of powers of these matrices is eventually non-negative P (resp. n positive), i.e., does there exist an integer N s.t for all n greater than N , (w_1 A_1^n + ... + w_m A_m^n) is atmost 0 (resp. greater than 0). The restricted setting when m = w_1 = 1, results in so-called eventually non-negative (or eventually positive) matrices, which enjoy nice spectral properties and have been well-studied in control theory. More applications arise in varied contexts, ranging from program verification to partially observable and multi-modal systems. Our goal is to investigate this problem and its link to linear recurrence sequences. Our first result is that for m at least 2, the problem is as hard as the ultimate positivity of linear recurrences, a long standing open question (known to be coNP-hard). Our second result is a reduction in the other direction showing that for any m at least 1, the problem reduces to ultimate positivity of linear recurrences. This shows precise upper bounds for several subclasses of matrices by exploiting known results on linear recurrence sequences. Our third main result is a novel reduction technique for a large class of problems (including those mentioned above) over rational diagonalizable matrices to the corresponding problem over simple real-algebraic matrices. This yields effective decision procedures for diagonalizable matrices.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

On synthesizing Skolem functions for first order logic formulae

Skolem functions play a central role in the study of first order logic, both from theoretical and practical perspectives. While every Skolemized formula in first-order logic makes use of Skolem constants and/or functions, not all such Skolem constants and/or functions admit effectively computable interpretations. Indeed, the question of whether there exists an effectively computable interpretation of a Skolem function, and if so, how to automatically synthesize it, is fundamental to their use in several applications, such as planning, strategy synthesis, program synthesis etc. In this paper, we investigate the computability of Skolem functions and their automated synthesis in the full generality of first order logic. We first show a strong negative result, that even under mild assumptions on the vocabulary, it is impossible to obtain computable interpretations of Skolem functions. We then show a positive result, providing a precise characterization of first-order theories that admit effective interpretations of Skolem functions, and also present algorithms to automatically synthesize such interpretations. We discuss applications of our characterization as well as complexity bounds for Skolem functions (interpreted as Turing machines).

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

On Uniformly Sampling Traces of a Transition System (Extended Version)

A key problem in constrained random verification (CRV) concerns generation of input stimuli that result in good coverage of the system's runs in targeted corners of its behavior space. Existing CRV solutions however provide no formal guarantees on the distribution of the system's runs. In this paper, we take a first step towards solving this problem. We present an algorithm based on Algebraic Decision Diagrams for sampling bounded traces (i.e. sequences of states) of a sequential circuit with provable uniformity (or bias) guarantees, while satisfying given constraints. We have implemented our algorithm in a tool called TraceSampler. Extensive experiments show that TraceSampler outperforms alternative approaches that provide similar uniformity guarantees.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Verifying Array Manipulating Programs with Full-Program Induction

We present a full-program induction technique for proving (a sub-class of) quantified as well as quantifier-free properties of programs manipulating arrays of parametric size N. Instead of inducting over individual loops, our technique inducts over the entire program (possibly containing multiple loops) directly via the program parameter N. Significantly, this does not require generation or use of loop-specific invariants. We have developed a prototype tool Vajra to assess the efficacy of our technique. We demonstrate the performance of Vajra vis-a-vis several state-of-the-art tools on a set of array manipulating benchmarks.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Approximate Probabilistic Inference via Word-Level Counting

Hashing-based model counting has emerged as a promising approach for large-scale probabilistic inference on graphical models. A key component of these techniques is the use of xor-based 2-universal hash functions that operate over Boolean domains. Many counting problems arising in probabilistic inference are, however, naturally encoded over finite discrete domains. Techniques based on bit-level (or Boolean) hash functions require these problems to be propositionalized, making it impossible to leverage the remarkable progress made in SMT (Satisfiability Modulo Theory) solvers that can reason directly over words (or bit-vectors). In this work, we present the first approximate model counter that uses word-level hashing functions, and can directly leverage the power of sophisticated SMT solvers. Empirical evaluation over an extensive suite of benchmarks demonstrates the promise of the approach.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Matching Multiplications in Bit-Vector Formulas

Bit-vector formulas arising from hardware verification problems often contain word-level arithmetic operations. Empirical evidence shows that state-of-the-art SMT solvers are not very efficient at reasoning about bit-vector formulas with multiplication. This is particularly true when multiplication operators are decomposed and represented in alternative ways in the formula.We present a pre-processing heuristic that identifies certain types of decomposed multipliers, and adds special assertions to the input formula encoding the equivalence of sub-terms to word-level multiplication. The pre-processed formulas are then solved using an SMT solver. Our experiments with three SMT solvers show that our heuristic allows several formulas to be solved quickly, while the same formulas time out without the pre-processing step.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Constrained Sampling and Counting: Universal Hashing Meets SAT Solving

Constrained sampling and counting are two fundamental problems in artificial intelligence with a diverse range of applications, spanning probabilistic reasoning and planning to constrained-random verification. While the theory of these problems was thoroughly investigated in the 1980s, prior work either did not scale to industrial size instances or gave up correctness guarantees to achieve scalability. Recently, we proposed a novel approach that combines universal hashing and SAT solving and scales to formulas with hundreds of thousands of variables without giving up correctness guarantees. This paper provides an overview of the key ingredients of the approach and discusses challenges that need to be overcome to handle larger real-world instances.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Skolem Functions for Factored Formulas

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 \exists 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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

Word-level Symbolic Trajectory Evaluation

Symbolic trajectory evaluation (STE) is a model checking technique that has been successfully used to verify industrial designs. Existing implementations of STE, however, reason at the level of bits, allowing signals to take values in {0, 1, X}. This limits the amount of abstraction that can be achieved, and presents inherent limitations to scaling. The main contribution of this paper is to show how much more abstract lattices can be derived automatically from RTL descriptions, and how a model checker for the general theory of STE instantiated with such abstract lattices can be implemented in practice. This gives us the first practical word-level STE engine, called STEWord. Experiments on a set of designs similar to those used in industry show that STEWord scales better than word-level BMC and also bit-level STE.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

A Generalization of the Łoś-Tarski Preservation Theorem over Classes of Finite Structures

We investigate a generalization of the Łoś-Tarski preservation theorem via the semantic notion of \emph{preservation under substructures modulo $k$-sized cores}. It was shown earlier that over arbitrary structures, this semantic notion for first-order logic corresponds to definability by $\exists^k\forall^*$ sentences. In this paper, we identify two properties of classes of finite structures that ensure the above correspondence. The first is based on well-quasi-ordering under the embedding relation. The second is a logic-based combinatorial property that strictly generalizes the first. We show that starting with classes satisfying any of these properties, the classes obtained by applying operations like disjoint union, cartesian and tensor products, or by forming words and trees over the classes, inherit the same property. As a fallout, we obtain interesting classes of structures over which an effective version of the Łoś-Tarski theorem holds.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Balancing Scalability and Uniformity in SAT Witness Generator

Constrained-random simulation is the predominant approach used in the industry for functional verification of complex digital designs. The effectiveness of this approach depends on two key factors: the quality of constraints used to generate test vectors, and the randomness of solutions generated from a given set of constraints. In this paper, we focus on the second problem, and present an algorithm that significantly improves the state-of-the-art of (almost-)uniform generation of solutions of large Boolean constraints. Our algorithm provides strong theoretical guarantees on the uniformity of generated solutions and scales to problems involving hundreds of thousands of variables.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Distribution-Aware Sampling and Weighted Model Counting for SAT

Given a CNF formula and a weight for each assignment of values to variables, two natural problems are weighted model counting and distribution-aware sampling of satisfying assignments. Both problems have a wide variety of important applications. Due to the inherent complexity of the exact versions of the problems, interest has focused on solving them approximately. Prior work in this area scaled only to small problems in practice, or failed to provide strong theoretical guarantees, or employed a computationally-expensive maximum a posteriori probability (MAP) oracle that assumes prior knowledge of a factored representation of the weight distribution. We present a novel approach that works with a black-box oracle for weights of assignments and requires only an {\NP}-oracle (in practice, a SAT-solver) to solve both the counting and sampling problems. Our approach works under mild assumptions on the distribution of weights of satisfying assignments, provides strong theoretical guarantees, and scales to problems involving several thousand variables. We also show that the assumptions can be significantly relaxed while improving computational efficiency if a factored representation of the weights is known.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

A Scalable and Nearly Uniform Generator of SAT Witnesses

Functional verification constitutes one of the most challenging tasks in the development of modern hardware systems, and simulation-based verification techniques dominate the functional verification landscape. A dominant paradigm in simulation-based verification is directed random testing, where a model of the system is simulated with a set of random test stimuli that are uniformly or near-uniformly distributed over the space of all stimuli satisfying a given set of constraints. Uniform or near-uniform generation of solutions for large constraint sets is therefore a problem of theoretical and practical interest. For Boolean constraints, prior work offered heuristic approaches with no guarantee of performance, and theoretical approaches with proven guarantees, but poor performance in practice. We offer here a new approach with theoretical performance guarantees and demonstrate its practical utility on large constraint sets.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

A Scalable Approximate Model Counter

Propositional model counting} (#SAT), i.e., counting the number of satisfying assignments of a propositional formula, is a problem of significant theoretical and practical interest. Due to the inherent complexity of the problem, approximate model counting, which counts the number of satisfying assignments to within given tolerance and confidence level, was proposed as a practical alternative to exact model counting. Yet, approximate model counting has been studied essentially only theoretically. The only reported implementation of approximate model counting, due to Karp and Luby, worked only for DNF formulas. A few existing tools for CNF formulas are bounding model counters; they can handle realistic problem sizes, but fall short of providing counts within given tolerance and confidence, and, thus, are not approximate model counters. We present here a novel algorithm, as well as a reference implementation, that is the first scalable approximate model counter for CNF formulas. The algorithm works by issuing a polynomial number of calls to a SAT solver. Our tool, ApproxMC, scales to formulas with tens of thousands of variables. Careful experimental comparisons show that ApproxMC reports, with high confidence, bounds that are close to the exact count, and also succeeds in reporting bounds with small tolerance and high confidence in cases that are too large for computing exact model counts.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Generalizations of the Los-Tarski Preservation Theorem

We present new preservation theorems that semantically characterize the $\exists^k \forall^*$ and $\forall^k \exists^*$ prefix classes of first order logic, for each natural number $k$. Unlike preservation theorems in the literature that characterize the $\exists^* \forall^*$ and $\forall^* \exists^*$ prefix classes, our theorems relate the count of quantifiers in the leading block of the quantifier prefix to natural quantitative properties of the models. As special cases of our results, we obtain the classical Los-Tarski preservation theorem for sentences in both its extensional and substructural versions. For arbitrary finite vocabularies, we also generalize the extensional version of the Los-Tarski preservation theorem for theories. We also present an interpolant-based approach towards these results. Finally, we present partial results towards generalizing to theories, the substructural version of the Los-Tarski theorem and in the process, we give a preservation theorem that provides a semantic characterization of $Σ^0_n$ theories for each natural number $n$.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

Preservation under Substructures modulo Bounded Cores

We investigate a model-theoretic property that generalizes the classical notion of "preservation under substructures". We call this property \emph{preservation under substructures modulo bounded cores}, and present a syntactic characterization via $Σ_2^0$ sentences for properties of arbitrary structures definable by FO sentences. As a sharper characterization, we further show that the count of existential quantifiers in the $Σ_2^0$ sentence equals the size of the smallest bounded core. We also present our results on the sharper characterization for special fragments of FO and also over special classes of structures. We present a (not FO-definable) class of finite structures for which the sharper characterization fails, but for which the classical Łoś-Tarski preservation theorem holds. As a fallout of our studies, we obtain combinatorial proofs of the Łoś-Tarski theorem for some of the aforementioned cases.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Determinization of $ω$-automata unified

We describe a uniform construction for converting $ω$-automata with arbitrary acceptance conditions (based on the notion of infinity sets i.e. the set of states visited infinitely often in a run of the automaton) to equivalent deterministic parity automata (DPW). Given a non-deterministic automaton with $n$ states, our construction gives a DPW with at most $2^{O(n^2 \log n)}$ states and $O(n^2)$ parity indices. The corresponding bounds when the original automaton is deterministic are O(n!) and O(n), respectively. Our algorithm gives better asymptotic bounds on the number of states and parity indices vis-a-vis the best known technique when determinizing Rabin or Streett automata with $Ω{(2^n)}$ acceptance pairs, where $n > 1$. We demonstrate this by describing a family of Streett (and Rabin) automata with $2^{n}$ non-redundant acceptance pairs, for which the best known determinization technique gives a DPW with at least $Ω{(2^{(n^3)})}$ states, while our construction constructs a DRW/DPW with $2^{O(n^2\log n)}$ states. An easy corollary of our construction is that an $ω$-language with Rabin index $k$ cannot be recognized by any $ω$-automaton (deterministic or non-deterministic) with fewer than $O(\sqrt{k})$ states.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

On Semantic Generalizations of the Bernays-Schönfinkel-Ramsey Class with Finite or Co-finite Spectra

Motivated by model-theoretic properties of the BSR class, we present a family of semantic classes of FO formulae with finite or co-finite spectra over a relational vocabulary Σ. A class in this family is denoted EBS_Σ(σ), where σis a subset of Σ. Formulae in EBS_Σ(σ) are preserved under substructures modulo a bounded core and modulo re-interpretation of predicates outside σ. We study properties of the family EBS_Σ= {EBS_Σ(σ) | σ\subseteq Σ}, e.g. classes in EBS_Σare spectrally indistinguishable, EBS_Σ(Σ) is semantically equivalent to BSR over Σ, and EBS_Σ(\emptyset) is the set of all FO formulae over Σwith finite or co-finite spectra. Furthermore, (EBS_Σ, \subseteq) forms a lattice isomorphic to the powerset lattice (\wp(Σ), \subseteq). This gives a natural semantic generalization of BSR as ascending chains in (EBS_Σ, \subseteq). Many well-known FO classes are semantically subsumed by EBS_Σ(Σ) or EBS_Σ(\emptyset). Our study provides alternative proofs of interesting results like the Loś-Tarski Theorem and the semantic subsumption of the Löwenheim class with equality by BSR. We also present a syntactic sub-class of EBS_Σ(σ) called EDP_Σ(σ) and give an expression for the size of the bounded cores of models of EDP_Σ(σ) formulae. We show that the EDP_Σ(σ) classes also form a lattice structure. Finally, we study some closure properties and applications of the classes presented.

0 citations0 reviewsNo code linkedOpen access