Identification of hard instances and backbones in 3-SAT using network theory and network guided decomposition

Download files
Access & Terms of Use
open access
Copyright: Hossain, Md Murad
Altmetric
Abstract
The satisfiability problem (SAT) is a core problem in mathematical logic and computing theory. In practice, SAT is fundamental for solving many problems in automated reasoning, computer-aided design, computer-aided manufacturing, machine vision, database design, robotics, integrated circuit design, computer architecture design and network design. How hard is a 3-SAT problem? This question has been the focal point of many research papers over the years. It is well accepted that the difficulty of the problem depends on its structure. In the case of combinatorial optimization problems, it is clear that many of them have phase transitions. Theoretical and experimental analyses revealed that, for a randomly generated 3-SAT problem a phase transition exists as the ratio of clauses to literals is varied. This thesis looks at a problem's difficulty using a graph theory lens. We reveal the relationship between the difficulty of a 3-SAT problem and the graph's properties. Given a 3-SAT problem, we construct a graph in which each literal becomes a node and the co-existence of two literals in a clause is represented by an undirected unweighted link between the two nodes. We find that graph properties, such as characteristic path lengths, motifs and clustering coefficients are correlated with the phase transition in a 3-SAT problem. Moreover, these properties can even reveal information about different backbone sizes. The significance of these findings is twofold. Firstly, we establish, for the first time a link between the theory of phase transition in a 3-SAT problem and those in complex systems and networks. Secondly, the properties discovered can guide a problem decomposition approach in order to identify the bottleneck(s) in large-scale real-world problems. We then extend the findings to establish whether or not the phase transition phenomenon exists for non-uniform randomly generated problems. A positive answer to this question means that, in principle, we can: (1) generate synthetic problems for combinatorial optimizations that are not uniform; (2) generate synthetic problems that resemble hard versions of real-world problems; and (3) identify the features we need to look for in a problem in order to test whether it is hard or not. Last, but not least, we address the question of whether network properties can guide a decomposition process to find out the bottleneck(s) in a large system. We show that clustering a large problem into sub-problems, according to its network properties, and starting the search process with the solution of each cluster as a partial solution for the overall problem is highly efficient for finding good solutions. We present results showing that the decomposition algorithm outperforms one of the best known heuristics, the `R-Novelty' in terms of the quality of the solution to a problem and the numbers of flips and binary checks required to achieve it.
Persistent link to this record
Link to Publisher Version
Link to Open Access Version
Additional Link
Author(s)
Hossain, Md Murad
Supervisor(s)
Abbass, Hussein
Lokan, Chris
Creator(s)
Editor(s)
Translator(s)
Curator(s)
Designer(s)
Arranger(s)
Composer(s)
Recordist(s)
Conference Proceedings Editor(s)
Other Contributor(s)
Corporate/Industry Contributor(s)
Publication Year
2011
Resource Type
Thesis
Degree Type
Masters Thesis
UNSW Faculty
Files
download whole.pdf 2.4 MB Adobe Portable Document Format
Related dataset(s)