Answer set programming modulo theories

154648-Thumbnail Image.png
Description
Knowledge representation and reasoning is a prominent subject of study within the field of artificial intelligence that is concerned with the symbolic representation of knowledge in such a way to facilitate automated reasoning about this knowledge. Often in real-world domains,

Knowledge representation and reasoning is a prominent subject of study within the field of artificial intelligence that is concerned with the symbolic representation of knowledge in such a way to facilitate automated reasoning about this knowledge. Often in real-world domains, it is necessary to perform defeasible reasoning when representing default behaviors of systems. Answer Set Programming is a widely-used knowledge representation framework that is well-suited for such reasoning tasks and has been successfully applied to practical domains due to efficient computation through grounding--a process that replaces variables with variable-free terms--and propositional solvers similar to SAT solvers. However, some domains provide a challenge for grounding-based methods such as domains requiring reasoning about continuous time or resources.

To address these domains, there have been several proposals to achieve efficiency through loose integrations with efficient declarative solvers such as constraint solvers or satisfiability modulo theories solvers. While these approaches successfully avoid substantial grounding, due to the loose integration, they are not suitable for performing defeasible reasoning on functions. As a result, this expressive reasoning on functions must either be performed using predicates to simulate the functions or in a way that is not elaboration tolerant. Neither compromise is reasonable; the former suffers from the grounding bottleneck when domains are large as is often the case in real-world domains while the latter necessitates encodings to be non-trivially modified for elaborations.

This dissertation presents a novel framework called Answer Set Programming Modulo Theories (ASPMT) that is a tight integration of the stable model semantics and satisfiability modulo theories. This framework both supports defeasible reasoning about functions and alleviates the grounding bottleneck. Combining the strengths of Answer Set Programming and satisfiability modulo theories enables efficient continuous reasoning while still supporting rich reasoning features such as reasoning about defaults and reasoning in domains with incomplete knowledge. This framework is realized in two prototype implementations called MVSM and ASPMT2SMT, and the latter was recently incorporated into a non-monotonic spatial reasoning system. To define the semantics of this framework, we extend the first-order stable model semantics by Ferraris, Lee and Lifschitz to allow "intensional functions" and provide analyses of the theoretical properties of this new formalism and on the relationships between this and existing approaches.
Date Created
2016
Agent

Energy-efficient digital circuit design using threshold logic gates

154195-Thumbnail Image.png
Description
Improving energy efficiency has always been the prime objective of the custom and automated digital circuit design techniques. As a result, a multitude of methods to reduce power without sacrificing performance have been proposed. However, as the field of design

Improving energy efficiency has always been the prime objective of the custom and automated digital circuit design techniques. As a result, a multitude of methods to reduce power without sacrificing performance have been proposed. However, as the field of design automation has matured over the last few decades, there have been no new automated design techniques, that can provide considerable improvements in circuit power, leakage and area. Although emerging nano-devices are expected to replace the existing MOSFET devices, they are far from being as mature as semiconductor devices and their full potential and promises are many years away from being practical.

The research described in this dissertation consists of four main parts. First is a new circuit architecture of a differential threshold logic flipflop called PNAND. The PNAND gate is an edge-triggered multi-input sequential cell whose next state function is a threshold function of its inputs. Second a new approach, called hybridization, that replaces flipflops and parts of their logic cones with PNAND cells is described. The resulting \hybrid circuit, which consists of conventional logic cells and PNANDs, is shown to have significantly less power consumption, smaller area, less standby power and less power variation.

Third, a new architecture of a field programmable array, called field programmable threshold logic array (FPTLA), in which the standard lookup table (LUT) is replaced by a PNAND is described. The FPTLA is shown to have as much as 50% lower energy-delay product compared to conventional FPGA using well known FPGA modeling tool called VPR.

Fourth, a novel clock skewing technique that makes use of the completion detection feature of the differential mode flipflops is described. This clock skewing method improves the area and power of the ASIC circuits by increasing slack on timing paths. An additional advantage of this method is the elimination of hold time violation on given short paths.

Several circuit design methodologies such as retiming and asynchronous circuit design can use the proposed threshold logic gate effectively. Therefore, the use of threshold logic flipflops in conventional design methodologies opens new avenues of research towards more energy-efficient circuits.
Date Created
2015
Agent

Toward small community discovery in social networks

153618-Thumbnail Image.png
Description
A community in a social network can be viewed as a structure formed by individuals who share similar interests. Not all communities are explicit; some may be hidden in a large network. Therefore, discovering these hidden communities becomes an interesting

A community in a social network can be viewed as a structure formed by individuals who share similar interests. Not all communities are explicit; some may be hidden in a large network. Therefore, discovering these hidden communities becomes an interesting problem. Researchers from a number of fields have developed algorithms to tackle this problem.

Besides the common feature above, communities within a social network have two unique characteristics: communities are mostly small and overlapping. Unfortunately, many traditional algorithms have difficulty recognizing these small communities (often called the resolution limit problem) as well as overlapping communities.

In this work, two enhanced community detection techniques are proposed for re-working existing community detection algorithms to find small communities in social networks. One method is to modify the modularity measure within the framework of the traditional Newman-Girvan algorithm so that more small communities can be detected. The second method is to incorporate a preprocessing step into existing algorithms by changing edge weights inside communities. Both methods help improve community detection performance while maintaining or improving computational efficiency.
Date Created
2015
Agent

Generating mixed-level covering arrays of lambda = 2 and test prioritization

153593-Thumbnail Image.png
Description
In software testing, components are tested individually to make sure each performs as expected. The next step is to confirm that two or more components are able to work together. This stage of testing is often difficult because there can

In software testing, components are tested individually to make sure each performs as expected. The next step is to confirm that two or more components are able to work together. This stage of testing is often difficult because there can be numerous configurations between just two components.

Covering arrays are one way to ensure a set of tests will cover every possible configuration at least once. However, on systems with many settings, it is computationally intensive to run every possible test. Test prioritization methods can identify tests of greater importance. This concept of test prioritization can help determine which tests can be removed with minimal impact to the overall testing of the system.

This thesis presents three algorithms that generate covering arrays that test the interaction of every two components at least twice. These algorithms extend the functionality of an established greedy test prioritization method to ensure important components are selected in earlier tests. The algorithms are tested on various inputs and the results reveal that on average, the resulting covering arrays are two-fifths to one-half times smaller than a covering array generated through brute force.
Date Created
2015
Agent

On choosability and paintability of graphs

153556-Thumbnail Image.png
Description
Let $G=(V,E)$ be a graph. A \emph{list assignment} $L$ for $G$ is a function from

$V$ to subsets of the natural numbers. An $L$-\emph{coloring} is a function $f$

with domain $V$ such that $f(v)\in L(v)$ for all vertices $v\in V$ and $f(x)\ne

Let $G=(V,E)$ be a graph. A \emph{list assignment} $L$ for $G$ is a function from

$V$ to subsets of the natural numbers. An $L$-\emph{coloring} is a function $f$

with domain $V$ such that $f(v)\in L(v)$ for all vertices $v\in V$ and $f(x)\ne f(y)$

whenever $xy\in E$. If $|L(v)|=t$ for all $v\in V$ then $L$ is a $t$-\emph{list

assignment}. The graph $G$ is $t$-choosable if for every $t$-list assignment $L$

there is an $L$-coloring. The least $t$ such that $G$ is $t$-choosable is called

the list chromatic number of $G$, and is denoted by $\ch(G)$. The complete multipartite

graph with $k$ parts, each of size $s$ is denoted by $K_{s*k}$. Erd\H{o}s et al.

suggested the problem of determining $\ensuremath{\ch(K_{s*k})}$, and showed that

$\ch(K_{2*k})=k$. Alon gave bounds of the form $\Theta(k\log s)$. Kierstead proved

the exact bound $\ch(K_{3*k})=\lceil\frac{4k-1}{3}\rceil$. Here it is proved that

$\ch(K_{4*k})=\lceil\frac{3k-1}{2}\rceil$.

An online version of the list coloring problem was introduced independently by Schauz

and Zhu. It can be formulated as a game between two players, Alice and Bob. Alice

designs lists of colors for all vertices, but does not tell Bob, and is allowed to

change her mind about unrevealed colors as the game progresses. On her $i$-th turn

Alice reveals all vertices with $i$ in their list. On his $i$-th turn Bob decides,

irrevocably, which (independent set) of these vertices to color with $i$. For a

function $l$ from $V$ to the natural numbers, Bob wins the $l$-\emph{game} if

eventually he colors every vertex $v$ before $v$ has had $l(v)+1$ colors of its

list revealed by Alice; otherwise Alice wins. The graph $G$ is $l$-\emph{online

choosable} or \emph{$l$-paintable} if Bob has a strategy to win the $l$-game. If

$l(v)=t$ for all $v\in V$ and $G$ is $l$-paintable, then $G$ is t-paintable.

The \emph{online list chromatic number }of $G$ is the least $t$ such that $G$

is $t$-paintable, and is denoted by $\ensuremath{\ch^{\mathrm{OL}}(G)}$. Evidently,

$\ch^{\mathrm{OL}}(G)\geq\ch(G)$. Zhu conjectured that the gap $\ch^{\mathrm{OL}}(G)-\ch(G)$

can be arbitrarily large. However there are only a few known examples with this gap

equal to one, and none with larger gap. This conjecture is explored in this thesis.

One of the obstacles is that there are not many graphs whose exact list coloring

number is known. This is one of the motivations for establishing new cases of Erd\H{o}s'

problem. Here new examples of graphs with gap one are found, and related technical

results are developed as tools for attacking Zhu's conjecture.

The square $G^{2}$ of a graph $G$ is formed by adding edges between all vertices

at distance $2$. It was conjectured that every graph $G$ satisfies $\chi(G^{2})=\ch(G^{2})$.

This was recently disproved for specially constructed graphs. Here it is shown that

a graph arising naturally in the theory of cellular networks is also a counterexample.
Date Created
2015
Agent

The classification of domain concepts in object-oriented systems

151802-Thumbnail Image.png
Description
The complexity of the systems that software engineers build has continuously grown since the inception of the field. What has not changed is the engineers' mental capacity to operate on about seven distinct pieces of information at a time. The

The complexity of the systems that software engineers build has continuously grown since the inception of the field. What has not changed is the engineers' mental capacity to operate on about seven distinct pieces of information at a time. The widespread use of UML has led to more abstract software design activities, however the same cannot be said for reverse engineering activities. The introduction of abstraction to reverse engineering will allow the engineer to move farther away from the details of the system, increasing his ability to see the role that domain level concepts play in the system. In this thesis, we present a technique that facilitates filtering of classes from existing systems at the source level based on their relationship to concepts in the domain via a classification method using machine learning. We showed that concepts can be identified using a machine learning classifier based on source level metrics. We developed an Eclipse plugin to assist with the process of manually classifying Java source code, and collecting metrics and classifications into a standard file format. We developed an Eclipse plugin to act as a concept identifier that visually indicates a class as a domain concept or not. We minimized the size of training sets to ensure a useful approach in practice. This allowed us to determine that a training set of 7:5 to 10% is nearly as effective as a training set representing 50% of the system. We showed that random selection is the most consistent and effective means of selecting a training set. We found that KNN is the most consistent performer among the learning algorithms tested. We determined the optimal feature set for this classification problem. We discussed two possible structures besides a one to one mapping of domain knowledge to implementation. We showed that classes representing more than one concept are simply concepts at differing levels of abstraction. We also discussed composite concepts representing a domain concept implemented by more than one class. We showed that these composite concepts are difficult to detect because the problem is NP-complete.
Date Created
2013
Agent

Coloring graphs from almost maximum degree sized palettes

151578-Thumbnail Image.png
Description
Every graph can be colored with one more color than its maximum degree. A well-known theorem of Brooks gives the precise conditions under which a graph can be colored with maximum degree colors. It is natural to ask for the

Every graph can be colored with one more color than its maximum degree. A well-known theorem of Brooks gives the precise conditions under which a graph can be colored with maximum degree colors. It is natural to ask for the required conditions on a graph to color with one less color than the maximum degree; in 1977 Borodin and Kostochka conjectured a solution for graphs with maximum degree at least 9: as long as the graph doesn't contain a maximum-degree-sized clique, it can be colored with one fewer than the maximum degree colors. This study attacks the conjecture on multiple fronts. The first technique is an extension of a vertex shuffling procedure of Catlin and is used to prove the conjecture for graphs with edgeless high vertex subgraphs. This general approach also bears more theoretical fruit. The second technique is an extension of a method Kostochka used to reduce the Borodin-Kostochka conjecture to the maximum degree 9 case. Results on the existence of independent transversals are used to find an independent set intersecting every maximum clique in a graph. The third technique uses list coloring results to exclude induced subgraphs in a counterexample to the conjecture. The classification of such excludable graphs that decompose as the join of two graphs is the backbone of many of the results presented here. The fourth technique uses the structure theorem for quasi-line graphs of Chudnovsky and Seymour in concert with the third technique to prove the Borodin-Kostochka conjecture for claw-free graphs. The fifth technique adds edges to proper induced subgraphs of a minimum counterexample to gain control over the colorings produced by minimality. The sixth technique adapts a recoloring technique originally developed for strong coloring by Haxell and by Aharoni, Berger and Ziv to general coloring. Using this recoloring technique, the Borodin-Kostochka conjectured is proved for graphs where every vertex is in a large clique. The final technique is naive probabilistic coloring as employed by Reed in the proof of the Borodin-Kostochka conjecture for large maximum degree. The technique is adapted to prove the Borodin-Kostochka conjecture for list coloring for large maximum degree.
Date Created
2013
Agent

On-line coloring of partial orders, circular arc graphs, and trees

151429-Thumbnail Image.png
Description
A central concept of combinatorics is partitioning structures with given constraints. Partitions of on-line posets and on-line graphs, which are dynamic versions of the more familiar static structures posets and graphs, are examined. In the on-line setting, vertices are continually

A central concept of combinatorics is partitioning structures with given constraints. Partitions of on-line posets and on-line graphs, which are dynamic versions of the more familiar static structures posets and graphs, are examined. In the on-line setting, vertices are continually added to a poset or graph while a chain partition or coloring (respectively) is maintained. %The optima of the static cases cannot be achieved in the on-line setting. Both upper and lower bounds for the optimum of the number of chains needed to partition a width $w$ on-line poset exist. Kierstead's upper bound of $\frac{5^w-1}{4}$ was improved to $w^{14 \lg w}$ by Bosek and Krawczyk. This is improved to $w^{3+6.5 \lg w}$ by employing the First-Fit algorithm on a family of restricted posets (expanding on the work of Bosek and Krawczyk) . Namely, the family of ladder-free posets where the $m$-ladder is the transitive closure of the union of two incomparable chains $x_1\le\dots\le x_m$, $y_1\le\dots\le y_m$ and the set of comparabilities $\{x_1\le y_1,\dots, x_m\le y_m\}$. No upper bound on the number of colors needed to color a general on-line graph exists. To lay this fact plain, the performance of on-line coloring of trees is shown to be particularly problematic. There are trees that require $n$ colors to color on-line for any positive integer $n$. Furthermore, there are trees that usually require many colors to color on-line even if they are presented without any particular strategy. For restricted families of graphs, upper and lower bounds for the optimum number of colors needed to maintain an on-line coloring exist. In particular, circular arc graphs can be colored on-line using less than 8 times the optimum number from the static case. This follows from the work of Pemmaraju, Raman, and Varadarajan in on-line coloring of interval graphs.
Date Created
2012
Agent

Listing combinatorial objects

151231-Thumbnail Image.png
Description
Gray codes are perhaps the best known structures for listing sequences of combinatorial objects, such as binary strings. Simply defined as a minimal change listing, Gray codes vary greatly both in structure and in the types of objects that they

Gray codes are perhaps the best known structures for listing sequences of combinatorial objects, such as binary strings. Simply defined as a minimal change listing, Gray codes vary greatly both in structure and in the types of objects that they list. More specific types of Gray codes are universal cycles and overlap sequences. Universal cycles are Gray codes on a set of strings of length n in which the first n-1 letters of one object are the same as the last n-1 letters of its predecessor in the listing. Overlap sequences allow this overlap to vary between 1 and n-1. Some of our main contributions to the areas of Gray codes and universal cycles include a new Gray code algorithm for fixed weight m-ary words, and results on the existence of universal cycles for weak orders on [n]. Overlap cycles are a relatively new structure with very few published results. We prove the existence of s-overlap cycles for k-permutations of [n], which has been an open research problem for several years, as well as constructing 1- overlap cycles for Steiner triple and quadruple systems of every order. Also included are various other results of a similar nature covering other structures such as binary strings, m-ary strings, subsets, permutations, weak orders, partitions, and designs. These listing structures lend themselves readily to some classes of combinatorial objects, such as binary n-tuples and m-ary n-tuples. Others require more work to find an appropriate structure, such as k-subsets of an n-set, weak orders, and designs. Still more require a modification in the representation of the objects to fit these structures, such as partitions. Determining when and how we can fit these sets of objects into our three listing structures is the focus of this dissertation.
Date Created
2012
Agent

Smart compilers for reliable and power-efficient embedded computing

150743-Thumbnail Image.png
Description
Thanks to continuous technology scaling, intelligent, fast and smaller digital systems are now available at affordable costs. As a result, digital systems have found use in a wide range of application areas that were not even imagined before, including medical

Thanks to continuous technology scaling, intelligent, fast and smaller digital systems are now available at affordable costs. As a result, digital systems have found use in a wide range of application areas that were not even imagined before, including medical (e.g., MRI, remote or post-operative monitoring devices, etc.), automotive (e.g., adaptive cruise control, anti-lock brakes, etc.), security systems (e.g., residential security gateways, surveillance devices, etc.), and in- and out-of-body sensing (e.g., capsule swallowed by patients measuring digestive system pH, heart monitors, etc.). Such computing systems, which are completely embedded within the application, are called embedded systems, as opposed to general purpose computing systems. In the design of such embedded systems, power consumption and reliability are indispensable system requirements. In battery operated portable devices, the battery is the single largest factor contributing to device cost, weight, recharging time, frequency and ultimately its usability. For example, in the Apple iPhone 4 smart-phone, the battery is $40\%$ of the device weight, occupies $36\%$ of its volume and allows only $7$ hours (over 3G) of talk time. As embedded systems find use in a range of sensitive applications, from bio-medical applications to safety and security systems, the reliability of the computations performed becomes a crucial factor. At our current technology-node, portable embedded systems are prone to expect failures due to soft errors at the rate of once-per-year; but with aggressive technology scaling, the rate is predicted to increase exponentially to once-per-hour. Over the years, researchers have been successful in developing techniques, implemented at different layers of the design-spectrum, to improve system power efficiency and reliability. Among the layers of design abstraction, I observe that the interface between the compiler and processor micro-architecture possesses a unique potential for efficient design optimizations. A compiler designer is able to observe and analyze the application software at a finer granularity; while the processor architect analyzes the system output (power, performance, etc.) for each executed instruction. At the compiler micro-architecture interface, if the system knowledge at the two design layers can be integrated, design optimizations at the two layers can be modified to efficiently utilize available resources and thereby achieve appreciable system-level benefits. To this effect, the thesis statement is that, ``by merging system design information at the compiler and micro-architecture design layers, smart compilers can be developed, that achieve reliable and power-efficient embedded computing through: i) Pure compiler techniques, ii) Hybrid compiler micro-architecture techniques, and iii) Compiler-aware architectures''. In this dissertation demonstrates, through contributions in each of the three compiler-based techniques, the effectiveness of smart compilers in achieving power-efficiency and reliability in embedded systems.
Date Created
2012
Agent