English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Optimal certifying algorithms for linear and lattice point feasibility in a system of UTVPI constraints by Piotr Jerzy Wojciechowski Master of Science in Computer Science West Virginia University K. Subramani, Ph.D., Chair This thesis is concerned with the design and analysis of time-optimal and spaceoptimal, certifying algorithms for checking the linear and lattice point feasibility of a class of constraints called Unit Two Variable Per Inequality (UTVPI) constraints. In a UTVPI constraint, there are at most two non-zero variables per constraint, and the coefficients of the non-zero variables belong to the set {+1, −1}. These constraints occur in a number of application domains, including but not limited to program verification, abstract interpretation, and operations research. As per the literature, the fastest known certifying algorithm for checking lattice point feasibility in UTVPI constraint systems ([1]), runs in O(m · n + n · log n) time and O(n) space, where m represents the number of constraints and n represents the number of variables in the constraint system. In this paper, we design and analyze new algorithms for checking the linear feasibility and the lattice point feasibility of UTVPI constraints. Both of the presented algorithms run in O(m · n) time and O(m + n) space. Additionally they are certifying in that they produce satisfying assignments in the event that they are presented with feasible instances and refutations in the event that they are presented with infeasible instances. The importance of providing certificates cannot be overemphasized, especially in mission-critical applications. Our approaches for both the linear and the lattice point feasibility problems in UTVPI constraints are fundamentally different from existing approaches for these problems (as described in the literature), in that our approaches are based on new insights on using well-known inference rules.