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, minmax 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 phi over n variable and a semiring (K,+, . ,0,1), find the maximum value over all possible interpretations of phi over K. This can be seen as a generalization of the wellknown 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 optConfVal and optConf. We first show that for general propositional formulas in negation normal form, optConfVal and optConf are in FP^NP. We then investigate optConf when the input formula phi is represented in the conjunctive normal form. For CNF formulae, we first derive an upper bound on the value of optConf 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 optConf value is at most 1/4^(mr). Building on this we establish that optConf for CNF formulae is hard for the complexity class FP^NP[log]. We also design polynomialtime approximation algorithms and establish an inapproximability for optConfVal. We establish similar complexity results for these optimization problems over other semirings including tropical, fuzzy, and access control semirings.
more »
« less
Estimating the Density of States of Boolean Satisfiability Problems on Classical and Quantum Computing Platforms
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 maximumsatisfiability (MAXSAT) 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 realworld scenarios, this problem is typically infeasible even when using stateoftheart 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 annealingbased solutions. We present the overall approach and compare results from the DWave quantum annealer against the bestknown classical algorithms such as the Hamzede FreitasSelby (HFS) algorithm and satisfiability modulo theory (SMT) solvers.
more »
« less
 NSFPAR ID:
 10181036
 Date Published:
 Journal Name:
 Proceedings of the AAAI Conference on Artificial Intelligence
 Volume:
 34
 Issue:
 02
 ISSN:
 21595399
 Page Range / eLocation ID:
 1627 to 1635
 Format(s):
 Medium: X
 Sponsoring Org:
 National Science Foundation
More Like this


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, minmax 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 wellknown 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^{mr}$. Building on this we establish that {\optrust} for CNF formulae is hard for the complexity class ${\mathrm{FP}}^{\mathrm{NP}[\log]}$. We also design polynomialtime 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

We describe an algorithm to solve the problem of Boolean CNFSatisfiability when the input formula is chosen randomly. We build upon the algorithms of Schöning 1999 and Dantsin et al. in 2002. The Schöning algorithm works by trying many possible random assignments, and for each one searching systematically in the neighborhood of that assignment for a satisfying solution. Previous algorithms for this problem run in time O(2^(n (1 Ω(1)/k))). Our improvement is simple: we count how many clauses are satisfied by each randomly sampled assignment, and only search in the neighborhoods of assignments with abnormally many satisfied clauses. We show that assignments like these are significantly more likely to be near a satisfying assignment. This improvement saves a factor of 2^(n Ω(lg² k)/k), resulting in an overall runtime of O(2^(n (1 Ω(lg² k)/k))) for random kSAT.more » « less

The constraint satisfaction problems kSAT and Quantum kSAT (kQSAT) are canonical NPcomplete and QMA_1complete problems (for k >= 3), respectively, where QMA_1 is a quantum generalization of NP with onesided error. Whereas kSAT has been wellstudied for special tractable cases, as well as from a parameterized complexity perspective, much less is known in similar settings for kQSAT. Here, we study the open problem of computing satisfying assignments to kQSAT instances which have a "matching" or "dimer covering"; this is an NP problem whose decision variant is trivial, but whose search complexity remains open. Our results fall into three directions, all of which relate to the "matching" setting: (1) We give a polynomialtime classical algorithm for kQSAT when all qubits occur in at most two clauses. (2) We give a parameterized algorithm for kQSAT instances from a certain nontrivial class, which allows us to obtain exponential speedups over brute force methods in some cases by reducing the problem to solving for a single root of a single univariate polynomial. (3) We conduct a structural graph theoretic study of 3QSAT interaction graphs which have a "matching". We remark that the results of (2), in particular, introduce a number of new tools to the study of Quantum SAT, including graph theoretic concepts such as transfer filtrations and blowups from algebraic geometry; we hope these prove useful elsewhere.more » « less

The Boolean constraint satisfaction problem 3SAT is arguably the canonical NPcomplete problem. In contrast, 2SAT can not only be decided in polynomial time, but in fact in deterministic linear time. In 2006, Bravyi proposed a physically motivated generalization of kSAT to the quantum setting, defining the problem "quantum kSAT". He showed that quantum 2SAT is also solvable in polynomial time on a classical computer, in particular in deterministic time O(n^4), assuming unitcost arithmetic over a field extension of the rational numbers, where n is number of variables. In this paper, we present an algorithm for quantum 2SAT which runs in linear time, i.e. deterministic time O(n+m) for n and m the number of variables and clauses, respectively. Our approach exploits the transfer matrix techniques of Laumann et al. [QIC, 2010] used in the study of phase transitions for random quantum 2SAT, and bears similarities with both the linear time 2SAT algorithms of Even, Itai, and Shamir (based on backtracking) [SICOMP, 1976] and Aspvall, Plass, and Tarjan (based on strongly connected components) [IPL, 1979].more » « less