subject:(SAT)

1. Hiramoto, Shinya. A novel hardware SAT solver using non-chronological backtracking and clause recording : Non-chronologicalバックトラッキング及びclauseレコーディングを用いるハードウェアSATソルバ; Non-chronological バックトラッキングオヨビ clause レコーディングオモチイルハードウェア SAT ソルバ.

Degree: Nara Institute of Science and Technology / 奈良先端科学技術大学院大学

URL: http://hdl.handle.net/10061/4298

Subjects/Keywords: SAT

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Hiramoto, S. (n.d.). A novel hardware SAT solver using non-chronological backtracking and clause recording : Non-chronologicalバックトラッキング及びclauseレコーディングを用いるハードウェアSATソルバ; Non-chronological バックトラッキングオヨビ clause レコーディングオモチイルハードウェア SAT ソルバ. (Thesis). Nara Institute of Science and Technology / 奈良先端科学技術大学院大学. Retrieved from http://hdl.handle.net/10061/4298

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):

Hiramoto, Shinya. “A novel hardware SAT solver using non-chronological backtracking and clause recording : Non-chronologicalバックトラッキング及びclauseレコーディングを用いるハードウェアSATソルバ; Non-chronological バックトラッキングオヨビ clause レコーディングオモチイルハードウェア SAT ソルバ.” Thesis, Nara Institute of Science and Technology / 奈良先端科学技術大学院大学. Accessed March 07, 2021. http://hdl.handle.net/10061/4298.

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):

Hiramoto, Shinya. “A novel hardware SAT solver using non-chronological backtracking and clause recording : Non-chronologicalバックトラッキング及びclauseレコーディングを用いるハードウェアSATソルバ; Non-chronological バックトラッキングオヨビ clause レコーディングオモチイルハードウェア SAT ソルバ.” Web. 07 Mar 2021.

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

Vancouver:

Hiramoto S. A novel hardware SAT solver using non-chronological backtracking and clause recording : Non-chronologicalバックトラッキング及びclauseレコーディングを用いるハードウェアSATソルバ; Non-chronological バックトラッキングオヨビ clause レコーディングオモチイルハードウェア SAT ソルバ. [Internet] [Thesis]. Nara Institute of Science and Technology / 奈良先端科学技術大学院大学; [cited 2021 Mar 07]. Available from: http://hdl.handle.net/10061/4298.

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:

Hiramoto S. A novel hardware SAT solver using non-chronological backtracking and clause recording : Non-chronologicalバックトラッキング及びclauseレコーディングを用いるハードウェアSATソルバ; Non-chronological バックトラッキングオヨビ clause レコーディングオモチイルハードウェア SAT ソルバ. [Thesis]. Nara Institute of Science and Technology / 奈良先端科学技術大学院大学; Available from: http://hdl.handle.net/10061/4298

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

Wesleyan University

2. Chavez, Olivia. Diversity, Inequality and Predictive Power: Why Do Colleges Go SAT Optional?.

Degree: Psychology, 2016, Wesleyan University

URL: https://wesscholar.wesleyan.edu/etd_mas_theses/126

► Standardized testing is a controversial topic that has gained national attention from the press. Testing is an issue that impacts students from the moment… (more)

Subjects/Keywords: Diversity; College; SAT; SAT Optional; Test Optional

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Chavez, O. (2016). Diversity, Inequality and Predictive Power: Why Do Colleges Go SAT Optional?. (Masters Thesis). Wesleyan University. Retrieved from https://wesscholar.wesleyan.edu/etd_mas_theses/126

Chicago Manual of Style (16^th Edition):

Chavez, Olivia. “Diversity, Inequality and Predictive Power: Why Do Colleges Go SAT Optional?.” 2016. Masters Thesis, Wesleyan University. Accessed March 07, 2021. https://wesscholar.wesleyan.edu/etd_mas_theses/126.

MLA Handbook (7^th Edition):

Chavez, Olivia. “Diversity, Inequality and Predictive Power: Why Do Colleges Go SAT Optional?.” 2016. Web. 07 Mar 2021.

Vancouver:

Chavez O. Diversity, Inequality and Predictive Power: Why Do Colleges Go SAT Optional?. [Internet] [Masters thesis]. Wesleyan University; 2016. [cited 2021 Mar 07]. Available from: https://wesscholar.wesleyan.edu/etd_mas_theses/126.

Council of Science Editors:

Chavez O. Diversity, Inequality and Predictive Power: Why Do Colleges Go SAT Optional?. [Masters Thesis]. Wesleyan University; 2016. Available from: https://wesscholar.wesleyan.edu/etd_mas_theses/126

3. Reis, Poliana Magalhães. Análise da distribuição do número de operações de resolvedores SAT.

Degree: Mestrado, Ciência da Computação, 2012, University of São Paulo

URL: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-21012013-220441/ ;

►

No estudo da complexidade de problemas computacionais destacam-se duas classes conhecidas como P e NP. A questao P=NP e um dos maiores problemas nao resolvidos… (more)

▼

No estudo da complexidade de problemas computacionais destacam-se duas classes conhecidas como P e NP. A questao P=NP e um dos maiores problemas nao resolvidos em Ciencia da Compu- tacao teorica e Matematica contemporanea. O problema SAT foi o primeiro problema reconhecido como NP-completo e consiste em verificar se uma determinada formula da logica proposicional clas- sica e ou nao satisfazivel. As implementacoes de algoritmos para resolver problemas SAT sao conhe- cidas como resolvedores SAT (SAT Solvers). Existem diversas aplicacoes em Ciencia da Computacao que podem ser realizadas com SAT Solvers e com outros resolvedores de problemas NP-completos que podem ser reduzidos ao SAT como por exemplo problemas de coloracao de grafos, problemas de agendamento e problemas de planejamento. Dentre os mais eficientes algoritmos para resolvedores de SAT estao Sato, Grasp, Chaff, MiniSat e Berkmin. O Algoritmo Chaff e baseado no Algoritmo DPLL o qual existe a mais de 40 anos e e a estrategia mais utilizada para os Sat Solvers. Essa dissertacao apresenta um estudo aprofundado do comportamento do zChaff (uma implementacao muito eficiente do Chaff) para saber o que esperar de suas execucoes em geral .

In the study of computational complexity stand out two classes known as P and NP. The question P = NP is one of the greatest unsolved problems in theoretical computer science and contemporary mathematics. The SAT problem was first problem recognized as NP-complete and consists to check whether a certain formula of classical propositional logic is satisfiable or not. The implementations of algorithms to solve SAT problems are known as SAT solvers. There are several applications in computer science that can be performed with SAT solvers and other solvers NP- complete problems can be reduced to SAT problems such as graph coloring, scheduling problems and planning problems. Among the most efficient algorithms for SAT solvers are Sato, Grasp, Chaf, MiniSat and Berkmin. The Chaff algorithm is based on the DPLL algorithm which there is more than 40 years and is the most used strategy for Sat Solvers. This dissertation presents a detailed study of the behavior of zChaff (a very efficient implementation of the Chaff) to know what to expect from their performance in general.

Advisors/Committee Members: Finger, Marcelo.

Subjects/Keywords: Chaff; Chaff; NP-complete; NP-completo; P=NP; P=NP; SAT; SAT; SAT Solvers; SAT Solvers; zChaff.; zChaff.

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Reis, P. M. (2012). Análise da distribuição do número de operações de resolvedores SAT. (Masters Thesis). University of São Paulo. Retrieved from http://www.teses.usp.br/teses/disponiveis/45/45134/tde-21012013-220441/ ;

Chicago Manual of Style (16^th Edition):

Reis, Poliana Magalhães. “Análise da distribuição do número de operações de resolvedores SAT.” 2012. Masters Thesis, University of São Paulo. Accessed March 07, 2021. http://www.teses.usp.br/teses/disponiveis/45/45134/tde-21012013-220441/ ;.

MLA Handbook (7^th Edition):

Reis, Poliana Magalhães. “Análise da distribuição do número de operações de resolvedores SAT.” 2012. Web. 07 Mar 2021.

Vancouver:

Reis PM. Análise da distribuição do número de operações de resolvedores SAT. [Internet] [Masters thesis]. University of São Paulo; 2012. [cited 2021 Mar 07]. Available from: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-21012013-220441/ ;.

Council of Science Editors:

Reis PM. Análise da distribuição do número de operações de resolvedores SAT. [Masters Thesis]. University of São Paulo; 2012. Available from: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-21012013-220441/ ;

Université du Québec à Montréal

4. Monnet, Anthony Jean-Luc. Améliorer l'efficacité de l'algorithme CDCL : décompositions arborescentes de grandes instances, CDCL sans saut arrière et CDCL à ordre partiel.

Degree: 2013, Université du Québec à Montréal

URL: http://archipel.uqam.ca/5863/1/D2535.pdf

► Cette thèse s'intéresse à l'amélioration des performances pratiques de l'algorithme CDCL (Conftict-Driven Clause Learning) pour la résolution du problème de satisfaisabilité des formules propositionnelles, ou… (more)

Subjects/Keywords: Algorithme CDCL; Problème SAT

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Monnet, A. J. (2013). Améliorer l'efficacité de l'algorithme CDCL : décompositions arborescentes de grandes instances, CDCL sans saut arrière et CDCL à ordre partiel. (Thesis). Université du Québec à Montréal. Retrieved from http://archipel.uqam.ca/5863/1/D2535.pdf

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):

Monnet, Anthony Jean-Luc. “Améliorer l'efficacité de l'algorithme CDCL : décompositions arborescentes de grandes instances, CDCL sans saut arrière et CDCL à ordre partiel.” 2013. Thesis, Université du Québec à Montréal. Accessed March 07, 2021. http://archipel.uqam.ca/5863/1/D2535.pdf.

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

MLA Handbook (7^th Edition):

Monnet, Anthony Jean-Luc. “Améliorer l'efficacité de l'algorithme CDCL : décompositions arborescentes de grandes instances, CDCL sans saut arrière et CDCL à ordre partiel.” 2013. Web. 07 Mar 2021.

Vancouver:

Monnet AJ. Améliorer l'efficacité de l'algorithme CDCL : décompositions arborescentes de grandes instances, CDCL sans saut arrière et CDCL à ordre partiel. [Internet] [Thesis]. Université du Québec à Montréal; 2013. [cited 2021 Mar 07]. Available from: http://archipel.uqam.ca/5863/1/D2535.pdf.

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

Council of Science Editors:

Monnet AJ. Améliorer l'efficacité de l'algorithme CDCL : décompositions arborescentes de grandes instances, CDCL sans saut arrière et CDCL à ordre partiel. [Thesis]. Université du Québec à Montréal; 2013. Available from: http://archipel.uqam.ca/5863/1/D2535.pdf

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

Texas A&M University

5. Bian, Kun. Efficient Path Delay Test Generation with Boolean Satisfiability.

Degree: PhD, Computer Engineering, 2013, Texas A&M University

URL: http://hdl.handle.net/1969.1/151900

► This dissertation focuses on improving the accuracy and efficiency of path delay test generation using a Boolean satisfiability (SAT) solver. As part of this research,… (more)

Subjects/Keywords: Delay Test; ATPG; SAT

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Bian, K. (2013). Efficient Path Delay Test Generation with Boolean Satisfiability. (Doctoral Dissertation). Texas A&M University. Retrieved from http://hdl.handle.net/1969.1/151900

Chicago Manual of Style (16^th Edition):

Bian, Kun. “Efficient Path Delay Test Generation with Boolean Satisfiability.” 2013. Doctoral Dissertation, Texas A&M University. Accessed March 07, 2021. http://hdl.handle.net/1969.1/151900.

MLA Handbook (7^th Edition):

Bian, Kun. “Efficient Path Delay Test Generation with Boolean Satisfiability.” 2013. Web. 07 Mar 2021.

Vancouver:

Bian K. Efficient Path Delay Test Generation with Boolean Satisfiability. [Internet] [Doctoral dissertation]. Texas A&M University; 2013. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/1969.1/151900.

Council of Science Editors:

Bian K. Efficient Path Delay Test Generation with Boolean Satisfiability. [Doctoral Dissertation]. Texas A&M University; 2013. Available from: http://hdl.handle.net/1969.1/151900

University of Waterloo

6. Nejati, Saeed. CDCL(Crypto) and Machine Learning based SAT Solvers for Cryptanalysis.

Degree: 2020, University of Waterloo

URL: http://hdl.handle.net/10012/15868

► Over the last two decades, we have seen a dramatic improvement in the efficiency of conflict-driven clause-learning Boolean satisfiability (CDCL SAT) solvers over industrial problems… (more)

▼ Over the last two decades, we have seen a dramatic improvement in the efficiency of conflict-driven clause-learning Boolean satisfiability (CDCL SAT) solvers over industrial problems from a variety of applications such as verification, testing, security, and AI. The availability of such powerful general-purpose search tools as the SAT solver has led many researchers to propose SAT-based methods for cryptanalysis, including techniques for finding collisions in hash functions and breaking symmetric encryption schemes. A feature of all of the previously proposed SAT-based cryptanalysis work is that they are it{blackbox}, in the sense that the cryptanalysis problem is encoded as a SAT instance and then a CDCL SAT solver is invoked to solve said instance. A weakness of this approach is that the encoding thus generated may be too large for any modern solver to solve it efficiently. Perhaps a more important weakness of this approach is that the solver is in no way specialized or tuned to solve the given instance. Finally, very little work has been done to leverage parallelism in the context of SAT-based cryptanalysis. To address these issues, we developed a set of methods that improve on the state-of-the-art SAT-based cryptanalysis along three fronts. First, we describe an approach called \cdcl (inspired by the CDCL(T) paradigm) to tailor the internal subroutines of the CDCL SAT solver with domain-specific knowledge about cryptographic primitives. Specifically, we extend the propagation and conflict analysis subroutines of CDCL solvers with specialized codes that have knowledge about the cryptographic primitive being analyzed by the solver. We demonstrate the power of this framework in two cryptanalysis tasks of algebraic fault attack and differential cryptanalysis of SHA-1 and SHA-256 cryptographic hash functions. Second, we propose a machine-learning based parallel SAT solver that performs well on cryptographic problems relative to many state-of-the-art parallel SAT solvers. Finally, we use a formulation of SAT into Bayesian moment matching to address heuristic initialization problem in SAT solvers.

Subjects/Keywords: SAT Solvers; Cryptography; machine learning

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Nejati, S. (2020). CDCL(Crypto) and Machine Learning based SAT Solvers for Cryptanalysis. (Thesis). University of Waterloo. Retrieved from http://hdl.handle.net/10012/15868

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):

Nejati, Saeed. “CDCL(Crypto) and Machine Learning based SAT Solvers for Cryptanalysis.” 2020. Thesis, University of Waterloo. Accessed March 07, 2021. http://hdl.handle.net/10012/15868.

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

MLA Handbook (7^th Edition):

Nejati, Saeed. “CDCL(Crypto) and Machine Learning based SAT Solvers for Cryptanalysis.” 2020. Web. 07 Mar 2021.

Vancouver:

Nejati S. CDCL(Crypto) and Machine Learning based SAT Solvers for Cryptanalysis. [Internet] [Thesis]. University of Waterloo; 2020. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/10012/15868.

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

Council of Science Editors:

Nejati S. CDCL(Crypto) and Machine Learning based SAT Solvers for Cryptanalysis. [Thesis]. University of Waterloo; 2020. Available from: http://hdl.handle.net/10012/15868

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

University of Toronto

7. Liu, Feiyuan. Indenpendent Transcription of a Functional Lucerne Transient Streak Virus Satellite RNA and its Packaging Requirement(s).

Degree: 2014, University of Toronto

URL: http://hdl.handle.net/1807/68863

►

The satellite RNA of Lucerne Transient Streak Virus (LTSV) is a 322-nucleotide, single-stranded circular RNA. To investigate whether interactions between genomic and satellite RNA are… (more)

Subjects/Keywords: functional; packaging; sat RNA; 0720

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Liu, F. (2014). Indenpendent Transcription of a Functional Lucerne Transient Streak Virus Satellite RNA and its Packaging Requirement(s). (Masters Thesis). University of Toronto. Retrieved from http://hdl.handle.net/1807/68863

Chicago Manual of Style (16^th Edition):

Liu, Feiyuan. “Indenpendent Transcription of a Functional Lucerne Transient Streak Virus Satellite RNA and its Packaging Requirement(s).” 2014. Masters Thesis, University of Toronto. Accessed March 07, 2021. http://hdl.handle.net/1807/68863.

MLA Handbook (7^th Edition):

Liu, Feiyuan. “Indenpendent Transcription of a Functional Lucerne Transient Streak Virus Satellite RNA and its Packaging Requirement(s).” 2014. Web. 07 Mar 2021.

Vancouver:

Liu F. Indenpendent Transcription of a Functional Lucerne Transient Streak Virus Satellite RNA and its Packaging Requirement(s). [Internet] [Masters thesis]. University of Toronto; 2014. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/1807/68863.

Council of Science Editors:

Liu F. Indenpendent Transcription of a Functional Lucerne Transient Streak Virus Satellite RNA and its Packaging Requirement(s). [Masters Thesis]. University of Toronto; 2014. Available from: http://hdl.handle.net/1807/68863

Colorado State University

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

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

URL: http://hdl.handle.net/10217/189292

► 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 07, 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. 07 Mar 2021.

Vancouver:

Chen W. Discovering and harnessing structures in solving application satisfiability instances. [Internet] [Doctoral dissertation]. Colorado State University; 2018. [cited 2021 Mar 07]. 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

University of Debrecen

9. Bécsi, Zoltán József. Intervallumokon végzett számítások .

Degree: DE – TEK – Informatikai Kar, 2009, University of Debrecen

URL: http://hdl.handle.net/2437/86287

Intervallum alapú logika, intervallumokkal végzett műveletek, SAT probléma megoldása intervallumokkal lineáris időben Advisors/Committee Members: Nagy, Benedek (advisor).

Subjects/Keywords: Intervallum; SAT

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Bécsi, Z. J. (2009). Intervallumokon végzett számítások . (Thesis). University of Debrecen. Retrieved from http://hdl.handle.net/2437/86287

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):

Bécsi, Zoltán József. “Intervallumokon végzett számítások .” 2009. Thesis, University of Debrecen. Accessed March 07, 2021. http://hdl.handle.net/2437/86287.

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

MLA Handbook (7^th Edition):

Bécsi, Zoltán József. “Intervallumokon végzett számítások .” 2009. Web. 07 Mar 2021.

Vancouver:

Bécsi ZJ. Intervallumokon végzett számítások . [Internet] [Thesis]. University of Debrecen; 2009. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/2437/86287.

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

Council of Science Editors:

Bécsi ZJ. Intervallumokon végzett számítások . [Thesis]. University of Debrecen; 2009. Available from: http://hdl.handle.net/2437/86287

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

University of Florida

10. Hasbini, Leena. The Impact of Standardized Testing on High-Achieving Students Postsecondary Acceptance Outcomes.

Degree: EdD, Educational Leadership - Human Development and Organizational Studies in Education, 2018, University of Florida

URL: https://ufdc.ufl.edu/UFE0052157

► Standardized testing, specifically geared toward postsecondary admission, such as the SAT and ACT, were designed to measure readiness for higher education. The purpose of this… (more)

Subjects/Keywords: act – admissions – college – sat – testing

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Hasbini, L. (2018). The Impact of Standardized Testing on High-Achieving Students Postsecondary Acceptance Outcomes. (Doctoral Dissertation). University of Florida. Retrieved from https://ufdc.ufl.edu/UFE0052157

Chicago Manual of Style (16^th Edition):

Hasbini, Leena. “The Impact of Standardized Testing on High-Achieving Students Postsecondary Acceptance Outcomes.” 2018. Doctoral Dissertation, University of Florida. Accessed March 07, 2021. https://ufdc.ufl.edu/UFE0052157.

MLA Handbook (7^th Edition):

Hasbini, Leena. “The Impact of Standardized Testing on High-Achieving Students Postsecondary Acceptance Outcomes.” 2018. Web. 07 Mar 2021.

Vancouver:

Hasbini L. The Impact of Standardized Testing on High-Achieving Students Postsecondary Acceptance Outcomes. [Internet] [Doctoral dissertation]. University of Florida; 2018. [cited 2021 Mar 07]. Available from: https://ufdc.ufl.edu/UFE0052157.

Council of Science Editors:

Hasbini L. The Impact of Standardized Testing on High-Achieving Students Postsecondary Acceptance Outcomes. [Doctoral Dissertation]. University of Florida; 2018. Available from: https://ufdc.ufl.edu/UFE0052157

11. -5591-465X. Using a statistical model to predict student success in Texas Woman's University mathematics program.

Degree: MS, Mathematics, 2018, Texas Woman's University

URL: http://hdl.handle.net/11274/10741

► Admission applications from high school students are received yearly by colleges but majority of the students that are being admitted eventually do not graduate. Colleges… (more)

Subjects/Keywords: Predict; Mathematics; Graduation; SAT mathematics

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

-5591-465X. (2018). Using a statistical model to predict student success in Texas Woman's University mathematics program. (Masters Thesis). Texas Woman's University. Retrieved from http://hdl.handle.net/11274/10741

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

Chicago Manual of Style (16^th Edition):

-5591-465X. “Using a statistical model to predict student success in Texas Woman's University mathematics program.” 2018. Masters Thesis, Texas Woman's University. Accessed March 07, 2021. http://hdl.handle.net/11274/10741.

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

MLA Handbook (7^th Edition):

-5591-465X. “Using a statistical model to predict student success in Texas Woman's University mathematics program.” 2018. Web. 07 Mar 2021.

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

Vancouver:

-5591-465X. Using a statistical model to predict student success in Texas Woman's University mathematics program. [Internet] [Masters thesis]. Texas Woman's University; 2018. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/11274/10741.

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

Council of Science Editors:

-5591-465X. Using a statistical model to predict student success in Texas Woman's University mathematics program. [Masters Thesis]. Texas Woman's University; 2018. Available from: http://hdl.handle.net/11274/10741

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

Universidade do Rio Grande do Sul

12. Silveira, Jaime Kirch da. Parallel SAT solvers and their application in automatic parallelization.

Degree: 2014, Universidade do Rio Grande do Sul

URL: http://hdl.handle.net/10183/95373

►

Since the slowdown in improvement in the frequency of processors, a new tendency has arisen to allow software to take advantage of faster hardware: parallelization.… (more)

▼

Since the slowdown in improvement in the frequency of processors, a new tendency has arisen to allow software to take advantage of faster hardware: parallelization. However, different from increasing the frequency of processors, using parallelization requires a different kind of programming, parallel programming, which is usually harder than common sequential programming. In this context, automatic parallelization has arisen, allowing software to take advantage of parallelism without the need of parallel programming. We present here two proposals: SAT-PaDdlinG and RePaSAT. SAT-PaDdlinG is a parallel DPLL SAT Solver on GPU, which allows RePaSAT to use this environment. RePaSAT is our proposal of a parallel machine that uses the SAT Problem to automatically parallelize sequential code. Because GPU provides a cheap, massively parallel environment, SATPaDdlinG aims at providing this massive parallelism and low cost to RePaSAT, as well as to any other tool or problem that uses SAT Solvers.

Desde a diminuição da tendência de aumento na frequência de processadores, uma nova tendência surgiu para permitir que softwares tirem proveito de harwares mais rápidos: a paralelização. Contudo, diferente de aumentar a frequência de processadores, utilizar parallelização requer um tipo diferente de programação, a programação paralela, que é geralmente mais difícil que a programação sequencial comum. Neste contexto, a paralelização automática apareceu, permitindo que o software tire proveito do paralelismo sem a necessidade de programação paralela. Nós apresentamos aqui duas propostas: SAT-PaDdlinG e RePaSAT. SAT-PaDdlinG é um SAT Solver DPLL paralelo que roda em GPU, o que permite que RePaSAT utilize esse ambiente. RePaSAT é a nossa proposta de uma máquina paralela que utiliza o Problema SAT para paralelizar automaticamente código sequencial. Como uma GPU provê um ambiente barato e massivamente paralelo, SAT-PaDdlinG tem como objetivo prover esse paralelismo massivo a baixo custo para RePaSAT, como para qualquer outra ferramenta ou problema que utilize SAT Solvers.

Advisors/Committee Members: Carro, Luigi.

Subjects/Keywords: Microeletrônica; Parallel SAT solver; Processadores; Automatic parallelization; RePaSAT; SAT-PaDdlinG

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Silveira, J. K. d. (2014). Parallel SAT solvers and their application in automatic parallelization. (Thesis). Universidade do Rio Grande do Sul. Retrieved from http://hdl.handle.net/10183/95373

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):

Silveira, Jaime Kirch da. “Parallel SAT solvers and their application in automatic parallelization.” 2014. Thesis, Universidade do Rio Grande do Sul. Accessed March 07, 2021. http://hdl.handle.net/10183/95373.

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

MLA Handbook (7^th Edition):

Silveira, Jaime Kirch da. “Parallel SAT solvers and their application in automatic parallelization.” 2014. Web. 07 Mar 2021.

Vancouver:

Silveira JKd. Parallel SAT solvers and their application in automatic parallelization. [Internet] [Thesis]. Universidade do Rio Grande do Sul; 2014. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/10183/95373.

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

Council of Science Editors:

Silveira JKd. Parallel SAT solvers and their application in automatic parallelization. [Thesis]. Universidade do Rio Grande do Sul; 2014. Available from: http://hdl.handle.net/10183/95373

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

13. Al-Saedi, Mohammad Saleh Balasim. Extensions of tractable classes for propositional satisfiability : Extensions de classes polynomiales pour le problème de satisfaisabilité.

Degree: Docteur es, Informatique, 2016, Université d'Artois

URL: http://www.theses.fr/2016ARTO0405

►

La représentation des connaissances et les problèmes d’inférence associés restent à l’heure actuelle une problématique riche et centrale en informatique et plus précisément en intelligence… (more)

▼

La représentation des connaissances et les problèmes d’inférence associés restent à l’heure actuelle une problématique riche et centrale en informatique et plus précisément en intelligence artificielle. Dans ce cadre, la logique propositionnelle permet d’allier puissance d’expression et efficacité. Il reste que, tant que P est différent de NP, la déduction en logique propositionnelle ne peut admettre de solutions à la fois générales et efficaces. Dans cette thèse, nous adressons le problème de satisfiabilité et proposons de nouvelles classes d’instances pouvant être résolues de manière polynomiale.La découverte de nouvelles classes polynomiales pour SAT est à la fois importante d’un point de vue théorique et pratique. En effet, on peut espérer les exploiter efficacement au sein de solveurs SAT. Dans cette thèse, nous proposons d’étendre deux fragments polynomiaux de SAT à l’aide de la propagation unitaire tout en s’assurant que ces fragments demeurent reconnus et résolus de manière polynomiale. Le premier résultat de cette thèse concerne la classe Quad. Nous avons établi certaines propriétés de cette classe d’instances et avons étendu cette dernière de manière à s’abstraire de l’ordre imposé sur les littéraux. Le fragment obtenu en remplaçant cet ordre par différents ordres sur les clauses, conserve lamême complexité dans le pire cas. Nous avons également étudié l’impact de la résolution bornée et de la redondance par propagation unitaire sur cette classe. La seconde contribution concerne la classe polynomiale proposée par Tovey. La propagation unitaire est une nouvelle fois utilisée pour étendre cette classe. Nous comparons le nouveau fragment polynomial obtenu à deux autres classes basées également sur la propagation unitaire : Quad et UP-Horn. Nousapportons également une réponse à une question ouverte au sujet des connexions de ces classes. Nous montrons que UP-Horn et d’autres classes basées sur la propagation unitaire sont strictement incluses dans S Quad qui représente l’union de toutes les classes Quad obtenues par l’exploitation de tous les ordres sur les clauses possibles.

Knowledge representation and reasoning is a key issue in computer science and more particularly in artificial intelligence. In this respect, propositional logic is a representation formalism that is a good trade-off between the opposite computational efficiency and expressiveness criteria. However, unless P = NP, deduction in propositional logic is not polynomial in the worst case. So, in this thesis we propose new extensions of tractable classes of the propositional satisfiability problem. Tractable fragments of SAT play a role in the implementation of the most efficient current SAT solvers, many of thesetractable classes use the linear time unit propagation (UP) inference rule. We attempt to extend two of currently-known polynomial fragments of SAT thanks to UP in such a way that the fragments can still be recognized and solved in polynomial time. A first result focuses on Quad fragments: we establish some properties of Quad fragments…

Advisors/Committee Members: Grégoire, Eric (thesis director), Mazure, Bertrand (thesis director), Saïs, Lakhdar (thesis director).

Subjects/Keywords: Logique propositionnelle; SAT; Classes polynomiales; Propositional logic; SAT; Tractable classes; 006.3

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Al-Saedi, M. S. B. (2016). Extensions of tractable classes for propositional satisfiability : Extensions de classes polynomiales pour le problème de satisfaisabilité. (Doctoral Dissertation). Université d'Artois. Retrieved from http://www.theses.fr/2016ARTO0405

Chicago Manual of Style (16^th Edition):

Al-Saedi, Mohammad Saleh Balasim. “Extensions of tractable classes for propositional satisfiability : Extensions de classes polynomiales pour le problème de satisfaisabilité.” 2016. Doctoral Dissertation, Université d'Artois. Accessed March 07, 2021. http://www.theses.fr/2016ARTO0405.

MLA Handbook (7^th Edition):

Al-Saedi, Mohammad Saleh Balasim. “Extensions of tractable classes for propositional satisfiability : Extensions de classes polynomiales pour le problème de satisfaisabilité.” 2016. Web. 07 Mar 2021.

Vancouver:

Al-Saedi MSB. Extensions of tractable classes for propositional satisfiability : Extensions de classes polynomiales pour le problème de satisfaisabilité. [Internet] [Doctoral dissertation]. Université d'Artois; 2016. [cited 2021 Mar 07]. Available from: http://www.theses.fr/2016ARTO0405.

Council of Science Editors:

Al-Saedi MSB. Extensions of tractable classes for propositional satisfiability : Extensions de classes polynomiales pour le problème de satisfaisabilité. [Doctoral Dissertation]. Université d'Artois; 2016. Available from: http://www.theses.fr/2016ARTO0405

Brno University of Technology

14. Izrael, Petr. SAT Solver akcelerovaný pomocí GPU: GPU Accelerated SAT Solver.

Degree: 2019, Brno University of Technology

URL: http://hdl.handle.net/11012/53479

► This thesis is concerned with design and implementation of a complete SAT solver accelerated on GPU. The achitecture of modern graphics cards is described as… (more)

Subjects/Keywords: SAT; DPLL; CUDA; GPU; GPGPU; SAT; DPLL; CUDA; GPU; GPGPU

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Izrael, P. (2019). SAT Solver akcelerovaný pomocí GPU: GPU Accelerated SAT Solver. (Thesis). Brno University of Technology. Retrieved from http://hdl.handle.net/11012/53479

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):

Izrael, Petr. “SAT Solver akcelerovaný pomocí GPU: GPU Accelerated SAT Solver.” 2019. Thesis, Brno University of Technology. Accessed March 07, 2021. http://hdl.handle.net/11012/53479.

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

MLA Handbook (7^th Edition):

Izrael, Petr. “SAT Solver akcelerovaný pomocí GPU: GPU Accelerated SAT Solver.” 2019. Web. 07 Mar 2021.

Vancouver:

Izrael P. SAT Solver akcelerovaný pomocí GPU: GPU Accelerated SAT Solver. [Internet] [Thesis]. Brno University of Technology; 2019. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/11012/53479.

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

Council of Science Editors:

Izrael P. SAT Solver akcelerovaný pomocí GPU: GPU Accelerated SAT Solver. [Thesis]. Brno University of Technology; 2019. Available from: http://hdl.handle.net/11012/53479

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

Rice University

15. Meel, Kuldeep Singh. Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice.

Degree: PhD, Engineering, 2017, Rice University

URL: http://hdl.handle.net/1911/105480

► Constrained counting and sampling are two fundamental problems in Computer Science with numerous applications, including network reliability, privacy, probabilistic reasoning, and constrained-random verification. In constrained… (more)

▼ Constrained counting and sampling are two fundamental problems in Computer Science with numerous applications, including network reliability, privacy, probabilistic reasoning, and constrained-random verification. In constrained counting, the task is to compute the total weight, subject to a given weighting function, of the set of solutions of the given constraints. In constrained sampling, the task is to sample randomly, subject to a given weighting function, from the set of solutions to a set of given constraints. Consequently, Constrained counting and sampling have been subject to intense theoretical and empirical investigations over the years. Prior work, however, offered either heuristic techniques with poor guarantees of accuracy or approaches with proven guarantees but poor performance in practice. In this thesis, we introduce a novel hashing-based algorithmic framework for constrained sampling and counting that combines the classical algorithmic technique of universal hashing with the dramatic progress made in Boolean reasoning solving, in particular, {\SAT} and {\SMT}, over the past two decades. By exploiting the connection between definability of formulas and variance of the distribution of solutions in a cell defined by 3-universal hash functions, we introduced an algorithmic technique, {\MIS}, that reduced the size of XOR constraints employed in the underlying universal hash functions by as much as two orders of magnitude. The resulting frameworks for counting ( {\ScalApproxMC}) and sampling ({\UniGen}) can handle formulas with up to million variables representing a significant boost up from the prior state of the art tools' capability to handle few hundreds of variables. If the initial set of constraints is expressed as Disjunctive Normal Form (DNF), {\ScalApproxMC} is the only known Fully Polynomial Randomized Approximation Scheme (FPRAS) that does not involve Monte Carlo steps. We demonstrate the utility of the above techniques on various real applications including probabilistic inference, design verification and estimating the reliability of critical infrastructure networks during natural disasters. The high parallelizability of our approach opens up new directions for development of artificial intelligence tools that can effectively leverage high-performance computing resources. Advisors/Committee Members: Chakraborty, Supratik (advisor), Chaudhuri, Swarat (committee member), Duenas-Osorio, Leonardo (committee member), Seshia, Sanjit A. (committee member), Vardi, Moshe Y. (committee member).

Subjects/Keywords: Constrained Counting; Constrained Sampling; SAT; universal hashing; SAT; SMT

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Meel, K. S. (2017). Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice. (Doctoral Dissertation). Rice University. Retrieved from http://hdl.handle.net/1911/105480

Chicago Manual of Style (16^th Edition):

Meel, Kuldeep Singh. “Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice.” 2017. Doctoral Dissertation, Rice University. Accessed March 07, 2021. http://hdl.handle.net/1911/105480.

MLA Handbook (7^th Edition):

Meel, Kuldeep Singh. “Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice.” 2017. Web. 07 Mar 2021.

Vancouver:

Meel KS. Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice. [Internet] [Doctoral dissertation]. Rice University; 2017. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/1911/105480.

Council of Science Editors:

Meel KS. Constrained Counting and Sampling: Bridging the Gap Between Theory and Practice. [Doctoral Dissertation]. Rice University; 2017. Available from: http://hdl.handle.net/1911/105480

University of Waterloo

16. Salmon, Ricardo. On the relationship between satisfiability and partially observable Markov decision processes.

Degree: 2018, University of Waterloo

URL: http://hdl.handle.net/10012/13951

► Stochastic satisfiability (SSAT), Quantified Boolean Satisfiability (QBF) and decision-theoretic planning in finite horizon partially observable Markov decision processes (POMDPs) are all PSPACE-Complete problems. Since they… (more)

Subjects/Keywords: POMDP; Stochastic SAT; Satisfiability; Planning; Probabilistic Inference; SAT; QBF

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Salmon, R. (2018). On the relationship between satisfiability and partially observable Markov decision processes. (Thesis). University of Waterloo. Retrieved from http://hdl.handle.net/10012/13951

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):

Salmon, Ricardo. “On the relationship between satisfiability and partially observable Markov decision processes.” 2018. Thesis, University of Waterloo. Accessed March 07, 2021. http://hdl.handle.net/10012/13951.

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

MLA Handbook (7^th Edition):

Salmon, Ricardo. “On the relationship between satisfiability and partially observable Markov decision processes.” 2018. Web. 07 Mar 2021.

Vancouver:

Salmon R. On the relationship between satisfiability and partially observable Markov decision processes. [Internet] [Thesis]. University of Waterloo; 2018. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/10012/13951.

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

Council of Science Editors:

Salmon R. On the relationship between satisfiability and partially observable Markov decision processes. [Thesis]. University of Waterloo; 2018. Available from: http://hdl.handle.net/10012/13951

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

University of Alberta

17. Chowdhury, Md Solimul. SAT with Global Constraints.

Degree: MS, Department of Computing Science, 2011, University of Alberta

URL: https://era.library.ualberta.ca/files/ws859f77v

► Propositional satisability (SAT) has been a dominant tool in solving some practical NP-complete problems. However, SAT also has a number of weaknesses, including its inability… (more)

Subjects/Keywords: Constraint Programming; Global Constraints; Integration; SAT

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Chowdhury, M. S. (2011). SAT with Global Constraints. (Masters Thesis). University of Alberta. Retrieved from https://era.library.ualberta.ca/files/ws859f77v

Chicago Manual of Style (16^th Edition):

Chowdhury, Md Solimul. “SAT with Global Constraints.” 2011. Masters Thesis, University of Alberta. Accessed March 07, 2021. https://era.library.ualberta.ca/files/ws859f77v.

MLA Handbook (7^th Edition):

Chowdhury, Md Solimul. “SAT with Global Constraints.” 2011. Web. 07 Mar 2021.

Vancouver:

Chowdhury MS. SAT with Global Constraints. [Internet] [Masters thesis]. University of Alberta; 2011. [cited 2021 Mar 07]. Available from: https://era.library.ualberta.ca/files/ws859f77v.

Council of Science Editors:

Chowdhury MS. SAT with Global Constraints. [Masters Thesis]. University of Alberta; 2011. Available from: https://era.library.ualberta.ca/files/ws859f77v

Texas A&M University

18. Deng, Yue. SAT-based Verification for Analog and Mixed-signal Circuits.

Degree: MS, Computer Engineering, 2012, Texas A&M University

URL: http://hdl.handle.net/1969.1/ETD-TAMU-2012-05-11221

► The wide application of analog and mixed-signal (AMS) designs makes the verification of AMS circuits an important task. However, verification of AMS circuits remains as… (more)

▼ The wide application of analog and mixed-signal (AMS) designs makes the verification of AMS circuits an important task. However, verification of AMS circuits remains as a significant challenge even though verification techniques for digital circuits design have been successfully applied in the semiconductor industry. In this thesis, we propose two techniques for AMS verification targeting DC and transient verifications, respectively. The proposed techniques leverage a combination of circuit modeling, satisfiability (SAT) and circuit simulation techniques. For DC verification, we first build bounded device models for transistors. The bounded models are conservative approximations to the accurate BSIM3/4 models. Then we formulate a circuit verification problem by gathering the circuit's KCL/KVL equations and the I-V characteristics which are constrained by the bounded models. A nonlinear SAT solver is then recursively applied to the problem formula to locate a candidate region which is guaranteed to enclose the actual DC equilibrium of the original circuit. In the end, a refinement technique is applied to reduce the size of candidate region to a desired resolution. To demonstrate the application of the proposed DC verification technique, we apply it to locate the DC equilibrium points for a set of ring oscillators. The experimental results show that the proposed DC verification technique is efficient in terms of runtime. For transient verification, we perform reachability analysis to verify the dynamic property of a circuit. Our method combines circuit simulation SAT to take advantage of the efficiency of simulation and the soundness of SAT. The novelty of the proposed transient verification lies in the fact that a significant part of the reachable state space is discovered via fast simulation while the full coverage of the reachable state space is guaranteed by the invoking of a few SAT runs. Furthermore, a box merging algorithm is presented to efficiently represent the reachable state space using grid boxes. The proposed technique is used to verify the startup condition of a tunnel diode oscillator and the phase-locking of a phase-locked loop (PLL). The experimental results demonstrate that the proposed transient verification technique can perform reachability analysis for reasonable complex circuits over a great number of time steps. Advisors/Committee Members: Li, Peng (advisor), Silva-Martinez, Jose (committee member), Walker, Duncan M. (committee member).

Subjects/Keywords: Analog; verification; simulation; SAT; modeling; reachability anlysis

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Deng, Y. (2012). SAT-based Verification for Analog and Mixed-signal Circuits. (Masters Thesis). Texas A&M University. Retrieved from http://hdl.handle.net/1969.1/ETD-TAMU-2012-05-11221

Chicago Manual of Style (16^th Edition):

Deng, Yue. “SAT-based Verification for Analog and Mixed-signal Circuits.” 2012. Masters Thesis, Texas A&M University. Accessed March 07, 2021. http://hdl.handle.net/1969.1/ETD-TAMU-2012-05-11221.

MLA Handbook (7^th Edition):

Deng, Yue. “SAT-based Verification for Analog and Mixed-signal Circuits.” 2012. Web. 07 Mar 2021.

Vancouver:

Deng Y. SAT-based Verification for Analog and Mixed-signal Circuits. [Internet] [Masters thesis]. Texas A&M University; 2012. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/1969.1/ETD-TAMU-2012-05-11221.

Council of Science Editors:

Deng Y. SAT-based Verification for Analog and Mixed-signal Circuits. [Masters Thesis]. Texas A&M University; 2012. Available from: http://hdl.handle.net/1969.1/ETD-TAMU-2012-05-11221

Universidad de Chile

19. Carmi Jara, Víctor Andrés. Consultas eficientes sobre bases de datos de grafo incompletas.

Degree: 2013, Universidad de Chile

URL: http://repositorio.uchile.cl/handle/2250/115697

► El principal objetivo de esta tesis es encontrar casos tratables y buenas técnicas para computar Certain Answers sobre bases de datos de grafos incompletas, en… (more)

Subjects/Keywords: Bases de datos; Certain Answers; 3-SAT

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Carmi Jara, V. A. (2013). Consultas eficientes sobre bases de datos de grafo incompletas. (Thesis). Universidad de Chile. Retrieved from http://repositorio.uchile.cl/handle/2250/115697

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):

Carmi Jara, Víctor Andrés. “Consultas eficientes sobre bases de datos de grafo incompletas.” 2013. Thesis, Universidad de Chile. Accessed March 07, 2021. http://repositorio.uchile.cl/handle/2250/115697.

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

MLA Handbook (7^th Edition):

Carmi Jara, Víctor Andrés. “Consultas eficientes sobre bases de datos de grafo incompletas.” 2013. Web. 07 Mar 2021.

Vancouver:

Carmi Jara VA. Consultas eficientes sobre bases de datos de grafo incompletas. [Internet] [Thesis]. Universidad de Chile; 2013. [cited 2021 Mar 07]. Available from: http://repositorio.uchile.cl/handle/2250/115697.

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

Council of Science Editors:

Carmi Jara VA. Consultas eficientes sobre bases de datos de grafo incompletas. [Thesis]. Universidad de Chile; 2013. Available from: http://repositorio.uchile.cl/handle/2250/115697

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

Brno University of Technology

20. Serédi, Silvester. Evoluční algoritmy v úloze booleovské splnitelnosti: Evolutionary Algorithms in the Task of Boolean Satisfiability.

Degree: 2018, Brno University of Technology

URL: http://hdl.handle.net/11012/53467

► The goal of this Master's Thesis is finding a SAT solving heuristic by the application of an evolutionary algorithm. This thesis surveys various approaches used… (more)

Subjects/Keywords: Genetické programovanie; evolučné algoritmy; zložitosť; SAT problém; NP-úplný problém; SAT solver.; Genetic programming; evolutionary algorithms; complexity; SAT problem; NP-complete problem; SAT solver.

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Serédi, S. (2018). Evoluční algoritmy v úloze booleovské splnitelnosti: Evolutionary Algorithms in the Task of Boolean Satisfiability. (Thesis). Brno University of Technology. Retrieved from http://hdl.handle.net/11012/53467

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):

Serédi, Silvester. “Evoluční algoritmy v úloze booleovské splnitelnosti: Evolutionary Algorithms in the Task of Boolean Satisfiability.” 2018. Thesis, Brno University of Technology. Accessed March 07, 2021. http://hdl.handle.net/11012/53467.

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

MLA Handbook (7^th Edition):

Serédi, Silvester. “Evoluční algoritmy v úloze booleovské splnitelnosti: Evolutionary Algorithms in the Task of Boolean Satisfiability.” 2018. Web. 07 Mar 2021.

Vancouver:

Serédi S. Evoluční algoritmy v úloze booleovské splnitelnosti: Evolutionary Algorithms in the Task of Boolean Satisfiability. [Internet] [Thesis]. Brno University of Technology; 2018. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/11012/53467.

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

Council of Science Editors:

Serédi S. Evoluční algoritmy v úloze booleovské splnitelnosti: Evolutionary Algorithms in the Task of Boolean Satisfiability. [Thesis]. Brno University of Technology; 2018. Available from: http://hdl.handle.net/11012/53467

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

Université de Lorraine

21. Bousmar, Khadija. Conception d'un solveur matériel spécifique pour la résolution rapide du problème SAT appliqué à l'évaluation du risque en génie industriel : Design of a specific hardware solver for a speed resolution of the SAT problem applied to risk assessment in industrial engineering.

Degree: Docteur es, Automatique, Traitement du Signal et des Images, Génie Informatique, 2018, Université de Lorraine

URL: http://www.theses.fr/2018LORR0341

►

Dans cette thèse, nous abordons un sujet dans le domaine du génie industriel se rapportant à la résolution d’un problème de décision, fondamental dans la… (more)

▼

Dans cette thèse, nous abordons un sujet dans le domaine du génie industriel se rapportant à la résolution d’un problème de décision, fondamental dans la théorie de la complexité et de la satisfiabilité propositionnelle, nommé SAT. Ce dernier est présenté généralement sous un formalisme mathématique, permettant de modéliser des problèmes complexes, tant académiques qu’issus du monde réel. Ces problèmes sont présentés sous une forme booléenne dans le but de tester leur faisabilité. Ils sont relatifs à plusieurs domaines applicatifs, tels que la vérification de matériels et logiciels, les télécommunications, la médecine, et notamment la planification. L’évolution et les progrès observés ces dernières années dans le domaine de la résolution des problèmes utilisant SAT, a permis de renforcer la conviction que ce domaine peut être encore plus prometteur dans la résolution des problèmes difficiles (complexes ou NP complexes) et qu’il faut lui accorder plus d’intérêt. C’est dans cette optique, que nous nous sommes intéressés à l’appliquer sur des problèmes purement industriels afin de proposer des contributions dans un nouveau domaine d’application. L’objectif de cette thèse est de développer des outils d’aide à la décision pouvant être employés dans le domaine de la gestion du risque industriel. Bien que le formalisme SAT soit très puissant, dans la pratique, quand les problèmes ciblés sont de taille importante, les outils de résolution s’avèrent moins performants. Par conséquent le but de ces travaux de recherche est de développer une architecture matérielle rapide (avec une implémentation ciblée sur FPGA) permettant une accélération massive de la résolution grâce au niveau élevé de traitement parallèle de l’approche matérielle. Dans cette thèse, deux aspects principaux sont étudiés et développés pour résoudre un problème de gestion des ressources de production industriel. Ces aspects sont d’une part, les principes de base de fonctionnement et de résolution d’un solveur générique paramétrable SAT, d’autre part, des méthodes adaptées au principe de fonctionnement retenu pour le solveur matériel. En effet, bien que ciblant des buts comparables à ceux de l’approche logicielle (optimisation du parcours de l’espace de recherche), l’approche matérielle requiert le développement de méthodes de résolutions spécifiques. Ces dernières ont été spécifiquement optimisées pour le domaine applicatif cible qui est celui de l’industrie. L’efficacité de l’approche matérielle développée a montré des résultats satisfaisant, point de vu du nombre de variables utilisés et temps de résolution sur les problèmes testés.

In this thesis, we address a topic in the field of industrial engineering related to solving a fundamental decision problem in the theory of complexity and propositional satisfiability called SAT. The latter is usually presented in a mathematical formalism, allowing the modelling of complex problems, both academic and from real world. These problems are presented in boolean form in order to check their feasibility. They relate…

Advisors/Committee Members: Dellagi, Sofiène (thesis director), Monteiro, Fabrice (thesis director).

Subjects/Keywords: SAT; Solveur SAT; Gestion du risque industriel; Problème combinatoire; Architecture matérielle de calcul; SAT; SAT Solver; Industrial risk management; Combinatorial problem; Hardware computing architecture; 620.004 2; 005.12

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Bousmar, K. (2018). Conception d'un solveur matériel spécifique pour la résolution rapide du problème SAT appliqué à l'évaluation du risque en génie industriel : Design of a specific hardware solver for a speed resolution of the SAT problem applied to risk assessment in industrial engineering. (Doctoral Dissertation). Université de Lorraine. Retrieved from http://www.theses.fr/2018LORR0341

Chicago Manual of Style (16^th Edition):

Bousmar, Khadija. “Conception d'un solveur matériel spécifique pour la résolution rapide du problème SAT appliqué à l'évaluation du risque en génie industriel : Design of a specific hardware solver for a speed resolution of the SAT problem applied to risk assessment in industrial engineering.” 2018. Doctoral Dissertation, Université de Lorraine. Accessed March 07, 2021. http://www.theses.fr/2018LORR0341.

MLA Handbook (7^th Edition):

Bousmar, Khadija. “Conception d'un solveur matériel spécifique pour la résolution rapide du problème SAT appliqué à l'évaluation du risque en génie industriel : Design of a specific hardware solver for a speed resolution of the SAT problem applied to risk assessment in industrial engineering.” 2018. Web. 07 Mar 2021.

Vancouver:

Bousmar K. Conception d'un solveur matériel spécifique pour la résolution rapide du problème SAT appliqué à l'évaluation du risque en génie industriel : Design of a specific hardware solver for a speed resolution of the SAT problem applied to risk assessment in industrial engineering. [Internet] [Doctoral dissertation]. Université de Lorraine; 2018. [cited 2021 Mar 07]. Available from: http://www.theses.fr/2018LORR0341.

Council of Science Editors:

Bousmar K. Conception d'un solveur matériel spécifique pour la résolution rapide du problème SAT appliqué à l'évaluation du risque en génie industriel : Design of a specific hardware solver for a speed resolution of the SAT problem applied to risk assessment in industrial engineering. [Doctoral Dissertation]. Université de Lorraine; 2018. Available from: http://www.theses.fr/2018LORR0341

22. Szczepanski, Nicolas. SAT en Parallèle : Parallel SAT solving.

Degree: Docteur es, Informatique, 2017, Université d'Artois

URL: http://www.theses.fr/2017ARTO0403

►

La thèse porte sur la résolution des problèmes de satisfaisabilité booléenne (SAT) dans un cadre massivement parallèle. Le problème SAT est largement utilisé pour résoudre… (more)

Subjects/Keywords: SAT; Colonies d'abeilles; Solveurs SAT; Parallèle; Calcul distribué; Modèles de programmation hybride; SAT; SAT solvers; Parallel; Distributed computing; Hybrid programming models; 006.3

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Szczepanski, N. (2017). SAT en Parallèle : Parallel SAT solving. (Doctoral Dissertation). Université d'Artois. Retrieved from http://www.theses.fr/2017ARTO0403

Chicago Manual of Style (16^th Edition):

Szczepanski, Nicolas. “SAT en Parallèle : Parallel SAT solving.” 2017. Doctoral Dissertation, Université d'Artois. Accessed March 07, 2021. http://www.theses.fr/2017ARTO0403.

MLA Handbook (7^th Edition):

Szczepanski, Nicolas. “SAT en Parallèle : Parallel SAT solving.” 2017. Web. 07 Mar 2021.

Vancouver:

Szczepanski N. SAT en Parallèle : Parallel SAT solving. [Internet] [Doctoral dissertation]. Université d'Artois; 2017. [cited 2021 Mar 07]. Available from: http://www.theses.fr/2017ARTO0403.

Council of Science Editors:

Szczepanski N. SAT en Parallèle : Parallel SAT solving. [Doctoral Dissertation]. Université d'Artois; 2017. Available from: http://www.theses.fr/2017ARTO0403

University of Houston

23. -0075-9784. ADMINISTRATIVE LEADERSHIP EFFECT ON COLLEGE ENTRANCE EXAMINATION PARTICIPATION AND PERFORMANCE.

Degree: EdD, Professional Leadership, 2015, University of Houston

URL: http://hdl.handle.net/10657/1777

► College entrance exam scores, namely the SAT and ACT, are an important criteria for students applying for admission to their college of choice. Clinedinst, Hurley,… (more)

Subjects/Keywords: Leadership; SAT; ACT; Participation; Performance; Achievement; Gap

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

-0075-9784. (2015). ADMINISTRATIVE LEADERSHIP EFFECT ON COLLEGE ENTRANCE EXAMINATION PARTICIPATION AND PERFORMANCE. (Doctoral Dissertation). University of Houston. Retrieved from http://hdl.handle.net/10657/1777

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

Chicago Manual of Style (16^th Edition):

-0075-9784. “ADMINISTRATIVE LEADERSHIP EFFECT ON COLLEGE ENTRANCE EXAMINATION PARTICIPATION AND PERFORMANCE.” 2015. Doctoral Dissertation, University of Houston. Accessed March 07, 2021. http://hdl.handle.net/10657/1777.

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

MLA Handbook (7^th Edition):

-0075-9784. “ADMINISTRATIVE LEADERSHIP EFFECT ON COLLEGE ENTRANCE EXAMINATION PARTICIPATION AND PERFORMANCE.” 2015. Web. 07 Mar 2021.

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

Vancouver:

-0075-9784. ADMINISTRATIVE LEADERSHIP EFFECT ON COLLEGE ENTRANCE EXAMINATION PARTICIPATION AND PERFORMANCE. [Internet] [Doctoral dissertation]. University of Houston; 2015. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/10657/1777.

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

Council of Science Editors:

-0075-9784. ADMINISTRATIVE LEADERSHIP EFFECT ON COLLEGE ENTRANCE EXAMINATION PARTICIPATION AND PERFORMANCE. [Doctoral Dissertation]. University of Houston; 2015. Available from: http://hdl.handle.net/10657/1777

Note: this citation may be lacking information needed for this citation format:
Author name may be incomplete

University of Debrecen

24. Czuczor, Gergő. A SAT probléma .

Degree: DE – Informatikai Kar, University of Debrecen

URL: http://hdl.handle.net/2437/238631

A dolgozat a SAT problémát mutatja be, annak történeti hátterét, illetve az azt megoldó algoritmusokat és a probléma kapcsolatát az egyenletrendszerekkel. Advisors/Committee Members: Várterész, Magda (advisor).

Subjects/Keywords: sat; bonyolultság; egyenletrendszerek

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Czuczor, G. (n.d.). A SAT probléma . (Thesis). University of Debrecen. Retrieved from http://hdl.handle.net/2437/238631

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):

Czuczor, Gergő. “A SAT probléma .” Thesis, University of Debrecen. Accessed March 07, 2021. http://hdl.handle.net/2437/238631.

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):

Czuczor, Gergő. “A SAT probléma .” Web. 07 Mar 2021.

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

Vancouver:

Czuczor G. A SAT probléma . [Internet] [Thesis]. University of Debrecen; [cited 2021 Mar 07]. Available from: http://hdl.handle.net/2437/238631.

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:

Czuczor G. A SAT probléma . [Thesis]. University of Debrecen; Available from: http://hdl.handle.net/2437/238631

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

Delft University of Technology

25. Zwart, Joost (author). Sparsity based hybrid system identification using a SAT solver.

Degree: 2019, Delft University of Technology

URL: http://resolver.tudelft.nl/uuid:725afc81-eefb-47b2-ac78-b6119a86eae8

►

System identification for switched linear systems from input output data has received substantial attention in recent years. There is a growing interest for techniques that… (more)

Subjects/Keywords: SAT solver; Hybrid Systems; Identification; Sparsity

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Zwart, J. (. (2019). Sparsity based hybrid system identification using a SAT solver. (Masters Thesis). Delft University of Technology. Retrieved from http://resolver.tudelft.nl/uuid:725afc81-eefb-47b2-ac78-b6119a86eae8

Chicago Manual of Style (16^th Edition):

Zwart, Joost (author). “Sparsity based hybrid system identification using a SAT solver.” 2019. Masters Thesis, Delft University of Technology. Accessed March 07, 2021. http://resolver.tudelft.nl/uuid:725afc81-eefb-47b2-ac78-b6119a86eae8.

MLA Handbook (7^th Edition):

Zwart, Joost (author). “Sparsity based hybrid system identification using a SAT solver.” 2019. Web. 07 Mar 2021.

Vancouver:

Zwart J(. Sparsity based hybrid system identification using a SAT solver. [Internet] [Masters thesis]. Delft University of Technology; 2019. [cited 2021 Mar 07]. Available from: http://resolver.tudelft.nl/uuid:725afc81-eefb-47b2-ac78-b6119a86eae8.

Council of Science Editors:

Zwart J(. Sparsity based hybrid system identification using a SAT solver. [Masters Thesis]. Delft University of Technology; 2019. Available from: http://resolver.tudelft.nl/uuid:725afc81-eefb-47b2-ac78-b6119a86eae8

University of Waterloo

26. Pisanov, Vladimir. Novel Value Ordering Heuristics Using Non-Linear Optimization In Boolean Satisfiability.

Degree: 2012, University of Waterloo

URL: http://hdl.handle.net/10012/6941

► Boolean Satisfiability (SAT) is a fundamental NP-complete problem of determining whether there exists an assignment of variables which makes a Boolean formula evaluate to True.… (more)

Subjects/Keywords: Boolean satisfiability; SAT; Backtracking search; Value ordering

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Pisanov, V. (2012). Novel Value Ordering Heuristics Using Non-Linear Optimization In Boolean Satisfiability. (Thesis). University of Waterloo. Retrieved from http://hdl.handle.net/10012/6941

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):

Pisanov, Vladimir. “Novel Value Ordering Heuristics Using Non-Linear Optimization In Boolean Satisfiability.” 2012. Thesis, University of Waterloo. Accessed March 07, 2021. http://hdl.handle.net/10012/6941.

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

MLA Handbook (7^th Edition):

Pisanov, Vladimir. “Novel Value Ordering Heuristics Using Non-Linear Optimization In Boolean Satisfiability.” 2012. Web. 07 Mar 2021.

Vancouver:

Pisanov V. Novel Value Ordering Heuristics Using Non-Linear Optimization In Boolean Satisfiability. [Internet] [Thesis]. University of Waterloo; 2012. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/10012/6941.

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

Council of Science Editors:

Pisanov V. Novel Value Ordering Heuristics Using Non-Linear Optimization In Boolean Satisfiability. [Thesis]. University of Waterloo; 2012. Available from: http://hdl.handle.net/10012/6941

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

27. Zulkoski, Edward. Understanding and Enhancing CDCL-based SAT Solvers.

Degree: 2018, University of Waterloo

URL: http://hdl.handle.net/10012/13525

► Modern conflict-driven clause-learning (CDCL) Boolean satisfiability (SAT) solvers routinely solve formulas from industrial domains with millions of variables and clauses, despite the Boolean satisfiability problem… (more)

▼ Modern conflict-driven clause-learning (CDCL) Boolean satisfiability (SAT) solvers routinely solve formulas from industrial domains with millions of variables and clauses, despite the Boolean satisfiability problem being NP-complete and widely regarded as intractable in general. At the same time, very small crafted or randomly generated formulas are often infeasible for CDCL solvers. A commonly proposed explanation is that these solvers somehow exploit the underlying structure inherent in industrial instances. A better understanding of the structure of Boolean formulas not only enables improvements to modern SAT solvers, but also lends insight as to why solvers perform well or poorly on certain types of instances. Even further, examining solvers through the lens of these underlying structures can help to distinguish the behavior of different solving heuristics, both in theory and practice. The first issue we address relates to the representation of SAT formulas. A given Boolean satisfiability problem can be represented in arbitrarily many ways, and the type of encoding can have significant effects on SAT solver performance. Further, in some cases, a direct encoding to SAT may not be the best choice. We introduce a new system that integrates SAT solving with computer algebra systems (CAS) to address representation issues for several graph-theoretic problems. We use this system to improve the bounds on several finitely-verified conjectures related to graph-theoretic problems. We demonstrate how our approach is more appropriate for these problems than other off-the-shelf SAT-based tools. For more typical SAT formulas, a better understanding of their underlying structural properties, and how they relate to SAT solving, can deepen our understanding of SAT. We perform a largescale evaluation of many of the popular structural measures of formulas, such as community structure, treewidth, and backdoors. We investigate how these parameters correlate with CDCL solving time, and whether they can effectively be used to distinguish formulas from different domains. We demonstrate how these measures can be used as a means to understand the behavior of solvers during search. A common theme is that the solver exhibits locality during search through the lens of these underlying structures, and that the choice of solving heuristic can greatly influence this locality. We posit that this local behavior of modern SAT solvers is crucial to their performance. The remaining contributions dive deeper into two new measures of SAT formulas. We first consider a simple measure, denoted “mergeability,” which characterizes the proportion of input clauses pairs that can resolve and merge. We develop a formula generator that takes as input a seed formula, and creates a sequence of increasingly more mergeable formulas, while maintaining many of the properties of the original formula. Experiments over randomly-generated industrial-like instances suggest that mergeability strongly negatively correlates with CDCL…

Subjects/Keywords: SAT Solvers; Backdoors; Computer Algebra Systems

10 more images…

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Zulkoski, E. (2018). Understanding and Enhancing CDCL-based SAT Solvers. (Thesis). University of Waterloo. Retrieved from http://hdl.handle.net/10012/13525

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):

Zulkoski, Edward. “Understanding and Enhancing CDCL-based SAT Solvers.” 2018. Thesis, University of Waterloo. Accessed March 07, 2021. http://hdl.handle.net/10012/13525.

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

MLA Handbook (7^th Edition):

Zulkoski, Edward. “Understanding and Enhancing CDCL-based SAT Solvers.” 2018. Web. 07 Mar 2021.

Vancouver:

Zulkoski E. Understanding and Enhancing CDCL-based SAT Solvers. [Internet] [Thesis]. University of Waterloo; 2018. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/10012/13525.

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

Council of Science Editors:

Zulkoski E. Understanding and Enhancing CDCL-based SAT Solvers. [Thesis]. University of Waterloo; 2018. Available from: http://hdl.handle.net/10012/13525

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

University of Waterloo

28. Li, Zijie. Backdoors in Satisfiability Problems.

Degree: 2009, University of Waterloo

URL: http://hdl.handle.net/10012/4810

► Although satisfiability problems (SAT) are NP-complete, state-of-the-art SAT solvers are able to solve large practical instances. The notion of backdoors has been introduced to capture… (more)

Subjects/Keywords: CSP; SAT; Backdoors

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Li, Z. (2009). Backdoors in Satisfiability Problems. (Thesis). University of Waterloo. Retrieved from http://hdl.handle.net/10012/4810

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):

Li, Zijie. “Backdoors in Satisfiability Problems.” 2009. Thesis, University of Waterloo. Accessed March 07, 2021. http://hdl.handle.net/10012/4810.

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

MLA Handbook (7^th Edition):

Li, Zijie. “Backdoors in Satisfiability Problems.” 2009. Web. 07 Mar 2021.

Vancouver:

Li Z. Backdoors in Satisfiability Problems. [Internet] [Thesis]. University of Waterloo; 2009. [cited 2021 Mar 07]. Available from: http://hdl.handle.net/10012/4810.

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

Council of Science Editors:

Li Z. Backdoors in Satisfiability Problems. [Thesis]. University of Waterloo; 2009. Available from: http://hdl.handle.net/10012/4810

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

Delft University of Technology

29. Vollebergh, M.A.J. (author). Incorporating flexible track use in the SAT model of the Dutch railway timetabling problem.

Degree: 2020, Delft University of Technology

URL: http://resolver.tudelft.nl/uuid:37aaf584-8775-44d6-b3cb-e914f8a54b48

► The construction of cyclic railway timetables is an important task for Netherlands Railways (NS).This construction can be formulated as a Periodic Event Scheduling Problem (PESP).… (more)

Subjects/Keywords: Flexible track use; SAT; PESP; Railways; Timetabling

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Vollebergh, M. A. J. (. (2020). Incorporating flexible track use in the SAT model of the Dutch railway timetabling problem. (Masters Thesis). Delft University of Technology. Retrieved from http://resolver.tudelft.nl/uuid:37aaf584-8775-44d6-b3cb-e914f8a54b48

Chicago Manual of Style (16^th Edition):

Vollebergh, M A J (author). “Incorporating flexible track use in the SAT model of the Dutch railway timetabling problem.” 2020. Masters Thesis, Delft University of Technology. Accessed March 07, 2021. http://resolver.tudelft.nl/uuid:37aaf584-8775-44d6-b3cb-e914f8a54b48.

MLA Handbook (7^th Edition):

Vollebergh, M A J (author). “Incorporating flexible track use in the SAT model of the Dutch railway timetabling problem.” 2020. Web. 07 Mar 2021.

Vancouver:

Vollebergh MAJ(. Incorporating flexible track use in the SAT model of the Dutch railway timetabling problem. [Internet] [Masters thesis]. Delft University of Technology; 2020. [cited 2021 Mar 07]. Available from: http://resolver.tudelft.nl/uuid:37aaf584-8775-44d6-b3cb-e914f8a54b48.

Council of Science Editors:

Vollebergh MAJ(. Incorporating flexible track use in the SAT model of the Dutch railway timetabling problem. [Masters Thesis]. Delft University of Technology; 2020. Available from: http://resolver.tudelft.nl/uuid:37aaf584-8775-44d6-b3cb-e914f8a54b48

30. Lonca, Emmanuel. Optimisation booléenne multiobjectif : complexité sous contraintes compilées et résolution via SAT : Multiobjective boolean optimization.

Degree: Docteur es, Informatique, 2015, Université d'Artois

URL: http://www.theses.fr/2015ARTO0405

►

L’aide à la décision a pour but d’assister un opérateur humain dans ses choix. La nécessité d’employer de telles techniques s’est imposée avec la volonté… (more)

▼

L’aide à la décision a pour but d’assister un opérateur humain dans ses choix. La nécessité d’employer de telles techniques s’est imposée avec la volonté de traiter des problèmes dépendant d’une quantité de données toujours plus importante. L’intérêt de l’aide à la décision est encore plus manifeste lorsqu’on souhaite obtenir non pas une solution quelconque, mais une des meilleures solutions d’un problème combinatoire selon un critère donné. On passe alors d’un problème de décision (déterminer l’existence d’une solution) à un problème d’optimisation monocritère (déterminer une des meilleures solutions possibles selon un critère). Un décideur peut aussi souhaiter considérer plusieurs critères, et ainsi faire passer le problème de décision initial à un problème d’optimisation multicritère. La difficulté de ce type de problèmes provient du fait que les critères considérés sont généralement antagonistes, et qu’il n’existe donc pas de solution meilleure que les autres pour l’ensemble des critères. Dans ce cas, il s’agit plutôt de déterminer une solution qui offre un bon compromis entre les critères. Dans cette thèse, nous étudions dans un premier temps la complexité théorique de tâches d’optimisation complexes sur les langages de la logique propositionnelle, puis nous étudions leur résolution pratique via le recours à des logiciels bâtis pour résoudre de manière efficace en pratique des problèmes de décision combinatoires, les prouveurs SAT.

Decision aiding aims at helping a decision-maker to pick up a solution among several others. The usefulness of such approaches is as prominent as the size of the problems under consideration increases. The need of decision aiding techniques is salient when the problem does not just consist in deciding whether a solutions exists, but to find one of the best solutions according to a given criterion. In this case, the problem goes from a decision problem (decide whether a solution exists) to a single criterion optimization problem (find one of the best solutions according to a criterion). A decision-maker may even want to consider multiple criteria, which turns the initial decision problem into a multicriteria optimization problem. The main issue arising in such cases lies in the fact that the criteria under consideration are often antagonistic, which implies that there is no solution which is the best for each of the objectives. In this case, a good compromise solution is looked for. In this thesis, we first focus on the complexity of optimization requests based on a set of propositional languages. We then study the practical aspects of the resolution of such problems, using pieces of software designed for dealing with combinatorial decision problems, namely SAT solvers.

Advisors/Committee Members: Le Berre, Daniel (thesis director).

Subjects/Keywords: Aide à la décision; Optimisation multicritère; SAT; Decision aid; MCDA; SAT; 006.3

Record Details Similar Records Cite « Share

❌

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

APA (6^th Edition):

Lonca, E. (2015). Optimisation booléenne multiobjectif : complexité sous contraintes compilées et résolution via SAT : Multiobjective boolean optimization. (Doctoral Dissertation). Université d'Artois. Retrieved from http://www.theses.fr/2015ARTO0405

Chicago Manual of Style (16^th Edition):

Lonca, Emmanuel. “Optimisation booléenne multiobjectif : complexité sous contraintes compilées et résolution via SAT : Multiobjective boolean optimization.” 2015. Doctoral Dissertation, Université d'Artois. Accessed March 07, 2021. http://www.theses.fr/2015ARTO0405.

MLA Handbook (7^th Edition):

Lonca, Emmanuel. “Optimisation booléenne multiobjectif : complexité sous contraintes compilées et résolution via SAT : Multiobjective boolean optimization.” 2015. Web. 07 Mar 2021.

Vancouver:

Lonca E. Optimisation booléenne multiobjectif : complexité sous contraintes compilées et résolution via SAT : Multiobjective boolean optimization. [Internet] [Doctoral dissertation]. Université d'Artois; 2015. [cited 2021 Mar 07]. Available from: http://www.theses.fr/2015ARTO0405.

Council of Science Editors:

Lonca E. Optimisation booléenne multiobjectif : complexité sous contraintes compilées et résolution via SAT : Multiobjective boolean optimization. [Doctoral Dissertation]. Université d'Artois; 2015. Available from: http://www.theses.fr/2015ARTO0405

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

Open Access Theses and Dissertations