Determining the Multiplicative Complexity of Boolean Functions using SAT

• URL: http://arxiv.org/abs/2005.01778v1
• Date: Mon, 4 May 2020 18:29:48 GMT
• Title: Determining the Multiplicative Complexity of Boolean Functions using SAT
• Abstract summary: We present a constructive SAT-based algorithm to determine the multiplicative complexity of a Boolean function. Our algorithm is capable to find all optimum XAGs for representatives of all 5-input affine-equivalent classes.
• Score: 1.4902915966744057
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present a constructive SAT-based algorithm to determine the multiplicative complexity of a Boolean function, i.e., the smallest number of AND gates in any logic network that consists of 2-input AND gates, 2-input XOR gates, and inverters. In order to speed-up solving time, we make use of several symmetry breaking constraints; these exploit properties of XAGs that may be useful beyond the proposed SAT-based algorithm. We further propose a heuristic post-optimization algorithm to reduce the number of XOR gates once the optimum number of AND gates has been obtained, which also makes use of SAT solvers. Our algorithm is capable to find all optimum XAGs for representatives of all 5-input affine-equivalent classes, and for a set of frequently occurring 6-input functions.

Related papers

• Block encoding of sparse matrices with a periodic diagonal structure [67.45502291821956]
  We provide an explicit quantum circuit for block encoding a sparse matrix with a periodic diagonal structure.<n>Various applications for the presented methodology are discussed in the context of solving differential problems.
  arXiv  Detail & Related papers  (2026-02-11T07:24:33Z)
• Provably optimal exact gate synthesis from a discrete gate set [0.0]
  We propose a method for exact circuit synthesizing using a discrete gate set. Our approach translates the problem of a gate specified by its unitary matrix into a satisfiability (SAT) instance.
  arXiv  Detail & Related papers  (2025-03-19T17:32:29Z)
• Simple and Provable Scaling Laws for the Test-Time Compute of Large Language Models [70.07661254213181]
  We propose two principled algorithms for the test-time compute of large language models. We prove theoretically that the failure probability of one algorithm decays to zero exponentially as its test-time compute grows.
  arXiv  Detail & Related papers  (2024-11-29T05:29:47Z)
• Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
  We propose a resource-constrained for instances of Max-SAT that iteratively decomposes a larger problem into smaller subcomponents. We analyze a set of variable selection methods, including a novel graph-based method that exploits the structure of a given SAT instance. We demonstrate our results on a set of randomly generated Max-SAT instances as well as real world examples from the Max-SAT evaluation benchmarks.
  arXiv  Detail & Related papers  (2024-10-11T18:20:08Z)
• Multi-qubit circuit synthesis and Hermitian lattices [0.0]
  We present new optimal and synthesis algorithms for exact synthesis of multi-qubit unitaries and isometries. The optimal algorithms are the A* search instantiated with a new data structure for graph and new consistent functions.
  arXiv  Detail & Related papers  (2024-05-29T17:27:50Z)
• Stochastic Optimization for Non-convex Problem with Inexact Hessian Matrix, Gradient, and Function [99.31457740916815]
  Trust-region (TR) and adaptive regularization using cubics have proven to have some very appealing theoretical properties. We show that TR and ARC methods can simultaneously provide inexact computations of the Hessian, gradient, and function values.
  arXiv  Detail & Related papers  (2023-10-18T10:29:58Z)
• A Parallel and Distributed Quantum SAT Solver Based on Entanglement and Quantum Teleportation [1.5201992393140886]
  We develop a parallel quantum SAT solver, which reduces the time complexity in each iteration from linear time O(m) to constant time O(1) by utilising extra entangled qubits. We have proved the correctness of our approaches and demonstrated them in simulations.
  arXiv  Detail & Related papers  (2023-08-07T06:52:06Z)
• Time-optimal multi-qubit gates: Complexity, efficient heuristic and gate-time bounds [0.2302001830524133]
  A fixed multi-qubit Ising-type interaction together with single-qubit X-gates can be used to synthesize global ZZ-gates. We show that the synthesis of such quantum gates that are time-optimal is NP-hard. We conjecture that any GZZ gate can be executed in a time O(n) for n qubits.
  arXiv  Detail & Related papers  (2023-07-20T18:00:05Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
  arXiv  Detail & Related papers  (2022-10-04T09:19:13Z)
• Constrained mixers for the quantum approximate optimization algorithm [55.41644538483948]
  We present a framework for constructing mixing operators that restrict the evolution to a subspace of the full Hilbert space. We generalize the "XY"-mixer designed to preserve the subspace of "one-hot" states to the general case of subspaces given by a number of computational basis states. Our analysis also leads to valid Trotterizations for "XY"-mixer with fewer CX gates than is known to date.
  arXiv  Detail & Related papers  (2022-03-11T17:19:26Z)
• 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)
• Provably Faster Algorithms for Bilevel Optimization [54.83583213812667]
  Bilevel optimization has been widely applied in many important machine learning applications. We propose two new algorithms for bilevel optimization. We show that both algorithms achieve the complexity of $mathcalO(epsilon-1.5)$, which outperforms all existing algorithms by the order of magnitude.
  arXiv  Detail & Related papers  (2021-06-08T21:05:30Z)
• Towards Optimally Efficient Tree Search with Deep Learning [76.64632985696237]
  This paper investigates the classical integer least-squares problem which estimates signals integer from linear models. The problem is NP-hard and often arises in diverse applications such as signal processing, bioinformatics, communications and machine learning. We propose a general hyper-accelerated tree search (HATS) algorithm by employing a deep neural network to estimate the optimal estimation for the underlying simplified memory-bounded A* algorithm.
  arXiv  Detail & Related papers  (2021-01-07T08:00:02Z)
• Introducing Structure to Expedite Quantum Search [0.0]
  We present a novel quantum algorithm for solving the unstructured search problem with one marked element. Our algorithm is optimal in the total number of elementary gates up to a multiplicative constant. We show how toally reduce the number of elementary gates required to solve the unstructured search problem with multiple marked elements.
  arXiv  Detail & Related papers  (2020-06-10T13:29:47Z)

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.