{"id":{"repo_id":"rice","oai_identifier":"oai:repository.rice.edu:1911/118674"},"canonical_url":"https://search.dev.ndltd.org/etd/rice/oai:repository.rice.edu:1911/118674","repository":{"repo_id":"rice","name":"Rice University","base_url":"https://repository.rice.edu/server/oai/request"},"display":{"title":"Solving Hybrid Boolean SAT by Continuous Optimization","abstract":"The Boolean SATisfiability problem (SAT) is of central importance in computer science. Despite the NP-completeness of SAT, progress on the engineering side—especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers—has been remarkable. Yet, while SAT solvers, aimed at solving industrial-scale benchmarks in Conjunctive Normal Form (CNF), have become quite mature, other types of non-CNF, i.e., hybrid constraints (e.g., cardinality/pseudo-Boolean constraints and XOR}s play important roles in critical applications such as cryptography, task scheduling, and quantum computing. Nevertheless, SAT solvers that are effective on hybrid constraints are less well studied; a general approach for handling hybrid constraints is still lacking. The thesis focuses on the applications and approaches for hybrid SAT solving. It starts with a motivating application of hybrid SAT solving in quantum computing. A smart hybrid SAT encoding is proposed to solve the problem with quantum interest. Then the thesis introduces efforts for addressing critical limitations of a continuous-optimization-based framework for hybrid SAT solving, named FourierSAT. In FourierSAT, Boolean constraints are converted into polynomials via Walsh-Hadamard-Fourier Transform and constrained continuous optimizers are then applied to search for a solution. FourierSAT suffers from slow gradient computation, incapability of handling pseudo-Boolean (PB) constraints, and the restriction to constrained optimizers, which together limit its potential. The thesis presents to use binary decision diagrams (BDDs) to replace polynomials, which significantly accelerates the gradient computation both in theory and practice, meanwhile handling PB constraints. The thesis then proposes an approach for removing the requirement of supporting constraints from the optimizers while still maintaining soundness, making FourierSAT compatible to several machine-learning-inspired optimizers. Empirical results demonstrate that the improved FourierSAT achieves promising performance on certain classes of applications and qualifies to be a useful complement to the SAT solver portfolio. This thesis further opens a solid research direction by bridging analysis of Boolean functions, continuous optimization and SAT solving. FourierSAT will continue benefiting from future advancements in multiple fields.","abstract_html":"The Boolean SATisfiability problem (SAT) is of central importance in computer science. Despite the NP-completeness of SAT, progress on the engineering side—especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers—has been remarkable. Yet, while SAT solvers, aimed at solving industrial-scale benchmarks in Conjunctive Normal Form (CNF), have become quite mature, other types of non-CNF, i.e., hybrid constraints (e.g., cardinality/pseudo-Boolean constraints and XOR}s play important roles in critical applications such as cryptography, task scheduling, and quantum computing. Nevertheless, SAT solvers that are effective on hybrid constraints are less well studied; a general approach for handling hybrid constraints is still lacking. The thesis focuses on the applications and approaches for hybrid SAT solving. It starts with a motivating application of hybrid SAT solving in quantum computing. A smart hybrid SAT encoding is proposed to solve the problem with quantum interest. Then the thesis introduces efforts for addressing critical limitations of a continuous-optimization-based framework for hybrid SAT solving, named FourierSAT. In FourierSAT, Boolean constraints are converted into polynomials via Walsh-Hadamard-Fourier Transform and constrained continuous optimizers are then applied to search for a solution. FourierSAT suffers from slow gradient computation, incapability of handling pseudo-Boolean (PB) constraints, and the restriction to constrained optimizers, which together limit its potential. The thesis presents to use binary decision diagrams (BDDs) to replace polynomials, which significantly accelerates the gradient computation both in theory and practice, meanwhile handling PB constraints. The thesis then proposes an approach for removing the requirement of supporting constraints from the optimizers while still maintaining soundness, making FourierSAT compatible to several machine-learning-inspired optimizers. Empirical results demonstrate that the improved FourierSAT achieves promising performance on certain classes of applications and qualifies to be a useful complement to the SAT solver portfolio. This thesis further opens a solid research direction by bridging analysis of Boolean functions, continuous optimization and SAT solving. FourierSAT will continue benefiting from future advancements in multiple fields.","abstract_has_math":false,"creators":["Zhang, Zhiwei"],"institution":"Rice University","degree_name":"Doctor of Philosophy","degree_level":"Doctoral","degree_discipline":"Engineering","degree_department":null,"school":null,"contributors":[],"advisors":["Vardi, Moshe Y."],"committee_chairs":[],"committee_members":[],"year":2025,"date_issued":"2025-06-06","date_published":"2025-06-06","updated_at":"2026-07-24T04:10:37Z","subjects":["SAT Solving","Continuous Optimization"],"languages":["eng"],"rights":["Copyright is held by the author, unless otherwise indicated. Permission to reuse, publish, or reproduce the work beyond the bounds of fair use or other exemptions to copyright law must be obtained from the copyright holder."],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/1911/118674","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Vardi, Moshe Y."]},{"key":"dc:creator","label":"Author","values":["Zhang, Zhiwei"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2025-09-11T16:09:33Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2025-09-11T16:09:33Z"]},{"key":"dc:date.issued","label":"Date","values":["2025-06-06"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Engineering"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Doctoral"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Doctor of Philosophy"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Rice University"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["SAT Solving","Continuous Optimization"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright is held by the author, unless otherwise indicated. Permission to reuse, publish, or reproduce the work beyond the bounds of fair use or other exemptions to copyright law must be obtained from the copyright holder."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1911/118674"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["The Boolean SATisfiability problem (SAT) is of central importance in computer science. Despite the NP-completeness of SAT, progress on the engineering side—especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers—has been remarkable. Yet, while SAT solvers, aimed at solving industrial-scale benchmarks in Conjunctive Normal Form (CNF), have become quite mature, other types of non-CNF, i.e., hybrid constraints (e.g., cardinality/pseudo-Boolean constraints and XOR}s play important roles in critical applications such as cryptography, task scheduling, and quantum computing. Nevertheless, SAT solvers that are effective on hybrid constraints are less well studied; a general approach for handling hybrid constraints is still lacking. The thesis focuses on the applications and approaches for hybrid SAT solving. It starts with a motivating application of hybrid SAT solving in quantum computing. A smart hybrid SAT encoding is proposed to solve the problem with quantum interest. Then the thesis introduces efforts for addressing critical limitations of a continuous-optimization-based framework for hybrid SAT solving, named FourierSAT. In FourierSAT, Boolean constraints are converted into polynomials via Walsh-Hadamard-Fourier Transform and constrained continuous optimizers are then applied to search for a solution. FourierSAT suffers from slow gradient computation, incapability of handling pseudo-Boolean (PB) constraints, and the restriction to constrained optimizers, which together limit its potential. The thesis presents to use binary decision diagrams (BDDs) to replace polynomials, which significantly accelerates the gradient computation both in theory and practice, meanwhile handling PB constraints. The thesis then proposes an approach for removing the requirement of supporting constraints from the optimizers while still maintaining soundness, making FourierSAT compatible to several machine-learning-inspired optimizers. Empirical results demonstrate that the improved FourierSAT achieves promising performance on certain classes of applications and qualifies to be a useful complement to the SAT solver portfolio. This thesis further opens a solid research direction by bridging analysis of Boolean functions, continuous optimization and SAT solving. FourierSAT will continue benefiting from future advancements in multiple fields."]},{"key":"dc:format.mimetype","label":"Dc Format Mimetype","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Solving Hybrid Boolean SAT by Continuous Optimization"]}]}],"canonical_facts":{"dc:contributor.advisor":["Vardi, Moshe Y."],"dc:creator":["Zhang, Zhiwei"],"dc:date.accessioned":["2025-09-11T16:09:33Z"],"dc:date.available":["2025-09-11T16:09:33Z"],"dc:date.issued":["2025-06-06"],"dc:description.abstract":["The Boolean SATisfiability problem (SAT) is of central importance in computer science. Despite the NP-completeness of SAT, progress on the engineering side—especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers—has been remarkable. Yet, while SAT solvers, aimed at solving industrial-scale benchmarks in Conjunctive Normal Form (CNF), have become quite mature, other types of non-CNF, i.e., hybrid constraints (e.g., cardinality/pseudo-Boolean constraints and XOR}s play important roles in critical applications such as cryptography, task scheduling, and quantum computing. Nevertheless, SAT solvers that are effective on hybrid constraints are less well studied; a general approach for handling hybrid constraints is still lacking. The thesis focuses on the applications and approaches for hybrid SAT solving. It starts with a motivating application of hybrid SAT solving in quantum computing. A smart hybrid SAT encoding is proposed to solve the problem with quantum interest. Then the thesis introduces efforts for addressing critical limitations of a continuous-optimization-based framework for hybrid SAT solving, named FourierSAT. In FourierSAT, Boolean constraints are converted into polynomials via Walsh-Hadamard-Fourier Transform and constrained continuous optimizers are then applied to search for a solution. FourierSAT suffers from slow gradient computation, incapability of handling pseudo-Boolean (PB) constraints, and the restriction to constrained optimizers, which together limit its potential. The thesis presents to use binary decision diagrams (BDDs) to replace polynomials, which significantly accelerates the gradient computation both in theory and practice, meanwhile handling PB constraints. The thesis then proposes an approach for removing the requirement of supporting constraints from the optimizers while still maintaining soundness, making FourierSAT compatible to several machine-learning-inspired optimizers. Empirical results demonstrate that the improved FourierSAT achieves promising performance on certain classes of applications and qualifies to be a useful complement to the SAT solver portfolio. This thesis further opens a solid research direction by bridging analysis of Boolean functions, continuous optimization and SAT solving. FourierSAT will continue benefiting from future advancements in multiple fields."],"dc:format.mimetype":["application/pdf"],"dc:identifier.uri":["https://hdl.handle.net/1911/118674"],"dc:language.iso":["eng"],"dc:rights":["Copyright is held by the author, unless otherwise indicated. Permission to reuse, publish, or reproduce the work beyond the bounds of fair use or other exemptions to copyright law must be obtained from the copyright holder."],"dc:subject":["SAT Solving","Continuous Optimization"],"dc:title":["Solving Hybrid Boolean SAT by Continuous Optimization"],"dc:type":["Thesis"],"thesis:degree_discipline":["Engineering"],"thesis:degree_level":["Doctoral"],"thesis:degree_name":["Doctor of Philosophy"],"thesis:institution_name":["Rice University"]},"updated_at":"2026-07-24T04:10:37Z"}