Research Reports for 2007

CSR 1-2007
Polynomial time SAT decision for linearly lean complement-invariant clause-sets of minimal reduced deficiency
Oliver Kullmann
abstract    PDF
CSR 2-2007
Computability on topological spaces via domain representations
V Stoltenberg-Hansen and J V Tucker
abstract    PDF
CSR 3-2007
PCC 2007, Proof, Computation, Complexity (International Workshop Abstracts)
abstract    PDF
CSR 4-2007
Exploring the Relationship between Faces and Aging in Image-based Age Transformation
Daniel Hubball, Min Chen and Phil W. Grant
abstract    PDF
CSR 5-2007
Meadows
J A Bergstra, Y Hirschfeld and J V Tucker
abstract    PDF
CSR 6-2007
Algebraic Models of Simultaneous Multithreaded and Multi-Core Microprocessors
N A Harman
abstract    PDF
CSR 7-2007
Modelling SMT and CMT Processors: A Simple Case Study
N A Harman
abstract    PDF
CSR 8-2007
Constraint satisfaction problems in clausal form: Autarkies and minimal unsatisfiability
Oliver Kullmann
abstract    PDF
CSR 9-2007
Alternative subcell discretisations for viscoelastic flow: Velocity gradient approximation
F. Belblidia, H. Matallah and M. F. Webster
abstract    PDF
CSR 10-2007
Excess pressure-drop estimation in contraction and expansion flows for constant shear viscosity, strain-hardening fluids- Part 2
J. P. Aguayo, H.R. Tamaddon-Jahromi and M. F. Webster
abstract    PDF
CSR 11-2007
Generalised approach for transient computation of start-up pressure-driven viscoelastic flow- Part 2
I. J. Keshtiban, B. Puangkird, H.R. Tamaddon-Jahromi and M. F. Webster
abstract    PDF
CSR 12-2007
Constraint satisfaction problems in clausal form: Autarkies, deficiency and minimal unsatisfiability
Oliver Kullmann
abstract    PDF
CSR 13-2007
Digital Libraries on an iPod: beyond the client-server model
David Bainbridge, Steve Jones, Sam McIntosh & Matt Jones
abstract    PDF
CSR 14-2007
A map-based Place-browser for a PDA
David Bainbridge, Matt Jones & David Arter
abstract    PDF
CSR 15-2007
On the computational complexity of cut-reduction
Klaus Aehlig & Arnold Beckmann
abstract    PDF
CSR 16-2007
VizThis : Rule-based Semantically Assisted Information Visualizationn
Owen Gilson, Nuno Silva, Phil W. Grant, Min Chen, and João Rocha
abstract    PDF

CSR 1-2007 Polynomial time SAT decision for linearly lean complement-invariant clause-sets of minimal reduced deficiency

Oliver Kullmann

We study complement-invariant clause-sets F, where for every clause CF we have C‾ = {x‾ : x ∈ C} ∈ F, i.e., F is closed under elementwise complementation of clauses. The reduced deficiency of a clauseset F is defined as δr(F) := ½ (δ(F) - n(F)), where δ(F) = c(F) - n(F) is the difference of the number of clauses and the number of variables, while the maximal reduced deficiency is δr*(F) := maxF'⊆F δr(F') ≥0. If F is complement-invariant and linearly lean (has no non-trivial linear autarkies) then we have δr*(F) = δr(F). We show polynomial time SAT decision for complement-invariant clause-sets F with δr*(F) = 0, exploiting the (non-trivial) decision algorithm for sign-non-singular matrices given by [Robertson, Seymour, Thomas 1999]. Minimally unsatisfiable complement-invariant clause-sets F fulfil δr(F) ≥ 0, and we immediately get polynomial time decidability of minimally unsatisfiable complement-invariant clause-sets F with δr(F) = 0, but we can give also somewhat more direct algorithms and characterisations (especially for sub-classes)
Report Titles


CSR 2-2007 Computability on topological spaces via domain representations

V Stoltenberg-Hansen and J V Tucker

Domains are ordered structures designed to model computation with approximations. We give an ntroduction to the theory of computability for topological spaces based upon representing topological spaces and algebras using domains. Among the topics covered are: different approaches to computability on topological spaces; orderings, approximations and domains; making domain representations; effective domains; classifying representations; type two effectivity and domains; special representations for inverse limits, regular spaces and metric spaces. Lastly, we sketch a variety of applications of the theory in algebra, calculus, graphics and hardware.
Report Titles


CSR 3-2007 PCC 2007, Proof, Computation, Complexity (International Workshop Abstracts)

"Proof, Computation, Complexity" (PCC) is a series of annual workshops that aims to stimulate research in proof theory, computation, and complexity, focusing on issues which combine logical and computational aspects. Its topics include applications of formal inference systems in computer science as well as new developments in proof theory motivated by computer science demands. Specific areas of interest are foundations for specification and programming languages, logical methods in specification and program development including program extraction from proofs, type theory, new developments in structural proof theory, and implicit computational complexity.
Previous PCC workshops were held in Tuebingen (2002), Dresden (2003 and 2004), Lisbon (2005) and Ilmenau (2006).
Report Titles


CSR 4-2007 Exploring the Relationship between Faces and Aging in Image-based Age Transformation

Aging has considerable effects on the appearance of the human face and is dif cult to simulate using a universallyapplicable global model. In this paper, we present a data-driven framework for image-based facial age progression (and regression) automatically in conjunction with a database of facial images. We build parameterized models for both face modeling and age-transformation based on a subset of imagery data selected according to an input image and associated metadata. In order to obtain a person-speci c mapping in the model space from an encoded face description to an encoded age-transformation, we employed genetic programming to automatically train a solution by learning from example transformations in the selected subset. Unlike most optimization approaches which typically operate only in the parameter space of a presupposed functional model, genetic programming enables us to infer from the input and the database the most appropriate functional model to be used for transforming the input face. It is particularly suited for aging simulation where the current understanding is not yet adequate for producing an effective global aging model. In comparison with the existing techniques for age transformation, We have achieved a noticeable improvement in terms of the resemblance between the output images and the actual target images (which are unknown to the training process), demonstrating the effectiveness and usability of this new approach.
Report Titles


CSR 5-2007 Meadows

A meadow is a commutative ring with an inverse operator satisfying two equations and in which 1/0 = 0. All fields and products of fields can be viewed as meadows. After reviewing alternate axioms for inverse, we start the development of a theory of meadows. We give a general representation theorem for meadows and find, as a corollary, that the equational theory of meadows coincides with the equational theory of zero totalized fields. We also prove representation results for meadows of finite characteristic.
Report Titles


CSR 6-2007 Algebraic Models of Simultaneous Multithreaded and Multi-Core Microprocessors

Superscalar microprocessors execute multiple instructions simultaneously by virtue of large amounts of (possibly duplicated) hardware. Much of this hardware is idle at least part of the time. simultaneous multithreaded (SMT) microprocessors utilize this idle hardware by interleaving multiple independent execution threads. In essence, a single physical processor appears to be multiple virtual processors. multi-core, or chip-level multithreaded (CMT) processors duplicate the execution pipeline, while sharing other resources. Both approaches increase processor hardware utilization (and hence speed) by introducing thread-level parallelism.
The key questions we consider in this paper are: how do we model SMT/CMT processors? In particular, how do we model multiple, parallel, intercommunicating threads of execution, whose behaviour is defined in terms of some lower level implementation? And, what does it mean for such SMT/CMT models to be correct? The model developed here focusses particularly on (a) the relationship between timing behaviour at different levels of abstraction; and (b) what it means for a representation of a processor at one level of abstraction (typically representing an implementation) to be correct with respect to another (typically representing a specification consisting of multiple interacting threads). An inevitable, and realistic, consequence of the model of SMT/CMT processors developed is a weakening of the long-established principle of separation between a processor implementation and specification.
Report Titles


CSR 7-2007 Modelling SMT and CMT Processors: A Simple Case Study

This paper builds on a series examining models of pipelined and superscalar microprocessors and their correctness by extending them to Simulataneous Multithreaded (SMT) and Chip-Level Multithreaded (CMT) processors. SMT and CMT implementations behave, to the programmer, like separate processors (virtual in the case of SMT) that communicate by means of shared state. The timing relationships are complex: the multiple (virtual) processors effectively operate over separate clocks, that are related by their temporal relationship with the corresponding implementation and its state. This relationship is complicated by the fact that SMT processors are inherently superscalar. In practice, CMT processors are also likely to be superscalar.
The existing tools for modeling microprocessors and their correctness are extended to SMT and CMT systems. The model is designed to preserve the (likely large) investment in time and effort made in developing non-SMT/CMT processor models. The model is illustated by a simple, dual-core pipelined processor example. The model also accurately reflects the inevitable presence of aspects of a SMT/CMT processor’s implementation in the programmer-visible behaviour.
Report Titles


CSR 8-2007 Constraint satisfaction problems in clausal form: Autarkies and minimal unsatisfiability

We consider the problem of generalising boolean formulas in conjunctive normal form by allowing non-boolean variables, where our goal is to maintain combinatorial properties. Requiring that a literal involves only a single variable, the most general form of literals is given by the well-known "signed literals", however we will argue that only the most restricted form of generalised clause-sets, corresponding to "sets of no-goods" in the AI literature, maintains the essential properties of boolean conjunctive normal forms. We start our investigations by building up a solid foundation for (generalised) clause-sets, including the notion of autarky systems, the interplay between autarkies and resolution, and basic notions of (DP-)reductions. As a basic combinatorial parameter of generalised clause-sets, we introduce the (generalised) notion of deficiency, which in the boolean case is the difference between the number of clauses and the number of variables. We obtain fixed parameter tractability (FPT) of satisfiability decision for generalised clause-sets, using as parameter the maximal deficiency (over all sub-clause-sets). Another central result in the boolean case regarding the deficiency is the classification of minimally unsatisfiable clause-sets with low deficiency (MU(1), MU(2), ...). We generalise the well-known characterisations of boolean MU(1). The proofs for FPT and MU(1) are not straight-forward, but are obtained by an interplay between suitable generalisations of techniques and notions from the boolean case, and exploiting combinatorial properties of the natural translation of (generalised) clause-sets into boolean clause-sets. Of fundamental importance here is autarky theory, and we concentrate especially on matching autarkies (based on matching theory). A natural question considered here is to determine the structure of (matching) lean clause-sets, which do not admit non-trivial (matching) autarkies. Special lean clause-sets are minimally unsatisfiable (generalised) clause-sets, and we consider the generalisation to irredundant clause-sets, so that also satisfiable clause-sets can be taken into account, with a special emphasise on hitting clause-sets (which are irredundant in a very strong sense) and the generalisation to multihitting clause-sets.
Report Titles


CSR 9-2007 Alternative subcell discretisations for viscoelastic flow: Velocity gradient approximation

Under subcell discretisation for viscoelastic flow, we have given further consideration to the compatibility of function spaces for stress/velocity-gradient approximation (see [JNNFM, special issue AERC 2006). This has been conducted through the three scheme discretisations (quad-fe(par), fe(sc) and fe/fv(sc)). In this companion study, we have extended the application of the original implementation for velocity gradient approximation, which was of localised superconvergent recovered form, continuous and quadratic on the parent fe-triangular element. This has led to the consideration of both localised (pointwise) and global (Galerkin weighted-residual) approximations for velocity gradients, highlighting some of their advantages and disadvantages. Each representation is based on linear/quadratic order upon parent or subcell element stencils. We consider Oldroyd modelling and the contraction flow benchmark, covering abrupt and rounded-corner planar geometries. The localised super-convergent quadratic velocitygradient treatment affords strong stability and accuracy properties for the three scheme variants. Through associated analysis, we have successfully linked global approximations to their localised counterparts, depicting the inadequacy of inaccurate but stable versions through their corresponding solution features. The inaccuracy of the global treatment can be repaired through an increase in mass iteration number. The efficiency of localised schemes is particularly attractive over their global alternatives, being less restrictive to choice of spatial-order. Such schemes come into their own when chosen to represent strongly localised solution features, such as arise in non-smooth flows.
Report Titles


CSR 10-2007 Excess pressure-drop estimation in contraction and expansion flows for constant shear viscosity, strain-hardening fluids- Part 2

This article addresses the issue of reproducing quantitative pressure-drop predictions for constant shear-viscosity fluids in contraction and contraction/expansion flow geometries. Experimental observations on pressure-drop for severe strain hardening Boger fluids reveal significant enhancement above Newtonian fluids in axisymmetric but not planar configurations. This discrepancy has eluded predictive capability to date in contraction flows when utilising Oldroyd models. Here, we identify why this is so. The 4:1:4 contraction/expansion flow and adjustment of material parameters provides the key to resolving this dilemma in comparative form to the 4:1 counterpart problem. During the investigation, Oldroyd-B fluid compositions of various solvent:polymeric viscosity ratio splits are employed. A hybrid finite element/volume algorithm of incremental pressure-correction time-stepping structure is utilised, reflecting some novel features with respect to the discrete treatment of pressure.
Report Titles


CSR 11-2007 Generalised approach for transient computation of start-up pressure-driven viscoelastic flow- Part 2

This article investigates a generalised solution approach for transient viscoelastic flows employing consistent dynamic boundary conditions. Such a procedure vaunts three key properties - independence of reference frame, problem dimension and constitutive equation type. Three different boundary condition protocols have been investigated, two transient and one steady, through a time-dependent incremental pressure-correction formulation with a hybrid finite element/finite volume scheme. These procedures are compared and contrasted through application to pressure-driven start-up flow in 4:1 planar rounded-corner contractions for two fluid models, Oldroyd and pom-pom. Some novel differences are highlighted in the dynamic evolution of flow structure and the impact upon stress generation, as a consequence of protocol, whether steady or transient, under flow-rate or force-driven control. Overshoot-undershoot kinematics observed under any particular flow protocol have been mutually linked to the precise boundary conditions imposed. Under flow-rate controlled protocols, large oscillations are stimulated in pressure, which may disturb computational tractability. Comparatively, the evolution of force-driven flow can provide considerably smoother development patterns in pressure, with largest attached vortices and strong oscillatory vortex structure features. Specifically under transient flow-rate control, some distinct complex flow features have emerged, including reversed flow, followed by vortex detachment and reattachment. For pom-pom SXPP-fluids and force-driven protocol, transient flow development is observed to be relatively smooth and non-oscillatory at a Weissenburg number of unity. At larger levels of Weissenburg number, transient overshoots have been detected in characteristic variables of stress and molecular backbone-stretch. In addition, Weissenburg number continuation to steady-state, has been shown to disconnect the dynamics between velocity and stress, which prevents highly-elastic localised regions from developing.
Report Titles


CSR 12-2007 Constraint satisfaction problems in clausal form: Autarkies, deficiency and minimal unsatisfiability

We consider the problem of generalising boolean formulas in conjunctive normal form by allowing non-boolean variables, with the goal of maintaining combinatorial properties. Requiring that a literal involves only a single variable, the most general form of literals is given by the well-known "signed literals", however we will argue that only the restricted form of "negative monosigned literals" and the resulting generalised clause-sets, corresponding to “sets of no-goods” in the AI literature, maintain the essential properties of boolean conjunctive normal forms. We build up a solid foundation for (generalised) clause-sets, including the notion of autarky systems, the interplay between autarkies and resolution, and basic notions of (DP-)reductions. As a basic combinatorial parameter of generalised clause-sets we introduce the (generalised) notion of deficiency, which in the boolean case is the difference between the number of clauses and the number of variables. Using as parameter the maximal deficiency (over all sub-clause-sets) we obtain fixed parameter tractability (FPT) of satisfiability decision for generalised clause-sets. Another central result in the boolean case regarding the deficiency is the classification of minimally unsatisfiable clause-sets with low deficiency (MU(1), MU(2), ...). We generalise the well-known characterisations of boolean MU(1). The proofs for FPT and MU(1) exploit combinatorial properties of the natural translation of (generalised) clause-sets into boolean clause-sets. Autarky theory plays a fundamental role here, and we concentrate especially on matching autarkies (based on matching theory). A natural question is to determine the structure of (matching) lean clause-sets, which do not admit non-trivial (matching) autarkies. Minimally unsatisfiable (generalised) clause-sets are special lean clause-sets, and we consider the generalisation to irredundant clause-sets, so that also satisfiable clause-sets can be taken into account, including hitting clause-sets, which are irredundant in a very strong sense, and the generalisation to multihitting clause-sets. Regarding regular hitting clause-sets we establish the connection to the theory of multiclique partitions of multigraphs, and we generalise the fundamental facts regarding the deficiency. We conclude with a list of open problems and conjectures.
Report Titles


CSR 13-2007 Digital Libraries on an iPod: beyond the client-server model

This paper describes an experimental system that enhanced an iPod with digital library capabilities. Using the open source digital library software Greenstone as a base, this paper more specifically maps out the technical steps necessary to achieve this, along with an account of our subsequent experimentation. This included command-line usage of Greenstone’s basic runtime system on the device, augmenting the iPod’s main interactive menu-driven application to include searching and hierarchical browsing of digital library collections stored locally, and a selection of “launcher” applications for target documents such as text files, images and audio. Media rich applications for digital stories and collaging were also developed. We also configured the iPod to run as a web server to provide digital library content to others over a network, effectively turning the traditional mobile client-server upsidedown.
Report Titles


CSR 14-2007 A map-based Place-browser for a PDA

This article describes PlaceBrowser, a PDA based application that allows the user of the application to navigate around an area of geographical interest, such as a city, using a zoomable, panable hierarchy of aerial images, in a fashion similar to Google Maps. The novel aspect to the work is that an area of precise interest within the map can be pin-pointed by the user by directly dragging out a rectangular area on the map. This forms the source to a spatial search that returns landmarks that are then used to trigger aWeb based query. The results of this query are displayed to the user. The net effect is that, in response to dragging out a retangular area, web pages that are relevent to this area but have not been explicitly geo-spatially tagged with metadata (longitigude,latitude) are shown to the user.
Report Titles


CSR 15-2007 On the computational complexity of cut-reduction

We investigate the complexity of cut-reduction on proof notations, in particular identifying situations where cut-reduction operates feasibly, i.e., sub-exponential, on proof notations. We then apply the machinery to characterise definable search problem in Bounded Arithmetic. To explain our results with an example, let E(d) denote Mints' continuous cut-reduction operator which reduces the complexity of all cuts of a propositional derivation d by one level. We will show that if all subproofs of d can be denoted with notations of size s, and the height of d is h, then sub-proofs of the derivation E(d) can be denoted by notations of size h.(s+O(1)). Together with the observation that determining the last inference of a denoted derivation as well as determining notations for immediate sub-derivations is easy (i.e., polynomial time computable), we can apply this result to re-obtain that the Σbi -definable functions of the Bounded Arithmetic theory Si2 are in the i-th level of the polynomial time hierarchy of functions FPΣbi-1.
Report Titles


CSR 16-2007 VizThis : Rule-based Semantically Assisted Information Visualization

Information Visualization can be considered as the task of mapping data entities in a source řle to representation artefacts in a tar- get visualization format. As such, mapping plays a signiřcant role in this process. The řeld of Ontology Mapping presents a wealth of work in the information mapping domain which we propose to exploit by applying it to Information Visualization for the Semantic Web. In this paper we describe a User Interface and a tool (VizThis) which demonstrates the proposed approach. We discuss the beneřts which a mapping paradigm brings to Information Visualization, including automaticity and rule con- straint. The system facilitates automatic mapping while still allowing users the ability to tweak the chosen mappings in order to improve the cognitive value of the visualizations. Additionally, the mapping choices available are constrained by rules governed by the characteristics of both the source and target format. A worked example is provided together with the results of a qualitative user evaluation of the resulting visual- izations.
Report Titles