The VLSI CAD flow encompasses an abundance of critical NP-complete and PSPACE-complete problems. Instead of developing a dedicated algorithm for each, the trend during the last decade has been to encode them in formal languages, such as Boolean satisfiability (SAT) and quantified Boolean formulas (QBFs), and focus academic resources on improving SAT and QBF solvers. The significant progress of these solvers has validated this strategy. This dissertation contributes to the further advancement of formal techniques in CAD. Today, the verification and debugging of increasingly complex RTL designs can consume up to 70% of the VLSI design cycle. In particular, RTL debug is a manual, resource-intensive task in the industry. The first contribution of this thesis is an in-depth examination of the factors affecting the theoretical computational complexity of debugging. It is established that most variations of the debugging problem are NP-complete. Automated debugging tools return all potential error sources in the RTL, called solutions, that can explain a given failing error trace. Finding each solution requires a separate call to a formal engine, which is computationally expensive. The second contribution of this dissertation comprises techniques for reducing the number of such iterations, by leveraging dominance relationships between RTL blocks to imply solutions. Extensive experiments on industrial designs show a three-fold reduction in the number of formal engine calls due to solution implications, resulting in a 1.64x overall speed-up. The third contribution aims to advance the state-of-the-art of QBF solvers, whose progress has not been as impressive as that of SAT solvers. We present a framework for using complete dominators to preprocess and reduce QBFs with an inherent circuit structure, which is common in encodings of PSPACE-complete CAD problems. Experiments show that three modern QBF solvers together solve 55% of preprocessed QBF instances, compared to none without preprocessing. The final contribution consists of a series of QBF encodings for evaluating the reconfigurability of partially programmable circuits (PPCs). The metrics of fault tolerance, design error tolerance and engineering change coverage are defined for PPCs and encoded using QBFs. These formulations along with experimental results demonstrate the theoretical and practical appropriateness of QBFs for dealing with reconfigurability.

The size and complexity of modern VLSI computer chips are growing at a rapid pace. Functional debugging is increasingly becoming a bottleneck in the design flow where it can take up to 60% of the total verification time. Scaling existing automated debugging tools is necessary in order to continue along this path of rapid growth and innovation in the semiconductor industry. This thesis aims to scale automated debugging techniques with two contributions. The first contribution introduces a succinct memory model for automated design debugging that dramatically lowers the memory requirements for the debugging problem. The second contribution presents a scalable SAT-based design debugging algorithm that uses a mathematical technique called interpolation to divide the debugging problem into multiple parts across time which greatly reduces the peak memory requirements of the debugging problem. Extensive experiments on real designs demonstrate the benefit of this work.

The runtime for solving constraint satisfaction problems (CSP) and propositional satisfiability problems (SAT) using systematic backtracking search has been shown to exhibit great variability. Randomization and restarts is an effective technique for reducing such variability to achieve better expected performance. Several restart strategies have been proposed and studied in previous work and show differing degrees of empirical effectiveness. <br /><br /> The first topic in this thesis is the extension of analytical results on restart strategies through the introduction of physically based assumptions. In particular, we study the performance of two of the restart strategies on Pareto runtime distributions. We show that the geometric strategy provably removes heavy tail. We also examine several factors that arise during implementation and their effects on existing restart strategies. <br /><br /> The second topic concerns the development of a new hybrid restart strategy in a realistic problem setting. Our work adapts the existing general approach on dynamic strategy but implements more sophisticated machine learning techniques. The resulting hybrid strategy shows superior performance compared to existing static strategies and an improved robustness.

The runtime for solving constraint satisfaction problems (CSP) and propositional satisfiability problems (SAT) using systematic backtracking search has been shown to exhibit great variability. Randomization and restarts is an effective technique for reducing such variability to achieve better expected performance. Several restart strategies have been proposed and studied in previous work and show differing degrees of empirical effectiveness. <br /><br /> The first topic in this thesis is the extension of analytical results on restart strategies through the introduction of physically based assumptions. In particular, we study the performance of two of the restart strategies on Pareto runtime distributions. We show that the geometric strategy provably removes heavy tail. We also examine several factors that arise during implementation and their effects on existing restart strategies. <br /><br /> The second topic concerns the development of a new hybrid restart strategy in a realistic problem setting. Our work adapts the existing general approach on dynamic strategy but implements more sophisticated machine learning techniques. The resulting hybrid strategy shows superior performance compared to existing static strategies and an improved robustness.

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. SAT is a convenient representation for many naturally occurring optimization and decisions problems such as planning and circuit verification. SAT is most commonly solved by a form of backtracking search which systematically explores the space of possible variable assignments. We show that the order in which variable polarities are assigned can have a significant impact on the performance of backtracking algorithms. We present several ways of transforming SAT instances into non-linear objective functions and describe three value-ordering methods based on iterative optimization techniques. We implement and test these heuristics in the widely-recognized MiniSAT framework. The first approach determines polarities by applying Newton's Method to a sparse system of non-linear objective functions whose roots correspond to the satisfying assignments of the propositional formula. The second approach determines polarities by minimizing an objective function corresponding to the number of clauses conflicting with each assignment. The third approach determines preferred polarities by performing stochastic gradient descent on objective functions sampled from a family of continuous potentials. The heuristics are evaluated on a set of standard benchmarks including random, crafted and industrial problems. We compare our results to five existing heuristics, and show that MiniSAT equipped with our heuristics often outperforms state-of-the-art SAT solvers.

The NP-complete k-SAT problem - decide wether a given formula is satisfiable - is of fundamental importance in theoretical computer science. In this dissertation we study random 4-SAT formulas with > 116 n^2 clauses. These formulas are almost surly unsatisfiable. Here we show the existence of a polynomial time algorithm that certifies the unsatisfiability. Therefore we study the discrepancy of hypergraphs and multigraphs. We also combine spectral techniques with approximation algorithms to achieve the new result. Our new algorithm is adaptable for Not-All-Equal-4-SAT and the 2-colouring of 4-uniform hypergraphs. We also extends the Hajos construction of non k-colourable graphs to non k-colourable uniform hypergraphs. / Das NP-vollständige Problem k-SAT ist von zentraler Bedeutung in der theoretischen Informatik. In der Dissertation werden zufällige 4-SAT-Formeln mit > n^2 vielen Klauseln studiert. Diese Formeln sind mit hoher Wahrscheinlichkeit unerfüllbar. Hier wird erstmalig die Existenz eines Algorithmus gezeigt, der diese Unerfüllbarkeit effizient verifiziert. Hierfür wird die geringe Diskrepanz von Hypergrpahen und Multigraphen betrachtet. Der Schlüssel zu diesem Algorithmus liegt in der Kombination von spektralen Techniken mit Approximationsalgorithmen der klassischen kombinatorischen Optimierung. Der vorgestellte Algorithmus kann auf den effizienten Nachweis der Unerfüllbarkeit von Not-All-Equal-4-SAT-Formeln und die Nicht-2-Färbbarkeit von 4-uniformen Hypergraphen erweitert werden. Es wird ebenfalls eine Erweiterung der Hajos-Konstruktion nicht k-färbbarer Graphen auf nicht k-färbbare uniforme Hypergraphen angegeben.

The Individuals with Disabilities Education Act (IDEA) and the No Child Left Behind (NCLB) Act mandate all children be included in state and district assessments to measure their progress. IDEA, NCLB, and the Americans with Disabilities Act (ADA) require students have access to accommodations necessary for their participation in mandated testing. Due to problems secondary to their disability, students who are deaf and hard-of-hearing (D/HH) may have difficulty participating in testing programs designed for the general population. In order to have equal access to standardized testing, D/HH students may need to use testing accommodations.The purposes of this study were to: a) document the use of testing accommodations by students who are D/HH, b) identify the types and frequency of testing accommodations required by D/HH students attending general education classes in Arizona public schools, and c) to analyze the relationships between type and degree of hearing loss and SAT-9 achievement for students who are D/HH in Arizona public schools.The participants included 62 students in the first year of the study, and 53 students in the second year. All participants had diagnosed hearing losses and attended general education classes with support from teachers of the D/HH and/or other support personnel.Extended Time was the most frequently required accommodation. Principal components analysis resulted in clustering of accommodations variables into three components in 2002: Time and Administration, Presentation, and Student Directed, and four components in 2003: Presentation and Administration, Time and Materials, Response, and Student Directed. The accommodations used and their clustering were similar to those reported in the literature. Type of hearing loss was found to significantly affect reading achievement even when controlling for testing accommodations. The interaction between type and degree of loss significantly affected language achievement. Results demonstrated the reading and language achievement performance of students with mild and high frequency hearing loss fell behind students having greater levels of hearing loss. The use of testing accommodations resulted in mixed effects on student reading and language achievement performance. Changes in language scores, but not in reading scores, were found.

The purpose of this study was to discover: (A) Whether the Tennessee Self-Concept Test would predict academic success better than the Scholastic Aptitude Test. (B) Whether Tennessee Self-Concept Test would add to Scholastic Aptitude Test as a predictor of academic success.The subjects were 102 first quarter Freshmen English students enrolled at Ball State University during the Fall Quarter of 1974. The predictor variables studied were: Scholastic Aptitude Test - verbal, Scholastic Aptitude Test -mathematical and Tennessee Self -Concept Test the counseling form. All the 14 scores on Tennessee Self-Concept Test, self criticism, total-P scores, Row 1-identity, Row 2-self satisfaction, Row 3-behavior, Column 1-physical self, Column 2-moral self, Column 3-personal self, Column 4-family self, Column 5-social self, Total variability score, Column total, Row total, and D-distribution score, were included. The criteria of success was the final grade point average.In order to find the statistical significance of the variables studied as a predictor of academic success, step wise multiple regression was applied.The result of this study indicated that (A) the single variable that offered the best information for predicting academic success was Scholastic Aptitude Test-verbal; (B) only one variable on Tennessee Self Concept Test, the personal self, was significant as a predictor of academic success; (C) the combination of variables on Scholastic Aptitude Test and Tennessee Self-Concept Test was test d. Only three variables were found to be significant as a predictor of academic success: SAT-verbal, Column 4-the family self, and Column 3-personal self.

There is no abstract available for this dissertation. / Department of Educational Leadership

The purpose of this research was to examine the records of all students who pursued a curriculum at Ball State University which could lead to provisional certification to teach biology in the public schools of Indiana, covering retrospectively, all consecutive years for which complete records could be retrieved, to determine if such provisional certification to teach biology could be predicted by the examination of test scores made by students on the Scholastic Aptitude Test of the College Entrance Examination Board.A statistical comparison was made between the Scholastic Aptitude Test scores of those persons achieving provisional certification to teach biology in the public schools of Indiana and those persons not achieving such provisional certification, to determine whether Scholastic Aptitude Test scores in and of themselves could be used to predict provisional certification to teach biology in the public schools of Indiana.The records of all students at Ball State University who at any time between September of 1965 and June of 1974 pursued a course of study which, if completed, would lead to provisional certification to teach biology in the public schools of Indiana were examined, excluding all who had not been graduated by June of 1974 and those who did not have Scholastic Aptitude Test scores in their files at Ball State University.These students were divided into two groups, Group one was made up of those students who achieved provisional certification to teach biology in the public schools of Indiana and consisted of 331 students, Group two was made up of those students who failed to achieve provisional certification to teach biology in the public schools of Indiana and consisted of 244 students,A statistical comparison was made of the two groups - those certified (group one) versus those who were not certified (group two) - by the use of discriminant analysis, using as variables within the two groups, the bivarients (1) verbal score made on the Scholastic Aptitude Test, and (2) mathematical score made on the Scholastic Aptitude Test, The method of discriminant analysis combines variables within the two groups and then compares those groups on the basis of group differences without regard for their interrelations and partly overlapping information.The statistical analysis of the two groups indicated that there was no significant difference in the scores attained by the students in the two groups on the Scholastic Aptitude Test of the College Entrance Examination Board. The conclusion was made that scores made on the Scholastic Aptitude Test of the College Entrance Examination Board are not valid predictors of provisional certification of biology teachers at Ball State University during the period between September of 1965 and June of 1974.The study recommends that the Scholastic Aptitude Test of the College Entrance Examination Board be evaluated in all areas of advisement, including high school, junior college, and university advisement.The study further recommends that scores attained on the Scholastic Aptitude Test of the College Entrance Examination Board not be used in situations to which they are not applicable and for which they were not designed.The study further recommends that the Scholastic Aptitude Test of the College Entrance Examination Board be totally reexamined by qualified independent researchers to determine not only the value of this test as currently applied, but other possible ways in which this test can be used with validity.