Solving SAT (and MaxSAT) with a quantum annealer: foundations, encodings, and preliminary results

DOI10.1016/j.ic.2020.104609zbMath1496.68298arXiv1811.02524OpenAlexW3046571544MaRDI QIDQ2216123

Stefano Varotti, Zhengbing Bian, Roberto Sebastiani, Fabián A. Chudak, Aidan Roy, William G. Macready

Publication date: 15 December 2020

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1811.02524

zbMATH Keywords

Ising modelSATquantum annealingMaxSATsatisfiability modulo theoriesquadratic unconstrained binary optimization (QUBO)optimization modulo theoriesChimera graph

Mathematics Subject Classification ID

Quantum computation (81P68) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (2)

Why adiabatic quantum annealing is unlikely to yield speed-up ⋮ Probabilistic nonunitary gate in imaginary time evolution

Uses Software

• MiniSat
• nauty
• UBCSAT
• Walksat
• Traces
• MathSAT
• ABC
• Capo
• OptiMathSAT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Fast clique minor generation in Chimera qubit connectivity graphs
• Faster min-max resource sharing in theory and practice
• Minor-embedding in adiabatic quantum computation. II: Minor-universal graph design
• Minor-embedding in adiabatic quantum computation. I: The parameter setting problem
• Systematic and deterministic graph minor embedding for Cartesian products of graphs
• Solving SAT and MaxSAT with a quantum annealer: foundations and a preliminary report
• Logical cryptanalysis as a SAT problem: Encoding and analysis of the U. S. Data Encryption Standard
• A case study in programming a quantum annealer for hard operational planning problems
• \textsc{OptiMathSAT}: a tool for optimization modulo theories
• Practical graph isomorphism. II.
• An improved LP-based approximation for steiner tree
• Optimization Modulo Theories with Linear Rational Costs
• Constructing SAT Filters with a Quantum Annealer
• Approximation algorithms for metric facility location and k -Median problems using the primal-dual schema and Lagrangian relaxation
• Faster Parameterized Algorithms for Minor Containment
• VLSI Physical Design: From Graph Partitioning to Timing Closure
• Applying Logic Synthesis for Speeding Up SAT
• Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer
• Performing fully parallel constraint logic programming on a quantum annealer
• A Nearly Best-Possible Approximation Algorithm for Node-Weighted Steiner Trees
• Zero-One Designs Produce Small Hard SAT Instances
• Applications of SAT Solvers in Cryptanalysis: Finding Weak Keys and Preimages
• Steiner Tree Approximation via Iterative Randomized Rounding
• sgen1
• The complexity of theorem-proving procedures
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Applications of SAT Solvers to Cryptanalysis of Hash Functions

This page was built for publication: Solving SAT (and MaxSAT) with a quantum annealer: foundations, encodings, and preliminary results