A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem

• URL: http://arxiv.org/abs/2306.13319v7
• Date: Tue, 9 Apr 2024 20:44:22 GMT
• Title: A SAT Solver and Computer Algebra Attack on the Minimum Kochen-Specker Problem
• Authors: Zhengyu Li, Curtis Bright, Vijay Ganesh,
• Abstract summary: We present a new verifiable proof-producing method based on a combination of a Boolean satisfiability solver and a computer algebra system. Our method shows that a KS system in 3D must contain at least 24 vectors. We also provide the first computer-verifiable proof certificate of a lower bound to the KS problem with a size of 40.3 TiB in order 23.
• Score: 14.693394941317843
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: One of the fundamental results in quantum foundations is the Kochen-Specker (KS) theorem, which states that any theory whose predictions agree with quantum mechanics must be contextual, i.e., a quantum observation cannot be understood as revealing a pre-existing value. The theorem hinges on the existence of a mathematical object called a KS vector system. While many KS vector systems are known, the problem of finding the minimum KS vector system in three dimensions (3D) has remained stubbornly open for over 55 years. To address the minimum KS problem, we present a new verifiable proof-producing method based on a combination of a Boolean satisfiability (SAT) solver and a computer algebra system (CAS) that uses an isomorph-free orderly generation technique that is very effective in pruning away large parts of the search space. Our method shows that a KS system in 3D must contain at least 24 vectors. We show that our sequential and parallel Cube-and-Conquer (CnC) SAT+CAS methods are significantly faster than SAT-only, CAS-only, and a prior CAS-based method of Uijlen and Westerbaan. Further, while our parallel pipeline is somewhat slower than the parallel CnC version of the recently introduced Satisfiability Modulo Theories (SMS) method, this is in part due to the overhead of proof generation. Finally, we provide the first computer-verifiable proof certificate of a lower bound to the KS problem with a size of 40.3 TiB in order 23.

Related papers

• Heuristic Time Complexity of NISQ Shortest-Vector-Problem Solvers [0.0]
  Shortest Vector Problem is believed to be hard for classical and quantum computers. We show that it is plausible to encode SVP on the ground state of a Hamiltonian efficiently. We propose a novel method to avoid the zero vector solution to SVP without introducing more logical qubits.
  arXiv  Detail & Related papers  (2025-02-07T19:42:35Z)
• An unholy trinity: TFNP, polynomial systems, and the quantum satisfiability problem [0.0]
  We define two new subclasses of Total Function NP (TFNP) based on the study of complex systems. At the heart of our study is the computational problem known as Quantum SAT with a System of Distinct Representatives (SDR) We show how to embed the roots of a sparse, high-degree complexity into QSAT with SDR, obtaining that SFTA is contained in a zero-error version of SDR.
  arXiv  Detail & Related papers  (2024-12-27T12:57:06Z)
• Unifying (Quantum) Statistical and Parametrized (Quantum) Algorithms [65.268245109828]
  We take inspiration from Kearns' SQ oracle and Valiant's weak evaluation oracle. We introduce an extensive yet intuitive framework that yields unconditional lower bounds for learning from evaluation queries.
  arXiv  Detail & Related papers  (2023-10-26T18:23:21Z)
• Quantum Bayesian Optimization [64.58749619145908]
  We introduce the quantum-Gaussian process-upper confidence bound (Q-GP-UCB) algorithm. It is the first BO algorithm able to achieve a regret upper bound of O(polylog T), which is significantly smaller than its regret lower bound of Omega(sqrt(T)) in the classical setting. Thanks to our novel analysis of the confidence ellipsoid, our Q-GP-UCB with the linear kernel achieves a smaller regret than the quantum linear UCB algorithm.
  arXiv  Detail & Related papers  (2023-10-09T03:10:42Z)
• A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
  This paper presents and describes a hybrid quantum computing strategy for solving 3-SAT problems. The performance of this approximation has been tested over a set of representative scenarios when dealing with 3-SAT from the quantum computing perspective.
  arXiv  Detail & Related papers  (2023-06-07T12:19:22Z)
• Simple Tests of Quantumness Also Certify Qubits [69.96668065491183]
  A test of quantumness is a protocol that allows a classical verifier to certify (only) that a prover is not classical. We show that tests of quantumness that follow a certain template, which captures recent proposals such as (Kalai et al., 2022) can in fact do much more. Namely, the same protocols can be used for certifying a qubit, a building-block that stands at the heart of applications such as certifiable randomness and classical delegation of quantum computation.
  arXiv  Detail & Related papers  (2023-03-02T14:18:17Z)
• Quantum Worst-Case to Average-Case Reductions for All Linear Problems [66.65497337069792]
  We study the problem of designing worst-case to average-case reductions for quantum algorithms. We provide an explicit and efficient transformation of quantum algorithms that are only correct on a small fraction of their inputs into ones that are correct on all inputs.
  arXiv  Detail & Related papers  (2022-12-06T22:01:49Z)
• Complexity-Theoretic Limitations on Quantum Algorithms for Topological Data Analysis [59.545114016224254]
  Quantum algorithms for topological data analysis seem to provide an exponential advantage over the best classical approach. We show that the central task of TDA -- estimating Betti numbers -- is intractable even for quantum computers. We argue that an exponential quantum advantage can be recovered if the input data is given as a specification of simplices.
  arXiv  Detail & Related papers  (2022-09-28T17:53:25Z)
• Quantum space, ground space traversal, and how to embed multi-prover interactive proofs into unentanglement [0.0]
  Savitch's theorem states that NPSPACE computations can be simulated in PSPACE. We show that a quantum analogue of Savitch's theorem is unlikely to hold, as SQCMASPACE=NEXP. We show how to embed SQCMASPACE into the Sparse Separable Hamiltonian problem of [Chailloux, Sattath, 2012] (QMA(2)-complete for 1/poly promise gap)
  arXiv  Detail & Related papers  (2022-06-10T17:35:10Z)
• Contextuality in composite systems: the role of entanglement in the Kochen-Specker theorem [0.0]
  The Kochen--Specker (KS) theorem reveals the nonclassicality of single quantum systems. Bell's theorem and entanglement concern the nonclassicality of composite quantum systems.
  arXiv  Detail & Related papers  (2021-09-28T10:10:53Z)
• Simpler Proofs of Quantumness [16.12500804569801]
  A proof of quantumness is a method for provably demonstrating that a quantum device can perform computational tasks that a classical device cannot. There are currently three approaches for exhibiting proofs of quantumness. We give a two-message (challenge-response) proof of quantumness based on any trapdoor claw-free function.
  arXiv  Detail & Related papers  (2020-05-11T01:31:18Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.