Advanced search options

Advanced Search Options 🞨

Browse by author name (“Author name starts with…”).

Find ETDs with:

in
/  
in
/  
in
/  
in

Written in Published in Earliest date Latest date

Sorted by

Results per page:

Sorted by: relevance · author · university · dateNew search

You searched for subject:(Satisfiability SAT solving). Showing records 1 – 3 of 3 total matches.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters


University of Colorado

1. Bennett, Huxley David. Results on Extensions of the Satisfability Problem.

Degree: MS, Computer Science, 2012, University of Colorado

The satisfiability problem (SAT) and its extensions have become indispensible tools in artificial intelligence, verification, and many other domains. Extensions of the problem such as model counting, quantified Boolean formulae (QBF), and MAX-SAT have similarly seen increased study and applications. This thesis provides a survey on SAT, and then presents novel results related to model counting and random QBF. Chapter 3 gives a general technique for computing inclusion-exclusion sums more efficiently for the purpose of model counting. The main contribution is a subsumption technique which reduces computational overhead. Treating an inclusion-exclusion sum's computation as tree exploration, subsumption allows us to prune large subtrees. We also give a better worst-case upper bound on the algorithm's running time, improving it from exponential in the number of clauses to the number of variables in a CNF formula. Chapter 5 describes a new phase transition in random QBF, along with related results on random QBF models. The clause-to-variable ratio phase transition identified in random k-SAT has been the subject of intense study on what makes a SAT instance intractable, and recent work has studied a similar transition in random QBF. Here we show that a satisfiability threshold exists around phase transitions arising from altering the fraction of existentially versus universally quantified variables in a formula. In chapter 6 we revisit work on generating trivially false formulas in several related random QBF models, giving precise bounds for how likely they are to occur. Advisors/Committee Members: Sriram Sankaranarayanan, Bor-Yuh Evan Chang, Aaron Clauset.

Subjects/Keywords: constraint solving; inclusion-exclusion; model counting; quantified boolean formulae; random sat; satisfiability problem; Computer Sciences

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Bennett, H. D. (2012). Results on Extensions of the Satisfability Problem. (Masters Thesis). University of Colorado. Retrieved from https://scholar.colorado.edu/csci_gradetds/39

Chicago Manual of Style (16th Edition):

Bennett, Huxley David. “Results on Extensions of the Satisfability Problem.” 2012. Masters Thesis, University of Colorado. Accessed April 18, 2021. https://scholar.colorado.edu/csci_gradetds/39.

MLA Handbook (7th Edition):

Bennett, Huxley David. “Results on Extensions of the Satisfability Problem.” 2012. Web. 18 Apr 2021.

Vancouver:

Bennett HD. Results on Extensions of the Satisfability Problem. [Internet] [Masters thesis]. University of Colorado; 2012. [cited 2021 Apr 18]. Available from: https://scholar.colorado.edu/csci_gradetds/39.

Council of Science Editors:

Bennett HD. Results on Extensions of the Satisfability Problem. [Masters Thesis]. University of Colorado; 2012. Available from: https://scholar.colorado.edu/csci_gradetds/39


University of Illinois – Urbana-Champaign

2. Lin, Chen-Hsuan. Design automation for circuit reliability and energy efficiency.

Degree: PhD, Electrical & Computer Engr, 2017, University of Illinois – Urbana-Champaign

This dissertation presents approaches to improve circuit reliability and energy efficiency from different angles, such as verification, logic synthesis, and functional unit design. A variety of algorithmic methods and heuristics are used in our approaches such as SAT solving, data mining, logic restructuring, and applied mathematics. Furthermore, the scalability of our approaches was taken into account while we developed our solutions. Experimental results show that our approaches offer the following advantages: 1) SAT-BAG can generate concise assertions that can always achieve 100% input space coverage. 2) C-Mine-DCT, compared to a recent publication, can achieve compatible performance with an additional 8% energy saving and 54x speedup for bigger benchmarks on average. 3) C-Mine-APR can achieve up to 13% more energy saving than C-Mine-DCT while confronting designs with more common cases. 4) CSL can achieve 6.5% NBTI delay reduction with merely 2.5% area overhead on average. 5) Our modulo functional units, compared to a previous approach, can achieve a 12.5% reduction in area and a 47.1% reduction in delay for a 32-bit mod-3 reducer. For modulo-15 and above, all of our modulo functional units have better area and delay than their previous counterparts. Advisors/Committee Members: Chen, Deming (advisor), Chen, Deming (Committee Chair), Hwu, Wen-Mei (committee member), Rutenbar, Rob A. (committee member), Wong, Martin D. F. (committee member).

Subjects/Keywords: Electronic design automation; Reliability; Energy efficiency; Data mining; Satisfiability (SAT) solving; Logic restructuring; Assertion; Negative bias temperature instability (NBTI) effect; Modulo arithmetic; Shadow datapath

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Lin, C. (2017). Design automation for circuit reliability and energy efficiency. (Doctoral Dissertation). University of Illinois – Urbana-Champaign. Retrieved from http://hdl.handle.net/2142/99237

Chicago Manual of Style (16th Edition):

Lin, Chen-Hsuan. “Design automation for circuit reliability and energy efficiency.” 2017. Doctoral Dissertation, University of Illinois – Urbana-Champaign. Accessed April 18, 2021. http://hdl.handle.net/2142/99237.

MLA Handbook (7th Edition):

Lin, Chen-Hsuan. “Design automation for circuit reliability and energy efficiency.” 2017. Web. 18 Apr 2021.

Vancouver:

Lin C. Design automation for circuit reliability and energy efficiency. [Internet] [Doctoral dissertation]. University of Illinois – Urbana-Champaign; 2017. [cited 2021 Apr 18]. Available from: http://hdl.handle.net/2142/99237.

Council of Science Editors:

Lin C. Design automation for circuit reliability and energy efficiency. [Doctoral Dissertation]. University of Illinois – Urbana-Champaign; 2017. Available from: http://hdl.handle.net/2142/99237

3. Backes, John D. Algorithms and data structures for logic synthesis and verification using Boolean satisfiability.

Degree: PhD, 2013, University of Minnesota

Boolean satisfiability (SAT) was the first problem to be proven to be NP-Complete. The proof, provided by Stephen Cook in 1971, demonstrated that inputs accepted by a non-deterministic Turing machine can be described by satisfying assignments of a Boolean formula. The reduction to SAT feels natural for a wealth of decision problems; this has motivated an immense amount of research into heuristics for solving SAT instances quickly. Over the past decade the performance of SAT solvers has improved tremendously, and as a consequence, real-world problems that were once thought to be intractable are now feasible in many cases. In this thesis we discuss how some problems in logic synthesis and verification can be solved with Boolean satisfiability. The dissertation begins by discussing Cyclic Combinational Circuits. Cyclic Combinational Circuits are logic circuits that contain feedback, but exhibit no state behavior. Many functions can be implemented with fewer gates using a cyclic topology rather than an acyclic topology. A pivotal step in synthesizing these circuits is proving whether or not the resulting structure is actually combinational, and if not, how to modify the circuit to behave properly. This analysis can be elegantly cast as an instance of SAT. Furthermore, this thesis demonstrates how modern SATBased synthesis techniques can be used to generate cyclic structures, rather than just analyze them. These SAT-Based synthesis techniques rely on augmenting proofs of unsatisfiability to generate circuit structures. These structures, called Craig Interpolants, and the proofs they are generated from are the focus of the second portion of this dissertation. Techniques are proposed for reducing the size of these interpolants,and then the use of proofs of unsatisfiability as an underlying data structure for synthesis is advocated. Finally, the last portion of this thesis discusses some improvements to a new model checking algorithm known as Property Directed Reachability (PDR). This algorithm iteratively solves SAT instances representing discrete time frames of a sequential circuit in order to demonstrate that a state invariant exists.

Subjects/Keywords: Automated theorem proving; Boolean satisfiability; Cyclic circuits; Formal verification; Model checking; SAT solving

…Boolean Satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2.2 Tsestin… …Satisfiability 2.1 2.2 10 Introduction… …Prior and Related Work . . . . . . . . . . . . . . . . . . . . . . . 14 2.1.3 SAT-Based… …Learning and Incremental SAT . . . . . . . . . . . . . . . 75 3.2.3 Resolution Proofs and… …table on the right side of the Figure lists all the satisfying assignments of the SAT instance… 

Page 1 Page 2 Page 3 Page 4 Page 5 Page 6 Page 7

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

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

APA (6th Edition):

Backes, J. D. (2013). Algorithms and data structures for logic synthesis and verification using Boolean satisfiability. (Doctoral Dissertation). University of Minnesota. Retrieved from http://purl.umn.edu/148684

Chicago Manual of Style (16th Edition):

Backes, John D. “Algorithms and data structures for logic synthesis and verification using Boolean satisfiability.” 2013. Doctoral Dissertation, University of Minnesota. Accessed April 18, 2021. http://purl.umn.edu/148684.

MLA Handbook (7th Edition):

Backes, John D. “Algorithms and data structures for logic synthesis and verification using Boolean satisfiability.” 2013. Web. 18 Apr 2021.

Vancouver:

Backes JD. Algorithms and data structures for logic synthesis and verification using Boolean satisfiability. [Internet] [Doctoral dissertation]. University of Minnesota; 2013. [cited 2021 Apr 18]. Available from: http://purl.umn.edu/148684.

Council of Science Editors:

Backes JD. Algorithms and data structures for logic synthesis and verification using Boolean satisfiability. [Doctoral Dissertation]. University of Minnesota; 2013. Available from: http://purl.umn.edu/148684

.