More Like this

1. Constraint Optimization over Semirings

   A. Pavan ; Kuldeep S Meel ; N. V. Vinodchandranl Arnab Bhattacharyya ( February 2023 , Proceedings of the AAAI Conference on Artificial Intelligence)

   Williams Brian ; Chen Yiling ; Neville Jennifer (Ed.)

   Interpretations of logical formulas over semirings (other than the Boolean semiring) have applications in various areas of computer science including logic, AI, databases, and security. Such interpretations provide richer information beyond the truth or falsity of a statement. Examples of such semirings include Viterbi semiring, min-max or access control semiring, tropical semiring, and fuzzy semiring. The present work investigates the complexity of constraint optimization problems over semirings. The generic optimization problem we study is the following: Given a propositional formula $\varphi$ over $n$ variable and a semiring $(K,+,\cdot,0,1)$, find the maximum value over all possible interpretations of $\varphi$ over $K$. This can be seen as a generalization of the well-known satisfiability problem (a propositional formula is satisfiable if and only if the maximum value over all interpretations/assignments over the Boolean semiring is 1). A related problem is to find an interpretation that achieves the maximum value. In this work, we first focus on these optimization problems over the Viterbi semiring, which we call \optrustval\ and \optrust. We first show that for general propositional formulas in negation normal form, \optrustval\ and {\optrust} are in ${\mathrm{FP}}^{\mathrm{NP}}$. We then investigate {\optrust} when the input formula $\varphi$ is represented in the conjunctive normal form. For CNF formulae, we first derive an upper bound on the value of {\optrust} as a function of the number of maximum satisfiable clauses. In particular, we show that if $r$ is the maximum number of satisfiable clauses in a CNF formula with $m$ clauses, then its $\optrust$ value is at most $1/4^{m-r}$. Building on this we establish that {\optrust} for CNF formulae is hard for the complexity class ${\mathrm{FP}}^{\mathrm{NP}[\log]}$. We also design polynomial-time approximation algorithms and establish an inapproximability for {\optrustval}. We establish similar complexity results for these optimization problems over other semirings including tropical, fuzzy, and access control semirings. 

   more » « less
2. Semiring Provenance for Fixed-Point Logic

   https://doi.org/10.4230/LIPIcs.CSL.2021.17  

   Dannert, K ; Graedel, E ; Naaf, N ; Tannen, V ( January 2021 , Conference on Computer Science Logic, CSL 2021,)

   null (Ed.)

   Semiring provenance is a successful approach, originating in database theory, to providing detailed information on how atomic facts combine to yield the result of a query. In particular, general provenance semirings of polynomials or formal power series provide precise descriptions of the evaluation strategies or “proof trees” for the query. By evaluating these descriptions in specific application semirings, one can extract practical information for instance about the confidence of a query or the cost of its evaluation. This paper develops semiring provenance for very general logical languages featuring the full interaction between negation and fixed-point inductions or, equivalently, arbitrary interleavings of least and greatest fixed points. This also opens the door to provenance analysis applications for modal μ-calculus and temporal logics, as well as for finite and infinite model-checking games. Interestingly, the common approach based on Kleene’s Fixed-Point Theorem for ω-continuous semirings is not sufficient for these general languages. We show that an adequate framework for the provenance analysis of full fixed-point logics is provided by semirings that are (1) fully continuous, and (2) absorptive. Full continuity guarantees that provenance values of least and greatest fixed-points are well-defined. Absorptive semirings provide a symmetry between least and greatest fixed-points and make sure that provenance values of greatest fixed points are informative. We identify semirings of generalized absorptive polynomials S∞[X] and prove universal properties that make them the most general appropriate semirings for our framework. These semirings have the further property of being (3) chain-positive, which is responsible for having truth-preserving interpretations that give non-zero values to all true formulae. We relate the provenance analysis of fixed-point formulae with provenance values of plays and strategies in the associated model-checking games. Specifically, we prove that the provenance value of a fixed point formula gives precise information on the evaluation strategies in these games. 

   more » « less
3. Estimating the Density of States of Boolean Satisfiability Problems on Classical and Quantum Computing Platforms

   https://doi.org/10.1609/aaai.v34i02.5524  

   Sahai, Tuhin ; Mishra, Anurag ; Pasini, Jose Miguel ; Jha, Susmit ( June 2020 , Proceedings of the AAAI Conference on Artificial Intelligence)

   Given a Boolean formula ϕ(x) in conjunctive normal form (CNF), the density of states counts the number of variable assignments that violate exactly e clauses, for all values of e. Thus, the density of states is a histogram of the number of unsatisfied clauses over all possible assignments. This computation generalizes both maximum-satisfiability (MAX-SAT) and model counting problems and not only provides insight into the entire solution space, but also yields a measure for the hardness of the problem instance. Consequently, in real-world scenarios, this problem is typically infeasible even when using state-of-the-art algorithms. While finding an exact answer to this problem is a computationally intensive task, we propose a novel approach for estimating density of states based on the concentration of measure inequalities. The methodology results in a quadratic unconstrained binary optimization (QUBO), which is particularly amenable to quantum annealing-based solutions. We present the overall approach and compare results from the D-Wave quantum annealer against the best-known classical algorithms such as the Hamze-de Freitas-Selby (HFS) algorithm and satisfiability modulo theory (SMT) solvers. 

   more » « less
4. Lifting with simple gadgets and applications to circuit and proof complexity

   Meir, O ; Nördstrom, J ; Pitassi, T ; Robere, R ; de Rezende, Susanna F ; Vinyals, M. ( February 2020 , Electronic colloquium on computational complexity)

   We significantly strengthen and generalize the theorem lifting Nullstellensatz degree to monotone span program size by Pitassi and Robere (2018) so that it works for any gadget with high enough rank, in particular, for useful gadgets such as equality and greater-than. We apply our generalized theorem to solve two open problems: • We present the first result that demonstrates a separation in proof power for cutting planes with unbounded versus polynomially bounded coefficients. Specifically, we exhibit CNF formulas that can be refuted in quadratic length and constant line space in cutting planes with unbounded coefficients, but for which there are no refutations in subexponential length and subpolynomial line space if coefficients are restricted to be of polynomial magnitude. • We give the first explicit separation between monotone Boolean formulas and monotone real formulas. Specifically, we give an explicit family of functions that can be computed with monotone real formulas of nearly linear size but require monotone Boolean formulas of exponential size. Previously only a non-explicit separation was known. An important technical ingredient, which may be of independent interest, is that we show that the Nullstellensatz degree of refuting the pebbling formula over a DAG G over any field coincides exactly with the reversible pebbling price of G. In particular, this implies that the standard decision tree complexity and the parity decision tree complexity of the corresponding falsified clause search problem are equal. 

   more » « less
5. Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse

   https://doi.org/10.29007/2s1q  

   Jiang, Chuan ; Ciardo, Gianfranco ( January 2018 , EPiC Series in Computing)

   A complementary technique to decision-diagram-based model checking is SAT-based bounded model checking (BMC), which reduces the model checking problem to a propositional satisfiability problem so that the corresponding formula is satisfiable iff a counterexample or witness exists. Due to the branching time nature of computation tree logic (CTL), BMC for the universal fragment of CTL (ACTL) considers a counterexample in a bounded model as a set of bounded paths. Since the existential fragment of CTL (ECTL) is dual to ACTL, and ACTL formulas are often negated to obtain ECTL ones in practice, we focus on BMC for ECTL and propose an improved translation that generates a possibly smaller propositional formula by reducing the number of bounded paths to be considered in a witness. Experimental results show that the formulas generated by our approach are often easier for a SAT solver to answer. In addition, we propose a simple modification to the translation so that it is also defined for models with deadlock states. 

   more » « less