اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدEfficient Solution of Boolean Satisfiability Problems with Digital MemComputing
323
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
Boolean satisfiability is a propositional logic problem of interest in multiple fields, e.g., physics, mathematics, and computer science. Beyond a field of research, instances of the SAT problem, as it is known, require efficient solution methods in a variety of applications. It is the decision problem of determining whether a Boolean formula has a satisfying assignment, believed to require exponentially growing time for an algorithm to solve for the worst-case instances. Yet, the efficient solution of many classes of Boolean formulae eludes even the most successful algorithms, not only for the worst-case scenarios, but also for typical-case instances. Here, we introduce a memory-assisted physical system (a digital memcomputing machine) that, when its non-linear ordinary differential equations are integrated numerically, shows evidence for polynomially-bounded scalability while solving hard planted-solution instances of SAT, known to require exponential time to solve in the typical case for both complete and incomplete algorithms. Furthermore, we analytically demonstrate that the physical system can efficiently solve the SAT problem in continuous time, without the need to introduce chaos or an exponentially growing energy. The efficiency of the simulations is related to the collective dynamical properties of the original physical system that persist in the numerical integration to robustly guide the solution search even in the presence of numerical errors. We anticipate our results to broaden research directions in physics-inspired computing paradigms ranging from theory to application, from simulation to hardware implementation.
قيم البحث
اقرأ أيضاً
Efficient solutions to NP-complete problems would significantly benefit both science and industry. However, such problems are intractable on digital computers based on the von Neumann architecture, thus creating the need for alternative solutions to
tackle such problems. Recently, a deterministic, continuous-time dynamical system (CTDS) was proposed (Nat.Phys. {bf 7}(12), 966 (2011)) to solve a representative NP-complete problem, Boolean Satisfiability (SAT). This solver shows polynomial analog time-complexity on even the hardest benchmark $k$-SAT ($k geq 3$) formulas, but at an energy cost through exponentially driven auxiliary variables. This paper presents a novel analog hardware SAT solver, AC-SAT, implementing the CTDS via incorporating novel, analog circuit design ideas. AC-SAT is intended to be used as a co-processor and is programmable for handling different problem specifications. It is especially effective for solving hard $k$-SAT problem instances that are challenging for algorithms running on digital machines. Furthermore, with its modular design, AC-SAT can readily be extended to solve larger size problems, while the size of the circuit grows linearly with the product of the number of variables and number of clauses. The circuit is designed and simulated based on a 32nm CMOS technology. SPICE simulation results show speedup factors of $sim$10$^4$ on even the hardest 3-SAT problems, when compared with a state-of-the-art SAT solver on digital computers. As an example, for hard problems with $N=50$ variables and $M=212$ clauses, solutions are found within from a few $ns$ to a few hundred $ns$.
Digital memcomputing machines (DMMs) are a class of computational machines designed to solve combinatorial optimization problems. A practical realization of DMMs can be accomplished via electrical circuits of highly non-linear, point-dissipative dyna
mical systems engineered so that periodic orbits and chaos can be avoided. A given logic problem is first mapped into this type of dynamical system whose point attractors represent the solutions of the original problem. A DMM then finds the solution via a succession of elementary instantons whose role is to eliminate solitonic configurations of logical inconsistency (logical defects) from the circuit. By employing a supersymmetric theory of dynamics, a DMM can be described by a cohomological field theory that allows for computation of certain topological matrix elements on instantons that have the mathematical meaning of intersection numbers on instantons. We discuss the dynamical meaning of these matrix elements, and argue that the number of elementary instantons needed to reach the solution cannot exceed the number of state variables of DMMs, which in turn can only grow at most polynomially with the size of the problem. These results shed further light on the relation between logic, dynamics and topology in digital memcomputing.
Transient chaos is an ubiquitous phenomenon characterizing the dynamics of phase space trajectories evolving towards a steady state attractor in physical systems as diverse as fluids, chemical reactions and condensed matter systems. Here we show that
transient chaos also appears in the dynamics of certain efficient algorithms searching for solutions of constraint satisfaction problems that include scheduling, circuit design, routing, database problems or even Sudoku. In particular, we present a study of the emergence of hardness in Boolean satisfiability ($k$-SAT), a canonical class of constraint satisfaction problems, by using an analog deterministic algorithm based on a system of ordinary differential equations. Problem hardness is defined through the escape rate $kappa$, an invariant measure of transient chaos of the dynamical system corresponding to the analog algorithm, and it expresses the rate at which the trajectory approaches a solution.We show that for a given density of constraints and fixed number of Boolean variables $N$, the hardness of formulas in random $k$-SAT ensembles has a wide variation, approximable by a lognormal distribution. We also show that when increasing the density of constraints $alpha$, hardness appears through a second-order phase transition at $alpha_{chi}$ in the random 3-SAT ensemble where dynamical trajectories become transiently chaotic. A similar behavior is found in 4-SAT as well, however, such transition does not occur for 2-SAT. This behavior also implies a novel type of transient chaos in which the escape rate has an exponential-algebraic dependence on the critical parameter $kappa sim N^{B|alpha - alpha_{chi}|^{1-gamma}}$ with $0< gamma < 1$. We demonstrate that the transition is generated by the appearance of metastable basins in the solution space as the density of constraints $alpha$ is increased.
The original Pascaline was a mechanical calculator able to sum and subtract integers. It encodes information in the angles of mechanical wheels and through a set of gears, and aided by gravity, could perform the calculations. Here, we show that such
a concept can be realized in electronics using memory elements such as memristive systems. By using memristive emulators we have demonstrated experimentally the memcomputing version of the mechanical Pascaline, capable of processing and storing the numerical results in the multiple levels of each memristive element. Our result is the first experimental demonstration of multidigit arithmetics with multi-level memory devices that further emphasizes the versatility and potential of memristive systems for future massively-parallel high-density computing architectures.
We report a cluster of results on k-QSAT, the problem of quantum satisfiability for k-qubit projectors which generalizes classical satisfiability with k-bit clauses to the quantum setting. First we define the NP-complete problem of product satisfiabi
lity and give a geometrical criterion for deciding when a QSAT interaction graph is product satisfiable with positive probability. We show that the same criterion suffices to establish quantum satisfiability for all projectors. Second, we apply these results to the random graph ensemble with generic projectors and obtain improved lower bounds on the location of the SAT--unSAT transition. Third, we present numerical results on random, generic satisfiability which provide estimates for the location of the transition for k=3 and k=4 and mild evidence for the existence of a phase which is satisfiable by entangled states alone.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
