Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userLinear Programming Formulation of the Boolean Satisfiability Problem
722
0
0.0
(
0
)
Added by
Moustapha Diaby
Publication date
2016
fields
Informatics Engineering
and research's language is
English
Authors
Moustapha Diaby
Ask ChatGPT about the research
No Arabic abstract
In this paper, we present a new, graph-based modeling approach and a polynomial-sized linear programming (LP) formulation of the Boolean satisfiability problem (SAT). The approach is illustrated with a numerical example.
rate research
Read More
This paper has been withdrawn because Theorem 21 and Corollary 22 are in error; The modeling idea is OK, but it needs 9-dimensional variables instead of the 8-dimensional variables defined in notations 6.9. Examples of the correct model (with 9-index variables) are: (1) Diaby, M., Linear Programming Formulation of the Set Partitioning Problem, International Journal of Operational Research 8:4 (August 2010) pp. 399-427; (2) Diaby, M., Linear Programming Formulation of the Vertex Coloring Problem, International Journal of Mathematics in Operational Research 2:3 (May 2010) pp. 259-289; (3) Diaby, M., The Traveling Salesman Problem: A Linear Programming Formulation, WSEAS Transactions on Mathematics, 6:6 (June 2007) pp. 745-754.
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$.
Propositional satisfiability (SAT) is one of the most fundamental problems in computer science. Its worst-case hardness lies at the core of computational complexity theory, for example in the form of NP-hardness and the (Strong) Exponential Time Hypothesis. In practice however, SAT instances can often be solved efficiently. This contradicting behavior has spawned interest in the average-case analysis of SAT and has triggered the development of sophisticated rigorous and non-rigorous techniques for analyzing random structures. Despite a long line of research and substantial progress, most theoretical work on random SAT assumes a uniform distribution on the variables. In contrast, real-world instances often exhibit large fluctuations in variable occurrence. This can be modeled by a non-uniform distribution of the variables, which can result in distributions closer to industrial SAT instances. We study satisfiability thresholds of non-uniform random $2$-SAT with $n$ variables and $m$ clauses and with an arbitrary probability distribution $(p_i)_{iin[n]}$ with $p_1 ge p_2 ge ldots ge p_n > 0$ over the n variables. We show for $p_1^2=Theta(sum_{i=1}^n p_i^2)$ that the asymptotic satisfiability threshold is at $m=Theta( (1-sum_{i=1}^n p_i^2)/(p_1cdot(sum_{i=2}^n p_i^2)^{1/2}) )$ and that it is coarse. For $p_1^2=o(sum_{i=1}^n p_i^2)$ we show that there is a sharp satisfiability threshold at $m=(sum_{i=1}^n p_i^2)^{-1}$. This result generalizes the seminal works by Chvatal and Reed [FOCS 1992] and by Goerdt [JCSS 1996].
In this paper, we present a new linear programming (LP) formulation of the Traveling Salesman Problem (TSP). The proposed model has O(n^8) variables and O(n^7) constraints, where n is the number of cities. Our numerical experimentation shows that computational times for the proposed linear program are several orders of magnitude smaller than those for the existing model [3].
Quantum walks have received a great deal of attention recently because they can be used to develop new quantum algorithms and to simulate interesting quantum systems. In this work, we focus on a model called staggered quantum walk, which employs advanced ideas of graph theory and has the advantage of including the most important instances of other discrete-time models. The evolution operator of the staggered model is obtained from a tessellation cover, which is defined in terms of a set of partitions of the graph into cliques. It is important to establish the minimum number of tessellations required in a tessellation cover, and what classes of graphs admit a small number of tessellations. We describe two main results: (1) infinite classes of graphs where we relate the chromatic number of the clique graph to the minimum number of tessellations required in a tessellation cover, and (2) the problem of deciding whether a graph is $k$-tessellable for $kge 3$ is NP-complete.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
