subject:(MAXSAT)

Colorado State University

1. Chen, Wenxiang. Discovering and harnessing structures in solving application satisfiability instances.

Degree: PhD, Computer Science, 2018, Colorado State University

► Boolean 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… (more)

▼ Boolean 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… Advisors/Committee Members: Whitley, L. Darrell (advisor), Draper, Bruce A. (committee member), Böhm, A. P. Wim (committee member), Chong, Edwin K. P. (committee member).

Subjects/Keywords: MAXSAT; SAT; optimization; local search

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Chen, W. (2018). Discovering and harnessing structures in solving application satisfiability instances. (Doctoral Dissertation). Colorado State University. Retrieved from http://hdl.handle.net/10217/189292

Chicago Manual of Style (16^th Edition):

Chen, Wenxiang. “Discovering and harnessing structures in solving application satisfiability instances.” 2018. Doctoral Dissertation, Colorado State University. Accessed March 09, 2021. http://hdl.handle.net/10217/189292.

MLA Handbook (7^th Edition):

Chen, Wenxiang. “Discovering and harnessing structures in solving application satisfiability instances.” 2018. Web. 09 Mar 2021.

Vancouver:

Chen W. Discovering and harnessing structures in solving application satisfiability instances. [Internet] [Doctoral dissertation]. Colorado State University; 2018. [cited 2021 Mar 09]. Available from: http://hdl.handle.net/10217/189292.

Council of Science Editors:

Chen W. Discovering and harnessing structures in solving application satisfiability instances. [Doctoral Dissertation]. Colorado State University; 2018. Available from: http://hdl.handle.net/10217/189292

2. Sohanghpurwala, Ali Asgar Ali Akbar. Exploits in Concurrency for Boolean Satisfiability.

Degree: PhD, Computer Engineering, 2018, Virginia Tech

URL: http://hdl.handle.net/10919/86417

► Boolean Satisfiability (SAT) is a problem that holds great theoretical significance along with effective formulations that benefit many real-world applications. While the general problem is… (more)

Subjects/Keywords: Satisfiability; FPGA; SLS; MaxSAT; Parallel Local Search; SAT

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Sohanghpurwala, A. A. A. A. (2018). Exploits in Concurrency for Boolean Satisfiability. (Doctoral Dissertation). Virginia Tech. Retrieved from http://hdl.handle.net/10919/86417

Chicago Manual of Style (16^th Edition):

Sohanghpurwala, Ali Asgar Ali Akbar. “Exploits in Concurrency for Boolean Satisfiability.” 2018. Doctoral Dissertation, Virginia Tech. Accessed March 09, 2021. http://hdl.handle.net/10919/86417.

MLA Handbook (7^th Edition):

Sohanghpurwala, Ali Asgar Ali Akbar. “Exploits in Concurrency for Boolean Satisfiability.” 2018. Web. 09 Mar 2021.

Vancouver:

Sohanghpurwala AAAA. Exploits in Concurrency for Boolean Satisfiability. [Internet] [Doctoral dissertation]. Virginia Tech; 2018. [cited 2021 Mar 09]. Available from: http://hdl.handle.net/10919/86417.

Council of Science Editors:

Sohanghpurwala AAAA. Exploits in Concurrency for Boolean Satisfiability. [Doctoral Dissertation]. Virginia Tech; 2018. Available from: http://hdl.handle.net/10919/86417

3. Gonzalez, Pedro Frazão. Application of substructural local search in the MAXSAT problem.

Degree: 2011, RCAAP

URL: https://www.rcaap.pt/detail.jsp?id=oai:sapientia.ualg.pt:10400.1/2746

►

Dissertação de mest., Engenharia Informática, Faculdade de Ciências e Tecnologia, Univ. do Algarve, 2011

Genetic Algorithms (GAs) are stochastic optimizers usually applied to problems where… (more)

▼

Dissertação de mest., Engenharia Informática, Faculdade de Ciências e Tecnologia, Univ. do Algarve, 2011

Genetic Algorithms (GAs) are stochastic optimizers usually applied to problems where the use of deterministic methods is not practical or when information about how to solve the problem is scarce. Although traditional GAs show good results in a broad range of problems, they do not take into account the dependencies that may exist among the variables of a given problem. Without respecting these links, achieving the optimum can be very hard or even impossible. Estimation of Distribution Algorithms (EDAs) are methods inspired on GAs that are able to learn the linkage between variables without providing any information about the problem structure. These methods use machine learning techniques to build a probabilistic model that captures the regularities present in the population (a set of candidate solutions for our problem). The learned model is used to generate new solutions similar to those present in the population but also with some innovation. The Substructural Local Search (SLS) is a method recently proposed that takes advantage from the model built by the EDA and performs local search in each substructure of the model, providing in the end a high quality solution. This method has shown to improve the e_ciency of the search when applied to di_erent EDAs in several arti_cial problems of bounded di_culty. In this thesis, the utility of SLS in the hierarchical Bayesian Optimization Algorithm (hBOA) (an EDA that uses Bayesian networks as probabilistic model), is investigated in the MAXSAT problem. Results show that SLS is able to improve the e_ciency of hBOA, but only on MAXSAT instances with a small number of variables. For larger instances that behavior is not observed. Additionally, the SLS execution is analyzed in order to better understand the obtained results. Finally, some observations and suggestions are exposed for an improvement of SLS.

Advisors/Committee Members: Lobo, Fernando.

Subjects/Keywords: Algoritmos genéticos; Algoritmos da estimação da distribuição; Redes Bayesianas; Pesquisa local sub-estrutural; MAXSAT

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Gonzalez, P. F. (2011). Application of substructural local search in the MAXSAT problem. (Thesis). RCAAP. Retrieved from https://www.rcaap.pt/detail.jsp?id=oai:sapientia.ualg.pt:10400.1/2746

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Gonzalez, Pedro Frazão. “Application of substructural local search in the MAXSAT problem.” 2011. Thesis, RCAAP. Accessed March 09, 2021. https://www.rcaap.pt/detail.jsp?id=oai:sapientia.ualg.pt:10400.1/2746.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Gonzalez, Pedro Frazão. “Application of substructural local search in the MAXSAT problem.” 2011. Web. 09 Mar 2021.

Vancouver:

Gonzalez PF. Application of substructural local search in the MAXSAT problem. [Internet] [Thesis]. RCAAP; 2011. [cited 2021 Mar 09]. Available from: https://www.rcaap.pt/detail.jsp?id=oai:sapientia.ualg.pt:10400.1/2746.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Gonzalez PF. Application of substructural local search in the MAXSAT problem. [Thesis]. RCAAP; 2011. Available from: https://www.rcaap.pt/detail.jsp?id=oai:sapientia.ualg.pt:10400.1/2746

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

4. Gabàs Masip, Joel. SAT-based approaches for constraint optimization.

Degree: Departament d'Informàtica i Enginyeria Industrial, 2016, Universitat de Lleida

URL: http://hdl.handle.net/10803/396610

► Constraint optimization has been successfully used to solve problems in many real world (industrial) domains. This PhD thesis is focused on logic-based approaches, in particular,… (more)

Subjects/Keywords: MaxSAT; SAT; Optimització; Optimización; Optimization; Ciència de la computació i intel·ligència artificial; 004

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Gabàs Masip, J. (2016). SAT-based approaches for constraint optimization. (Thesis). Universitat de Lleida. Retrieved from http://hdl.handle.net/10803/396610

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Gabàs Masip, Joel. “SAT-based approaches for constraint optimization.” 2016. Thesis, Universitat de Lleida. Accessed March 09, 2021. http://hdl.handle.net/10803/396610.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Gabàs Masip, Joel. “SAT-based approaches for constraint optimization.” 2016. Web. 09 Mar 2021.

Vancouver:

Gabàs Masip J. SAT-based approaches for constraint optimization. [Internet] [Thesis]. Universitat de Lleida; 2016. [cited 2021 Mar 09]. Available from: http://hdl.handle.net/10803/396610.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Gabàs Masip J. SAT-based approaches for constraint optimization. [Thesis]. Universitat de Lleida; 2016. Available from: http://hdl.handle.net/10803/396610

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

5. Klein, Dominik. Equational Reasoning and Completion.

Degree: Japan Advanced Institute of Science and Technology / 北陸先端科学技術大学院大学

URL: http://hdl.handle.net/10119/10560

Supervisor: Mizuhito Ogawa

情報科学研究科

博士

Subjects/Keywords: Term Rewriting; Rewriting; Confluence; Completion; Constraint Solving; MaxSAT; Relative Termination

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Klein, D. (n.d.). Equational Reasoning and Completion. (Thesis). Japan Advanced Institute of Science and Technology / 北陸先端科学技術大学院大学. Retrieved from http://hdl.handle.net/10119/10560

Note: this citation may be lacking information needed for this citation format:
No year of publication.
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Klein, Dominik. “Equational Reasoning and Completion.” Thesis, Japan Advanced Institute of Science and Technology / 北陸先端科学技術大学院大学. Accessed March 09, 2021. http://hdl.handle.net/10119/10560.

Note: this citation may be lacking information needed for this citation format:
No year of publication.
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Klein, Dominik. “Equational Reasoning and Completion.” Web. 09 Mar 2021.

Note: this citation may be lacking information needed for this citation format:
No year of publication.

Vancouver:

Klein D. Equational Reasoning and Completion. [Internet] [Thesis]. Japan Advanced Institute of Science and Technology / 北陸先端科学技術大学院大学; [cited 2021 Mar 09]. Available from: http://hdl.handle.net/10119/10560.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
No year of publication.

Council of Science Editors:

Klein D. Equational Reasoning and Completion. [Thesis]. Japan Advanced Institute of Science and Technology / 北陸先端科学技術大学院大学; Available from: http://hdl.handle.net/10119/10560

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation
No year of publication.

6. Cabiscol i Teixidó, Alba. Encodings and Benchmarks for MaxSAT Solving.

Degree: Departament d'Informàtica i Enginyeria Industrial, 2012, Universitat de Lleida

URL: http://hdl.handle.net/10803/84021

Subjects/Keywords: SAT; MaxSAT; Codificacions; CSP; Benchmarks; Encodings; Codificaciones; Ciència de la Computació i Inteligència Artificial; 004

…vi CONTENTS 3.2 MaxSAT algorithms… …bound with inference . . . . . . . . . . . . 46 3.4 SAT-based MaxSAT algorithms… …76 5 Encoding MaxCSP into Partial MaxSAT 83 5.1 MaxCSP preliminaries… …84 5.2 Direct encodings from MaxCSP into Partial MaxSAT . . . . . . . . . . 84 5.3… …Minimal support encodings from MaxCSP into Partial MaxSAT . . . . 86 5.4 Support encodings…

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Cabiscol i Teixidó, A. (2012). Encodings and Benchmarks for MaxSAT Solving. (Thesis). Universitat de Lleida. Retrieved from http://hdl.handle.net/10803/84021

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Chicago Manual of Style (16^th Edition):

Cabiscol i Teixidó, Alba. “Encodings and Benchmarks for MaxSAT Solving.” 2012. Thesis, Universitat de Lleida. Accessed March 09, 2021. http://hdl.handle.net/10803/84021.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

MLA Handbook (7^th Edition):

Cabiscol i Teixidó, Alba. “Encodings and Benchmarks for MaxSAT Solving.” 2012. Web. 09 Mar 2021.

Vancouver:

Cabiscol i Teixidó A. Encodings and Benchmarks for MaxSAT Solving. [Internet] [Thesis]. Universitat de Lleida; 2012. [cited 2021 Mar 09]. Available from: http://hdl.handle.net/10803/84021.

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

Council of Science Editors:

Cabiscol i Teixidó A. Encodings and Benchmarks for MaxSAT Solving. [Thesis]. Universitat de Lleida; 2012. Available from: http://hdl.handle.net/10803/84021

Note: this citation may be lacking information needed for this citation format:
Not specified: Masters Thesis or Doctoral Dissertation

7. Zhang, Xin. Combining logical and probabilistic reasoning in program analysis.

Degree: PhD, Computer Science, 2017, Georgia Tech

URL: http://hdl.handle.net/1853/59200

► Software is becoming increasingly pervasive and complex. These trends expose masses of users to unintended software failures and deliberate cyber-attacks. A widely adopted solution to… (more)

Subjects/Keywords: Program analysis; Logic; Probability; Combined logical and probabilistic reasoning; Markov logic networks; Datalog; MaxSAT; Verification; Bug finding; Programming languages; Software engineering

12 more images…

Record Details Similar Records Cite « Share

❌

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6^th Edition):

Zhang, X. (2017). Combining logical and probabilistic reasoning in program analysis. (Doctoral Dissertation). Georgia Tech. Retrieved from http://hdl.handle.net/1853/59200

Chicago Manual of Style (16^th Edition):

Zhang, Xin. “Combining logical and probabilistic reasoning in program analysis.” 2017. Doctoral Dissertation, Georgia Tech. Accessed March 09, 2021. http://hdl.handle.net/1853/59200.

MLA Handbook (7^th Edition):

Zhang, Xin. “Combining logical and probabilistic reasoning in program analysis.” 2017. Web. 09 Mar 2021.

Vancouver:

Zhang X. Combining logical and probabilistic reasoning in program analysis. [Internet] [Doctoral dissertation]. Georgia Tech; 2017. [cited 2021 Mar 09]. Available from: http://hdl.handle.net/1853/59200.

Council of Science Editors:

Zhang X. Combining logical and probabilistic reasoning in program analysis. [Doctoral Dissertation]. Georgia Tech; 2017. Available from: http://hdl.handle.net/1853/59200

		in
And / Or
		in
And / Or
		in
And / Or
		in

Open Access Theses and Dissertations