Atomic distributions in crystal structures solved by Boolean satisfiability techniques

2016 ◽  
Vol 231 (2) ◽  
Author(s):  
Mathias Soeken ◽  
Rolf Drechsler ◽  
Reinhard X. Fischer
Keyword(s):  
Crystal Structures ◽  
Unsolved Problem ◽  
Boolean Satisfiability ◽  
Satisfying Assignment ◽  
Interatomic Distances ◽  
Complete Problem ◽  
Atomic Distribution ◽  
Sat Solver ◽  
Np Complete ◽  
Close Contacts

AbstractThe atomic distribution in crystal structures becomes very complex if atoms are disordered and randomly distributed over positions not being fully occupied. Interatomic distances between neighboring atoms might be too close for simultaneous occupancies and thus are mutually exclusive. The distribution of atoms over crystallographic positions avoiding close contacts with neighboring atoms represents an NP-complete problem that is believed to have no efficient solution. Here, we use Boolean satisfiability (SAT) techniques to find a valid atomic distribution pattern in the crystal structure. Distance constraints are encoded as conjunctions of logical disjunctions over Boolean variables and handed to a SAT solver. If a solution exists, the solver supplies a satisfying assignment to the Boolean variables yielding a valid distribution after decoding. That way the hitherto unsolved problem of distributing

scholarly journals NLocalSAT: Boosting Local Search with Solution Prediction

2020 ◽  
Author(s):  
Wenjie Zhang ◽  
Zeyu Sun ◽  
Qihao Zhu ◽  
Ge Li ◽  
Shaowei Cai ◽  
...  
Keyword(s):  
Neural Network ◽  
Local Search ◽  
Prediction Model ◽  
Computer Science ◽  
Boolean Satisfiability ◽  
Stochastic Local Search ◽  
Boolean Satisfiability Problem ◽  
Complete Problem ◽  
Random Manner ◽  
Np Complete

The Boolean satisfiability problem (SAT) is a famous NP-complete problem in computer science. An effective way for solving a satisfiable SAT problem is the stochastic local search (SLS). However, in this method, the initialization is assigned in a random manner, which impacts the effectiveness of SLS solvers. To address this problem, we propose NLocalSAT. NLocalSAT combines SLS with a solution prediction model, which boosts SLS by changing initialization assignments with a neural network. We evaluated NLocalSAT on five SLS solvers (CCAnr, Sparrow, CPSparrow, YalSAT, and probSAT) with instances in the random track of SAT Competition 2018. The experimental results show that solvers with NLocalSAT achieve 27% ~ 62% improvement over the original SLS solvers.

A Multilevel Memetic Algorithm for Large SAT-Encoded Problems

2012 ◽  
Vol 20 (4) ◽  
pp. 641-664 ◽  
Author(s):  
Noureddine Bouhmala
Keyword(s):  
Original Problem ◽  
Memetic Algorithm ◽  
Satisfying Assignment ◽  
Boolean Expression ◽  
Complete Problem ◽  
Starting Solution ◽  
Previous Level ◽  
Np Complete ◽  
Problem Instances ◽  
Hardware Designs

Many researchers have focused on the satisfiability problem and on many of its variants due to its applicability in many areas of artificial intelligence. This NP-complete problem refers to the task of finding a satisfying assignment that makes a Boolean expression evaluate to True. In this work, we introduce a memetic algorithm that makes use of the multilevel paradigm. The multilevel paradigm refers to the process of dividing large and difficult problems into smaller ones, which are hopefully much easier to solve, and then work backward toward the solution of the original problem, using a solution from a previous level as a starting solution at the next level. Results comparing the memetic with and without the multilevel paradigm are presented using problem instances drawn from real industrial hardware designs.

scholarly journals An exact tensor network for the 3SAT problem

2012 ◽  
Vol 12 (3&4) ◽  
pp. 283-292
Author(s):  
Artur Garcia-Saez ◽  
Jose I. Latorre
Keyword(s):  
Computational Complexity ◽  
Explicit Solutions ◽  
Experimental Task ◽  
Satisfying Assignment ◽  
Physical Realization ◽  
Number Of Solutions ◽  
Complete Problem ◽  
Tensor Network ◽  
Np Complete ◽  
Local Observables

We construct a tensor network that delivers an unnormalized quantum state whose coefficients are the solutions to a given instance of 3SAT, an NP-complete problem. The tensor network contraction that corresponds to the norm of the state counts the number of solutions to the instance. It follows that exact contractions of this tensor network are in the \#P-complete computational complexity class, thus believed to be a hard task. Furthermore, we show that for a 3SAT instance with $n$ bits, it is enough to perform a polynomial number of contractions of the tensor network structure associated to the computation of local observables to obtain one of the explicit solutions to the problem, if any. Physical realization of a state described by a generic tensor network is equivalent to finding the satisfying assignment of a 3SAT instance and, consequently, this experimental task is expected to be hard.

scholarly journals Statistical mechanics of an NP-complete problem: subset sum

2001 ◽  
Vol 34 (44) ◽  
pp. 9555-9567 ◽  
Author(s):  
Tomohiro Sasamoto ◽  
Taro Toyoizumi ◽  
Hidetoshi Nishimori
Keyword(s):  
Statistical Mechanics ◽  
Complete Problem ◽  
Subset Sum ◽  
Np Complete

On the transferability of electron density in binary vanadium borides VB, V3B4 and VB2

2015 ◽  
Vol 71 (6) ◽  
pp. 777-787 ◽  
Author(s):  
Bürgehan Terlan ◽  
Lev Akselrud ◽  
Alexey I. Baranov ◽  
Horst Borrmann ◽  
Yuri Grin
Keyword(s):  
Quantum Theory ◽  
Crystal Structures ◽  
Electron Density ◽  
Critical Points ◽  
Atoms In Molecules ◽  
Model Systems ◽  
Suitable Model ◽  
Interatomic Distances ◽  
Systematic Analysis ◽  
A Charge

Binary vanadium borides are suitable model systems for a systematic analysis of the transferability concept in intermetallic compounds due to chemical intergrowth in their crystal structures. In order to underline this structural relationship, topological properties of the electron density in VB, V3B4 and VB2 reconstructed from high-resolution single-crystal X-ray diffraction data as well as derived from quantum chemical calculations, are analysed in terms of Bader's Quantum Theory of Atoms in Molecules [Bader (1990). Atoms in Molecules: A Quantum Theory, 1st ed. Oxford: Clarendon Press]. The compounds VB, V3B4 and VB2 are characterized by a charge transfer from the metal to boron together with two predominant atomic interactions, the shared covalent B—B interactions and the polar covalent B—M interactions. The resembling features of the crystal structures are well reflected by the respective B—B interatomic distances as well as by ρ(r) values at the B—B bond critical points. The latter decrease with an increase in the corresponding interatomic distances. The B—B bonds show transferable electron density properties at bond critical points depending on the respective bond distances.

scholarly journals The Computational Complexity of Probabilistic Planning

1998 ◽  
Vol 9 ◽  
pp. 1-36 ◽  
Author(s):  
M. L. Littman ◽  
J. Goldsmith ◽  
M. Mundhenk
Keyword(s):  
Computational Complexity ◽  
Efficient Algorithms ◽  
Boolean Satisfiability ◽  
Complexity Classes ◽  
Probabilistic Planning ◽  
Plan Evaluation ◽  
Partially Ordered ◽  
Boolean Satisfiability Problem ◽  
Complete Problem ◽  
Planning Problems

We examine the computational complexity of testing and finding small plans in probabilistic planning domains with both flat and propositional representations. The complexity of plan evaluation and existence varies with the plan type sought; we examine totally ordered plans, acyclic plans, and looping plans, and partially ordered plans under three natural definitions of plan value. We show that problems of interest are complete for a variety of complexity classes: PL, P, NP, co-NP, PP, NP^PP, co-NP^PP, and PSPACE. In the process of proving that certain planning problems are complete for NP^PP, we introduce a new basic NP^PP-complete problem, E-MAJSAT, which generalizes the standard Boolean satisfiability problem to computations involving probabilistic quantities; our results suggest that the development of good heuristics for E-MAJSAT could be important for the creation of efficient algorithms for a wide variety of problems.

scholarly journals Consecutive Colouring of Oriented Graphs

2021 ◽  
Vol 76 (4) ◽  
Author(s):  
Marta Borowiecka-Olszewska ◽  
Ewa Drgas-Burchardt ◽  
Nahid Yelene Javier-Nol ◽  
Rita Zuazua
Keyword(s):  
Planar Graphs ◽  
Maximum Degree ◽  
Bipartite Graphs ◽  
Complete Graphs ◽  
Oriented Graphs ◽  
Complete Problem ◽  
Np Complete

AbstractWe consider arc colourings of oriented graphs such that for each vertex the colours of all out-arcs incident with the vertex and the colours of all in-arcs incident with the vertex form intervals. We prove that the existence of such a colouring is an NP-complete problem. We give the solution of the problem for r-regular oriented graphs, transitive tournaments, oriented graphs with small maximum degree, oriented graphs with small order and some other classes of oriented graphs. We state the conjecture that for each graph there exists a consecutive colourable orientation and confirm the conjecture for complete graphs, 2-degenerate graphs, planar graphs with girth at least 8, and bipartite graphs with arboricity at most two that include all planar bipartite graphs. Additionally, we prove that the conjecture is true for all perfect consecutively colourable graphs and for all forbidden graphs for the class of perfect consecutively colourable graphs.

Sign in / Sign up

Export Citation Format

Share Document