-
Minsum Problem for Discrete and Weighted Set Flow on Dynamic Path Network
Authors:
Bubai Manna,
Bodhayan Roy,
Vorapong Suppakitpaisarn
Abstract:
In this research, we examine the minsum flow problem in dynamic path networks where flows are represented as discrete and weighted sets. The minsum flow problem has been widely studied for its relevance in finding evacuation routes during emergencies such as earthquakes. However, previous approaches often assume that individuals are separable and identical, which does not adequately account for th…
▽ More
In this research, we examine the minsum flow problem in dynamic path networks where flows are represented as discrete and weighted sets. The minsum flow problem has been widely studied for its relevance in finding evacuation routes during emergencies such as earthquakes. However, previous approaches often assume that individuals are separable and identical, which does not adequately account for the fact that some groups of people, such as families, need to move together and that some groups may be more important than others. To address these limitations, we modify the minsum flow problem to support flows represented as discrete and weighted sets. We also propose a 2-approximation pseudo-polynomial time algorithm to solve this modified problem for path networks with uniform capacity.
△ Less
Submitted 2 July, 2024;
originally announced July 2024.
-
Minimum Strict Consistent Subset in Paths, Spiders, Combs and Trees
Authors:
Bubai Manna
Abstract:
Let G be a simple connected graph with vertex set V(G) and edge set E(G. Each vertex of V(G) is colored by a color from the set of colors {c_1, c_2,\dots, c_α}. We take a subset S of V(G), such that for every vertex v in V(G)§, at least one vertex of the same color is present in its set of nearest neighbors in S. We refer to such an S as a consistent subset (CS). The Minimum Consistent Subset (MCS…
▽ More
Let G be a simple connected graph with vertex set V(G) and edge set E(G. Each vertex of V(G) is colored by a color from the set of colors {c_1, c_2,\dots, c_α}. We take a subset S of V(G), such that for every vertex v in V(G)§, at least one vertex of the same color is present in its set of nearest neighbors in S. We refer to such an S as a consistent subset (CS). The Minimum Consistent Subset (MCS) problem is the computation of a consistent subset of the minimum cardinality. It is established that MCS is NP-complete for general graphs, including planar graphs. The strict consistent subset is a variant of consistent subset problems. We take a subset S^{\prime} of V(G), such that for every vertex v in V(G)§^{\prime}, all the vertices in its set of nearest neighbors in S^{\prime} have the same color as that of v. We refer to such an S^{\prime} as a strict consistent subset (SCS). The Minimum Strict Consistent Subset (MSCS) problem is the computation of a strict consistent subset of the minimum cardinality.
We demonstrate that MSCS is NP-hard for general graphs using a reduction from dominating set problems. We construct a 2-approximation algorithm and a polynomial-time algorithm in trees. Lastly, we conclude the faster polynomial-time algorithms in paths, spiders, and combs.
△ Less
Submitted 5 July, 2024; v1 submitted 28 May, 2024;
originally announced May 2024.
-
Minimum Consistent Subset in Interval Graphs and Circle Graphs
Authors:
Bubai Manna
Abstract:
In a connected simple graph G = (V,E), each vertex of V is colored by a color from the set of colors C={c1, c2,..., c_α}$. We take a subset S of V, such that for every vertex v in V§, at least one vertex of the same color is present in its set of nearest neighbors in S. We refer to such a S as a consistent subset. The Minimum Consistent Subset (MCS) problem is the computation of a consistent subse…
▽ More
In a connected simple graph G = (V,E), each vertex of V is colored by a color from the set of colors C={c1, c2,..., c_α}$. We take a subset S of V, such that for every vertex v in V§, at least one vertex of the same color is present in its set of nearest neighbors in S. We refer to such a S as a consistent subset. The Minimum Consistent Subset (MCS) problem is the computation of a consistent subset of the minimum size. It is established that MCS is NP-complete for general graphs, including planar graphs. We expand our study to interval graphs and circle graphs in an attempt to gain a complete understanding of the computational complexity of the \mcs problem across various graph classes.
This work introduces an (4α+ 2)- approximation algorithm for MCS in interval graphs where αis the number of colors in the interval graphs. Later, we show that in circle graphs, MCS is APX-hard.
△ Less
Submitted 23 May, 2024;
originally announced May 2024.
-
On Approximating the Dynamic and Discrete Network Flow Problem
Authors:
Bubai Manna,
Bodhayan Roy,
Vorapong Suppakitpaisarn
Abstract:
We examine the dynamic network flow problem under the assumption that the flow consists of discrete units. The dynamic network flow problem is commonly addressed in the context of developing evacuation plans, where the flow is typically treated as a continuous quantity. However, real-world scenarios often involve moving groups, such as families, as single units. We demonstrate that solving the dyn…
▽ More
We examine the dynamic network flow problem under the assumption that the flow consists of discrete units. The dynamic network flow problem is commonly addressed in the context of developing evacuation plans, where the flow is typically treated as a continuous quantity. However, real-world scenarios often involve moving groups, such as families, as single units. We demonstrate that solving the dynamic flow problem with this consideration is APX-hard. Conversely, we present a PTAS for instances where the base graph is a path with a constant number of nodes. We introduce a `ready time' constraint to the minsum bin packing problem, meaning certain items cannot be placed in specific bins, develop a PTAS for this modified problem, and apply our algorithms to the discrete and dynamic flow problem.
△ Less
Submitted 25 April, 2024;
originally announced April 2024.
-
Minimum Consistent Subset in Trees and Interval Graphs
Authors:
Aritra Banik,
Sayani Das,
Anil Maheshwari,
Bubai Manna,
Subhas C Nandy,
Krishna Priya K M,
Bodhayan Roy,
Sasanka Roy,
Abhishek Sahu
Abstract:
In the Minimum Consistent Subset (MCS) problem, we are presented with a connected simple undirected graph $G=(V,E)$, consisting of a vertex set $V$ of size $n$ and an edge set $E$. Each vertex in $V$ is assigned a color from the set $\{1,2,\ldots, c\}$. The objective is to determine a subset $V' \subseteq V$ with minimum possible cardinality, such that for every vertex $v \in V$, at least one of i…
▽ More
In the Minimum Consistent Subset (MCS) problem, we are presented with a connected simple undirected graph $G=(V,E)$, consisting of a vertex set $V$ of size $n$ and an edge set $E$. Each vertex in $V$ is assigned a color from the set $\{1,2,\ldots, c\}$. The objective is to determine a subset $V' \subseteq V$ with minimum possible cardinality, such that for every vertex $v \in V$, at least one of its nearest neighbors in $V'$ (measured in terms of the hop distance) shares the same color as $v$. The decision problem, indicating whether there exists a subset $V'$ of cardinality at most $l$ for some positive integer $l$, is known to be NP-complete even for planar graphs.
In this paper, we establish that the MCS problem for trees, when the number of colors $c$ is considered an input parameter, is NP-complete. We propose a fixed-parameter tractable (FPT) algorithm for MCS on trees running in $O(2^{6c}n^6)$ time, significantly improving the currently best-known algorithm whose running time is $O(2^{4c}n^{2c+3})$.
In an effort to comprehensively understand the computational complexity of the MCS problem across different graph classes, we extend our investigation to interval graphs. We show that it remains NP-complete for interval graphs, thus enriching graph classes where MCS remains intractable.
△ Less
Submitted 23 April, 2024;
originally announced April 2024.
-
Variation-Resilient FeFET-Based In-Memory Computing Leveraging Probabilistic Deep Learning
Authors:
Bibhas Manna,
Arnob Saha,
Zhouhang Jiang,
Kai Ni,
Abhronil Sengupta
Abstract:
Reliability issues stemming from device level non-idealities of non-volatile emerging technologies like ferroelectric field-effect transistors (FeFET), especially at scaled dimensions, cause substantial degradation in the accuracy of In-Memory crossbar-based AI systems. In this work, we present a variation-aware design technique to characterize the device level variations and to mitigate their imp…
▽ More
Reliability issues stemming from device level non-idealities of non-volatile emerging technologies like ferroelectric field-effect transistors (FeFET), especially at scaled dimensions, cause substantial degradation in the accuracy of In-Memory crossbar-based AI systems. In this work, we present a variation-aware design technique to characterize the device level variations and to mitigate their impact on hardware accuracy employing a Bayesian Neural Network (BNN) approach. An effective conductance variation model is derived from the experimental measurements of cycle-to-cycle (C2C) and device-to-device (D2D) variations performed on FeFET devices fabricated using 28 nm high-$k$ metal gate technology. The variations were found to be a function of different conductance states within the given programming range, which sharply contrasts earlier efforts where a fixed variation dispersion was considered for all conductance values. Such variation characteristics formulated for three different device sizes at different read voltages were provided as prior variation information to the BNN to yield a more exact and reliable inference. Near-ideal accuracy for shallow networks (MLP5 and LeNet models) on the MNIST dataset and limited accuracy decline by $\sim$3.8-16.1% for deeper AlexNet models on CIFAR10 dataset under a wide range of variations corresponding to different device sizes and read voltages, demonstrates the efficacy of our proposed device-algorithm co-design technique.
△ Less
Submitted 13 March, 2024; v1 submitted 24 December, 2023;
originally announced December 2023.
-
Some results on Minimum Consistent Subsets of Trees
Authors:
Bubai Manna,
Bodhayan Roy
Abstract:
For a graph G = (V,E) where each vertex is coloured by one of k colours, consider a subset C of V such that for each vertex v in V\C, its set of nearest neighbours in C contains at least one vertex of the same colour as v. Such a C is called a consistent subset (CS). Computing a consistent subset of the minimum size is called the Minimum Consistent Subset problem (MCS). MCS is known to be NP-compl…
▽ More
For a graph G = (V,E) where each vertex is coloured by one of k colours, consider a subset C of V such that for each vertex v in V\C, its set of nearest neighbours in C contains at least one vertex of the same colour as v. Such a C is called a consistent subset (CS). Computing a consistent subset of the minimum size is called the Minimum Consistent Subset problem (MCS). MCS is known to be NP-complete for planar graphs. We propose a polynomial-time algorithm for finding a minimum consistent subset of a k-chromatic spider graph when k is a constant. We also show MCS remains NP-complete on trees.
△ Less
Submitted 30 May, 2023; v1 submitted 4 March, 2023;
originally announced March 2023.
-
Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory
Authors:
Bassel Mannaa,
Rasmus Ejlers Møgelberg,
Niccolò Veltri
Abstract:
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to enjoy a number of syntactic properties including strong normalisation, canonicity and decidability of…
▽ More
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to enjoy a number of syntactic properties including strong normalisation, canonicity and decidability of the equational theory. In this paper we present a denotational semantics for CloTT useful, e.g., for studying future extensions of CloTT with constructions such as path types.
The main challenge for constructing this model is to model the notion of ticks on a clock used in CloTT for coinductive reasoning about coinductive types. We build on a category previously used to model guarded recursion with multiple clocks. In this category there is an object of clocks but no object of ticks, and so tick-assumptions in a context can not be modelled using standard tools. Instead we model ticks using dependent right adjoint functors, a generalisation of the category theoretic notion of adjunction to the setting of categories with families. Dependent right adjoints are known to model Fitch-style modal types, but in the case of CloTT, the modal operators constitute a family indexed internally in the type theory by clocks. We model this family using a dependent right adjoint on the slice category over the object of clocks. Finally we show how to model the tick constant of CloTT using a semantic substitution.
This work improves on a previous model by the first two named authors which not only had a flaw but was also considerably more complicated.
△ Less
Submitted 14 December, 2020; v1 submitted 3 April, 2020;
originally announced April 2020.
-
The clocks they are adjunctions:Denotational semantics for Clocked Type Theory
Authors:
Bassel Mannaa,
Rasmus Ejlers Møgelberg
Abstract:
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to enjoy a number of syntactic properties including strong normalisation, canonicity and decidability of…
▽ More
Clocked Type Theory (CloTT) is a type theory for guarded recursion useful for programming with coinductive types, allowing productivity to be encoded in types, and for reasoning about advanced programming language features using an abstract form of step-indexing. CloTT has previously been shown to enjoy a number of syntactic properties including strong normalisation, canonicity and decidability of type checking. In this paper we present a denotational semantics for CloTT useful, e.g., for studying future extensions of CloTT with constructions such as path types.
The main challenge for constructing this model is to model the notion of ticks used in CloTT for coinductive reasoning about coinductive types. We build on a category previously used to model guarded recursion, but in this category there is no object of ticks, so tick-assumptions in a context can not be modelled using standard tools. Instead we show how ticks can be modelled using adjoint functors, and how to model the tick constant using a semantic substitution.
△ Less
Submitted 18 April, 2018;
originally announced April 2018.
-
Modal Dependent Type Theory and Dependent Right Adjoints
Authors:
Lars Birkedal,
Ranald Clouston,
Bassel Mannaa,
Rasmus Ejlers Møgelberg,
Andrew M. Pitts,
Bas Spitters
Abstract:
In recent years we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked type theory, and spatial and cohesive type theory. In this paper we study modal dependent type theory: dependent type theory with an operator satisfying (a dependent version of) the K-axiom of modal logic. We investigate bo…
▽ More
In recent years we have seen several new models of dependent type theory extended with some form of modal necessity operator, including nominal type theory, guarded and clocked type theory, and spatial and cohesive type theory. In this paper we study modal dependent type theory: dependent type theory with an operator satisfying (a dependent version of) the K-axiom of modal logic. We investigate both semantics and syntax. For the semantics, we introduce categories with families with a dependent right adjoint (CwDRA) and show that the examples above can be presented as such. Indeed, we show that any finite limit category with an adjunction of endofunctors gives rise to a CwDRA via the local universe construction. For the syntax, we introduce a dependently typed extension of Fitch-style modal lambda-calculus, show that it can be interpreted in any CwDRA, and build a term model. We extend the syntax and semantics with universes.
△ Less
Submitted 25 July, 2019; v1 submitted 14 April, 2018;
originally announced April 2018.
-
Stack Semantics of Type Theory
Authors:
Thierry Coquand,
Bassel Mannaa,
Fabian Ruch
Abstract:
We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalising the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.
We give a model of dependent type theory with one univalent universe and propositional truncation interpreting a type as a stack, generalising the groupoid model of type theory. As an application, we show that countable choice cannot be proved in dependent type theory with one univalent universe and propositional truncation.
△ Less
Submitted 19 April, 2017; v1 submitted 10 January, 2017;
originally announced January 2017.
-
The Independence of Markov's Principle in Type Theory
Authors:
Thierry Coquand,
Bassel Mannaa
Abstract:
In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One way to prove this would be to remark that Markov's principle does not hold in a sheaf model of type theory over Cantor space, since Markov's principle does not hold for the generic point of this model. Instead we design an extension of type theory, which intuitively e…
▽ More
In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One way to prove this would be to remark that Markov's principle does not hold in a sheaf model of type theory over Cantor space, since Markov's principle does not hold for the generic point of this model. Instead we design an extension of type theory, which intuitively extends type theory by the addition of a generic point of Cantor space. We then show the consistency of this extension by a normalization argument. Markov's principle does not hold in this extension, and it follows that it cannot be proved in type theory.
△ Less
Submitted 14 August, 2017; v1 submitted 14 February, 2016;
originally announced February 2016.
-
High Sensitivity Biosensor using Injection Locked Spin Torque Nano-Oscillators
Authors:
Tathagata Srimani,
Bibhas Manna,
Anand Kumar Mukhopadhyay,
Kaushik Roy,
Mrigank Sharad
Abstract:
With ever increasing research on magnetic nano systems it is shown to have great potential in the areas of magnetic storage, biosensing, magnetoresistive insulation etc. In the field of biosensing specifically Spin Valve sensors coupled with Magnetic Nanolabels is showing great promise due to noise immunity and energy efficiency [1]. In this paper we present the application of injection locked bas…
▽ More
With ever increasing research on magnetic nano systems it is shown to have great potential in the areas of magnetic storage, biosensing, magnetoresistive insulation etc. In the field of biosensing specifically Spin Valve sensors coupled with Magnetic Nanolabels is showing great promise due to noise immunity and energy efficiency [1]. In this paper we present the application of injection locked based Spin Torque Nano Oscillator (STNO) suitable for high resolution energy efficient labeled DNA Detection. The proposed STNO microarray consists of 20 such devices oscillating at different frequencies making it possible to multiplex all the signals using capacitive coupling. Frequency Division Multiplexing can be aided with Time division multiplexing to increase the device integration and decrease the readout time while maintaining the same efficiency in presence of constant input referred noise.
△ Less
Submitted 29 November, 2015;
originally announced November 2015.
