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 C ∈ F 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
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