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
Ising modelSATquantum annealingMaxSATsatisfiability modulo theoriesquadratic unconstrained binary optimization (QUBO)optimization modulo theoriesChimera graph
Quantum computation (81P68) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items (2)
Uses Software
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
