Repository logo
 

Discovering and harnessing structures in solving application satisfiability instances

Simple item page
dc.contributor.authorChen, Wenxiang, author
dc.contributor.authorWhitley, L. Darrell, advisor
dc.contributor.authorDraper, Bruce A., committee member
dc.contributor.authorBöhm, A. P. Wim, committee member
dc.contributor.authorChong, Edwin K. P., committee member
dc.date.accessioned2018-06-12T16:13:50Z
dc.date.available2018-06-12T16:13:50Z
dc.date.issued2018
dc.description.abstractBoolean satisfiability (SAT) is the first problem proven to be NP-Complete. It has become a fundamental problem for computational complexity theory, and many real-world problems can be encoded as SAT instances. Two major search paradigms have been proposed for SAT solving: Systematic Search (SS) and Stochastic Local Search (SLS). SLS solvers have been shown to be very effective at uniform random instances; SLS solvers are consistently the top winning entries for random tracks at SAT competitions. However, SS solvers dominate hard combinatorial tracks and industrial tracks at SAT competitions, with SLS entries being at the very bottom of the ranking. In this work, we classify both hard combinatorial instances and industrial instances as Application Instances. As application instances are more interesting from a practical perspective, it is critical to analyze the structures in application instances as well as to improve SLS on application instances. We focus on two structural properties of SAT instances in this work: variable interaction topology and subproblem constrainedness. Decomposability focuses on how well the variable interaction of an application instance can be decomposed. We first show that many application instances are indeed highly decomposable. The decomposability of a SAT instance have been extensively exploited with success by SS solvers. Meanwhile, SLS solvers direct the variables to flip using only the objective function, and are completely oblivious of the decomposability of application instances that is inherent to the original problem domain. We propose a new method to decompose variable interactions within SLS solvers, leveraging numerous visited local optima. Our empirical study suggests that the proposed method can vastly simplify SAT instances, which further results in decomposing the instances into thousands of connected components. Furthermore, we demonstrate the utility of the decomposition, in improving SLS solvers. We propose a new framework called PXSAT, based on the recombination operator Partition Crossover (PX). Given q components, PX is able to find the best of 2q possible candidate solutions in linear time. Empirical results on an extensive set of application instances show PXSAT can yield statistically significantly better results. We improve two of best local search solvers, AdaptG2WSAT and Sparrow. PXSAT combined with AdaptG2WSAT is also able to outperform CCLS, winners of several recent MAXSAT competitions. The other structural property we study is subproblem constrainedness. We observe that, on some application SAT instance classes, the original problem can be partitioned into several subproblems, where each subproblems is highly constrained. While subproblem constrainedness has been exploited in SS solvers before, we propose to exploit it in SLS solvers using two alternative representations that can be obtained efficiently based on the canonical CNF representation. Our empirical results show that the new alternative representative enables a simple SLS solver to outperform several sophisticated and highly optimized SLS solvers on the SAT encoding of semiprime factoring problem.
dc.format.mediumborn digital
dc.format.mediumdoctoral dissertations
dc.identifierChen_colostate_0053A_14665.pdf
dc.identifier.urihttps://hdl.handle.net/10217/189292
dc.languageEnglish
dc.language.isoeng
dc.publisherColorado State University. Libraries
dc.relation.ispartof2000-2019
dc.rightsCopyright and other restrictions may apply. User is responsible for compliance with all applicable laws. For information about copyright law, please see https://libguides.colostate.edu/copyright.
dc.subjectMAXSAT
dc.subjectSAT
dc.subjectoptimization
dc.subjectlocal search
dc.titleDiscovering and harnessing structures in solving application satisfiability instances
dc.typeText
dcterms.rights.dplaThis Item is protected by copyright and/or related rights (https://rightsstatements.org/vocab/InC/1.0/). You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use. For other uses you need to obtain permission from the rights-holder(s).
thesis.degree.disciplineComputer Science
thesis.degree.grantorColorado State University
thesis.degree.levelDoctoral
thesis.degree.nameDoctor of Philosophy (Ph.D.)

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Chen_colostate_0053A_14665.pdf
Size:
4.79 MB
Format:
Adobe Portable Document Format
Download

Collections

2000-2019
Theses and Dissertations