Solving QSAT problems with neural MCTS

• URL: http://arxiv.org/abs/2101.06619v1
• Date: Sun, 17 Jan 2021 08:20:07 GMT
• Title: Solving QSAT problems with neural MCTS
• Authors: Ruiyang Xu, Karl Lieberherr
• Abstract summary: Recent achievements from AlphaZero using self-play has shown remarkable performance on several board games. In this paper, we try to leverage the computational power of neural Monte Carlo Tree Search (neural MCTS), the core algorithm from AlphaZero. Knowing that every QSAT problem is equivalent to a QSAT game, the game outcome can be used to derive the solutions of the original QSAT problems.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent achievements from AlphaZero using self-play has shown remarkable performance on several board games. It is plausible to think that self-play, starting from zero knowledge, can gradually approximate a winning strategy for certain two-player games after an amount of training. In this paper, we try to leverage the computational power of neural Monte Carlo Tree Search (neural MCTS), the core algorithm from AlphaZero, to solve Quantified Boolean Formula Satisfaction (QSAT) problems, which are PSPACE complete. Knowing that every QSAT problem is equivalent to a QSAT game, the game outcome can be used to derive the solutions of the original QSAT problems. We propose a way to encode Quantified Boolean Formulas (QBFs) as graphs and apply a graph neural network (GNN) to embed the QBFs into the neural MCTS. After training, an off-the-shelf QSAT solver is used to evaluate the performance of the algorithm. Our result shows that, for problems within a limited size, the algorithm learns to solve the problem correctly merely from self-play.

Related papers

• Towards Less Greedy Quantum Coalition Structure Generation in Induced Subgraph Games [3.6021182997326022]
  The transition to 100% renewable energy requires new techniques for managing energy networks, such as dividing them into sensible subsets of prosumers called micro-grids. Doing so in an optimal manner is a difficult optimization problem, as it can be abstracted to the Coalition Structure Generation problem in Induced Subgraph Games. This work proposes several less greedy QA-based approaches and investigates whether any of them can outperform GCS-Q in terms of solution quality.
  arXiv  Detail & Related papers  (2024-08-08T10:54:56Z)
• LinSATNet: The Positive Linear Satisfiability Neural Networks [116.65291739666303]
  This paper studies how to introduce the popular positive linear satisfiability to neural networks. We propose the first differentiable satisfiability layer based on an extension of the classic Sinkhorn algorithm for jointly encoding multiple sets of marginal distributions.
  arXiv  Detail & Related papers  (2024-07-18T22:05:21Z)
• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem [1.5850859526672516]
  We derive a single differentiable function capable of approximating solutions for the Maximum Satisfiability Problem (MaxSAT) We present a novel neural network architecture to model our differentiable function, and progressively solve MaxSAT using backpropagation.
  arXiv  Detail & Related papers  (2024-02-06T02:33:00Z)
• 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)
• Hardness of Independent Learning and Sparse Equilibrium Computation in Markov Games [70.19141208203227]
  We consider the problem of decentralized multi-agent reinforcement learning in Markov games. We show that no algorithm attains no-regret in general-sum games when executed independently by all players. We show that our lower bounds hold even for seemingly easier setting in which all agents are controlled by a centralized algorithm.
  arXiv  Detail & Related papers  (2023-03-22T03:28:12Z)
• Solving boolean satisfiability problems with the quantum approximate optimization algorithm [0.05076419064097732]
  We study the ability of QAOA to solve hard constraint satisfaction problems, as opposed to quantum computing problems. We develop analytic bounds on the average success probability of QAOA over random formulae at the satisfiability threshold. We find that for around 14 ansatz layers, QAOA matches the scaling performance of the highest-performance classical solver.
  arXiv  Detail & Related papers  (2022-08-14T20:39:48Z)
• An AlphaZero-Inspired Approach to Solving Search Problems [63.24965775030674]
  We adapt the methods and techniques used in AlphaZero for solving search problems. We describe possible representations in terms of easy-instance solvers and self-reductions. We also describe a version of Monte Carlo tree search adapted for search problems.
  arXiv  Detail & Related papers  (2022-07-02T23:39:45Z)
• Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
  The paper reviews the recent literature on solving the Boolean satisfiability problem (SAT) with machine learning techniques. We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT.
  arXiv  Detail & Related papers  (2022-03-02T05:14:12Z)
• Can Graph Neural Networks Learn to Solve MaxSAT Problem? [22.528432249712637]
  We study the capability of GNNs in learning to solve MaxSAT problem, both from theoretical and practical perspectives. We build two kinds of GNN models to learn the solution of MaxSAT instances from benchmarks, and show that GNNs have attractive potential to solve MaxSAT problem through experimental evaluation. We also present a theoretical explanation of the effect that GNNs can learn to solve MaxSAT problem to some extent for the first time, based on the algorithmic alignment theory.
  arXiv  Detail & Related papers  (2021-11-15T07:33:33Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Goal-Aware Neural SAT Solver [2.609784101826762]
  Modern neural networks obtain information about the problem and calculate the output solely from the input values. We argue that it is not always optimal, and the network's performance can be significantly improved by augmenting it with a query mechanism. We propose a neural SAT solver with a query mechanism called QuerySAT and show that it outperforms the neural baseline on a wide range of SAT tasks.
  arXiv  Detail & Related papers  (2021-06-14T04:51:24Z)

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.