The logics \(\mathsf {CS4} \) and \(\mathsf {IS4} \) are the two leading intuitionistic variants of the modal logic \(\mathsf {S4} \) . Whether the finite model property holds for each of these logics have been long-standing open problems. In this paper, we resolve the first of these problems, proving that \(\mathsf {CS4} \) has the finite frame property. Additionally, we investigate the following three logics closely related to \(\mathsf {IS4} \) . The logic \(\mathsf {GS4} \) is obtained by adding the Gödel–Dummett axiom to \(\mathsf {IS4} \) ; it is both a superintuitionistic and a fuzzy logic and has previously been given a real-valued semantics. We provide an alternative birelational semantics and prove strong completeness with respect to this semantics. The extension \(\mathsf {GS4}^c \) of \(\mathsf {GS4} \) corresponds to requiring a crisp accessibility relation on the real-valued semantics. We give \(\mathsf {GS4}^c \) a birelational semantics corresponding to an extra confluence condition on the \(\mathsf {GS4} \) birelational semantics and prove strong completeness. Neither of these two logics have the finite model property with respect to their real-valued semantics, but we prove that they have the finite frame property with respect to their birelational semantics. Establishing the finite birelational frame property immediately establishes decidability, which was previously open for these two logics. Our proofs yield coNEXPTIME upper bounds for \(\mathsf {CS4} \) , \(\mathsf {GS4} \) , and \(\mathsf {GS4}^c \) . The logic \(\mathsf {S4I} \) is obtained from \(\mathsf {IS4} \) by reversing the roles of the modal and intuitionistic relations in the birelational semantics. We also prove the finite frame property, and thereby decidability, for \(\mathsf {S4I} \) , although our proof does not yield an elementary complexity bound. In summary, we prove that \(\mathsf {CS4} \) , \(\mathsf {GS4} \) , \(\mathsf {GS4}^c \) , and \(\mathsf {S4I} \) all have the finite birelational frame property, with the first three having a coNEXPTIME validity problem.
In traditional algorithm design, no incentives come into play: the input is given, and your algorithm must produce a correct output. How much harder is it to solve the same problem when the input is not given directly, but instead reported by strategic agents with interests of their own? The unique challenge stems from the fact that the agents may choose to lie about the input in order to manipulate the behavior of the algorithm for their own interests, and tools from Game Theory are, therefore, required in order to predict how these agents will behave. We develop a new algorithmic framework with which to study such problems. Specifically, we provide a computationally efficient black-box reduction from solving any Bayesian optimization problem on “strategic input,” often called algorithmic mechanism design , to solving a perturbed version of that same optimization problem when the input is directly given, traditionally called algorithm design . We further demonstrate the power of our framework by making significant progress on several long-standing open problems. First, we provide an algorithmic extension of Myerson’s celebrated characterization of single item auctions [ 105 ] to multiple items, providing also a computationally efficient implementation of optimal auctions. Next, we design a computationally efficient 2-approximate mechanism for Bayesian job scheduling on unrelated machines, the original problem studied in Nisan and Ronen’s seminal article introducing the field of Algorithmic Mechanism Design [ 106 ]. This matches the guarantee of the best known computationally efficient algorithm when the input is directly given. Finally, leveraging a connection to our framework, we additionally prove hardness of approximation for Bayesian mechanism design with submodular bidders.
In the classical survivable network design problem (SNDP), we are given an undirected graph G = (V, E) with costs on edges and a connectivity requirement k(s, t) for each pair of vertices. The goal is to find a minimum-cost subgraph H subset of G such that every pair (s, t) is connected by k(s, t) edge or (openly) vertex disjoint paths, abbreviated as EC-SNDP and VC-SNDP, respectively. The seminal result of Jain [FOCS'98, Combinatorica'01] gives a 2-approximation algorithm for EC-SNDP, and a decade later, an O(k(3) log n)-approximation algorithm for VC-SNDP, where k is the largest connectivity requirement, was discovered by Chuzhoy and Khanna [FOCS'09, Theory Comput.'12]. While there is a rich literature on point-to-point settings of SNDP, the viable case of connectivity between subsets is still relatively poorly understood. This article concerns the generalization of EC-SNDP into the subset-to-subset setting, namely Group EC-SNDP. We develop a framework, which yields the first non-trivial (true) approximation algorithm for Group EC-SNDP. Previously, only a bicriteria approximation algorithm is known for Group EC-SNDP [Chalermsook, Grandoni, and Laekhanukit, SODA'15], and a true approximation algorithm is known only for the single-source variant with connectivity requirement k(S, T) is an element of {0, 1, 2} [Gupta, Krishnaswamy, and Ravi, SODA'10; Khandekar, Kortsarz, and Nutov, FSTTCS'09 and Theor. Comput. Sci.'12]. On the negative side, in terms of the number of connectivity demands q, we give an Omega (q/log q)-hardness result for large k, complementing the previous inapproximability results, e.g., hardness in terms of k: k(1/5-epsilon)- hardness [Cheriyan et al., SODA'12; Laekhanukit, SODA'14; Chalermsook et al., SODA'15; Manurangsi, IPL'19]; hardness in terms of n: 2(log1-epsilon) (n)-hardness [Chalermsook et al., SODA'15].
We develop a quantitative analogue of equational reasoning, which we call quantitative equational logic. The quantitative equations use, instead of classical equality, quantitative equalities, which are equalities indexed with nonnegative reals. Thus, s = ε t means that “ s and t are points in a metric space and their distance is less than ε”. Quantitative equalities will be used to encode behavioural distances, with ε being an upper bound on the measure of dissimilarity between two terms. We develop the metatheory of this subject. We define a notion of quantitative algebra, which is the quantitative analogue of universal algebra. We prove a completeness theorem for quantitative equational logic, and we show that we obtain monads on suitable categories of metric spaces. We present a set of examples where the free algebra of a quantitative equational theory corresponds to some well-known structure. These examples are: Hausdorff metrics from quantitative semilattices; p -Wasserstein metrics (hence also the Kantorovich metric), and the total variation metric.
An important objective function in the scheduling literature is to minimize the sum of weighted flow times. We are given a set of jobs, where each job is characterized by a release time, a processing time, and a weight. Our goal is to find a preemptive schedule on a single machine that minimizes the sum of the weighted flow times of the jobs, where the flow time of a job is the time between its completion time and its release time. In their breakthrough result, Batra, Garg, and Kumar [FOCS 2018] found the first pseudopolynomial-time constant-factor approximation algorithm for the problem, which was turned into a polynomial-time algorithm by Feige, Kulkarni, and Li [SODA 2019]. The resulting approximation ratio is a (not explicitly stated) constant which is at least 10,000. In this article, we improve this to a PTAS. 1 The algorithm by Batra et al. reduces the problem to Demand MultiCut on trees and solves the resulting instances via LP-rounding and a dynamic program. Instead, we first reduce the problem to a (different) geometric problem while losing only a factor \(1 + \varepsilon\) , and then solve its resulting instances exactly by a dynamic program. In particular, our reduction ensures certain structural properties, due to which we do not need LP-rounding techniques.
