Ott: Effective Tool Support for the Working Semanticist

ACM SIGPLAN has judged Ott: Effective Tool Support for the Working Semanticist, by Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša, to be the recipient of the Most Influential ICFP Paper Award for 2017. From the citation:

“Over the past ten years, ICFP researchers have benefitted tremendously from the open-source tool and the effective design space exploration that it promotes.”

n-Queens Completion is NP-Complete

Peter Nightingale and Ian Gent at Falkland Palace, Wednesday, 17 August 2017.
©Stuart Nicol Photography, 2017

Ian Gent, Christopher Jefferson and Peter Nightingale have shown that a classic chess puzzle is NP-Complete. Their paper “Complexity of n-Queens Completion” was published in the Journal of Artificial Intelligence Research on August 30.

The n-Queens puzzle is a classic chess problem: given a chessboard of size n by n, can you place n queens so that no two queens attack each other?  That is, can you place the queens with no two queens are on the same row, column, or diagonal? The n-Queens puzzle has long been known to be simple to solve:  you can solve the problem for all n except 2 and 3, and solutions for all other n can be described in a few lines.  This very simplicity has led to repeated controversy in Artificial Intelligence (AI). The n-Queens puzzle is often used as a benchmark problem, but good results on the problem can always be challenged because the problem is so simple to solve without using AI methods.

The new work follows a challenge on Facebook on New Year’s Day, 2015, when a friend of Ian’s asked him how hard n-Queens is if some queens were already placed on the board.  It turns out, this version (dating from 1850) of the puzzle is only two years younger than the more famous n-Queens problem. The picture shows Peter (left) and Ian (right) with queens on the board at positions suggested by Nauck in 1850, the squares b4 and d5.  Can you put another 6 queens on the board so that the entire board is a solution of 8-Queens?  The general version with some number of queens preplaced on an n by n board is the n-Queens Completion puzzle.

 

With queens at b4 and d5, can you place 6 more queens to get a solution to the 8-queens puzzle? ©Stuart Nicol Photography, 2017

Ian, Christopher and Peter have shown that the n-Queens puzzle is in fact hard, not simple.  It belongs to the complexity classes NP-Complete and #P-Complete. Other NP-Complete problems include the “travelling salesperson problem”, finding cliques in graphs, and many other important problems, from scheduling to circuit layout. This puts n-Queens Completion at the centre of the most important theoretical problem in computer science — it has long been known that either all NP-complete problems are easy, or none of them are. Most computer scientists believe that this means there is no efficient algorithm possible for solving this problem, compared to the very simple techniques long known for n-Queens.
The importance of this work is that it provides researchers with a benchmark that can be used for evaluating AI techniques. Moreover, it helps to explain why so many AI techniques have been used on the n-Queens puzzle. Most techniques do most of their work with some queens partially placed, using some form of (hopefully intelligent) trial and error. In fact it turns out that many researchers – in order to solve a simple problem – have solved it by turning the simple problem of n-Queens into the hard problem of n-Queens Completion.
It does seem that AI researchers should not use n-Queens as a benchmark, but the very closely related n-Queens Completion puzzle is a valid benchmark. As well as the theoretical results, the paper shows how example instances can be generated which appear to be hard in practice. Some caution is still needed, though. It does seem to be quite hard to generate hard instances of n-Queens Completion.
The University has also issued an article on the same paper, under the title “Simple” chess puzzle holds key to $1m prize

Senior Honours: Poster Presentation and Demo Session 2017

Our talented hard working SH students from CS4099: Major Software Project and CS4098: Minor Software Project presented their posters and final year software artifact to staff and students earlier this week.

As Illustrated in the above collage, the busy poster session is the perfect opportunity to discuss output from their year long project with markers, and provides time to share research ideas and reflect on the experience with their peer group. We wish them success with forthcoming exams and look forward to seeing them during June graduation celebrations.

Hot off the press: Type-Driven Development with Idris

A new book, Type-Driven Development with Idris has just been published by Manning Publications. Written by Dr Edwin Brady, the creator of Idris, Type-Driven Development with Idris teaches you how to improve the performance and accuracy of your programs by taking advantage of a state-of-the-art type system.

Type-driven development is an approach to programming that embraces types as the foundation of your code. It is based on the concept of “dependent types”, which allow you to express relationships and other assumptions directly in your code, and have these assumptions checked by the compiler. With this approach, you can define specifications early in development and write code that’s easy to maintain, test, and extend.

Dr Brady said:

“Idris arose as a result of my own research into program verification and language design with advanced type systems. After spending several years immersed in the concept of programming with dependent types, I felt there was a need for a language designed for developers and practitioners as well as researchers. By teaching the concept of type-driven development using Idris, the book aims to make state-of-the-art verification techniques accessible to software practitioners.”

The book is currently available via MANNING publications: https://www.manning.com/books/type-driven-development-with-idris. ePub and Kindle versions available from April 10th. The source code, chapter 1 and chapter 13 are available as free downloads.

Distinguished Lecture Series 2017: Dr David Manlove

On March 31st, Dr David Manlove from the University of Glasgow, delivered the semester two distinguished lectures in Lower and Upper College Hall. The overall title was algorithms for healthcare-related matching problems.

David started with an overview of complexity theory and solving hard problems. He gave examples of this in practice, for example how researchers constructed a best-possible tour around the best 20,000 pubs in the UK. The second lecture focussed on how to assign junior doctors to hospitals in the best way, a very practical problem but with interesting complexity issues. The final lecture focussed on the life-changing topic of how to set up exchanges of kidneys between healthy donors and patients needing transplants. David talked about how his expertise in algorithms has been translated into regularly finding the best possible matches which then result in real transplants taking place.

David is pictured above at various stages of the distinguished lecture series and outside College Hall with Head of School, Prof Steve Linton, Prof Ian Gent and Dr Ishbel Duncan,

Videos from the DLS can be accessed on Vimeo –
Lecture 1: https://vimeo.com/211633740
Lecture 2: https://vimeo.com/211634119
Lecture 3: https://vimeo.com/211634923

Images courtesy of Ryo Yanagida.

Team NOMAD win IDEA Explosion 2017

Congratulations to PhD students Shyam Reyal and Simone Conte , from Computer Science and Senior Scientific Officer Tomas Lebl, from Chemistry who presented NOMAD (NMR Online Management and Datastore) at IDEA Explosion 2017 and emerged victorious. Shyam delivered a five-minute elevator pitch, whilst Simone and Tomas responded to questions. Judges acknowledged that NOMAD has huge potential with researchers, and were impressed that it has been used in St Andrews for the past 5 years, with other universities now lined-up to make use of its services, fully supporting the use of the prize money to set-up a company.


Continue reading

Wrist Worn Haptic Feedback Device

One of our PhD students Esma Mansouri Benssassi and her supervisor Dr Erica Ye defined a requirement for a wrist worn device to group a number of Haptic feedback elements for an experiment they wished to carry out. The on-board Haptic elements are two eccentric rotating mass micro motors and an linear resonant actuator. Initial circuit schematics and printed circuit board designs were created in an Open Source Electronics Design Automation Suite KiCAD EDA. The resulting printed circuit board (PCB) design was made on the CS CNC Router , this produces the PCB by engraving the copper clad fibreglass-epoxy board with a Vee cutter.

PCBBare Circular Engraved PCB

The case for the PCB was created in Autodesk Inventor and was 3D printed using the CS Makerbot 2X 3D printer.

Blank PCB and 3D Printed Case

Haptic Wristband and Haptic Transducers

The wrist worn Haptic feedback device will be connected via an umbilical cable to the main control Feather M0 embedded ARM and Haptic Driver breadboard. This is an ARM microcontroller and wifi module which can be programmed using the Arduino IDE. Code for the ARM processor will enable stored and custom waveforms to be played on the haptic devices on the wrist.

Haptic Feedback Breadboard Assembly

Research on containers for HPC environments featured in CACM and HPC Wire

Rethinking High performance computing Platforms: Challenges, Opportunities and Recommendations, co-authored by Adam Barker and a team (Ole Weidner, Malcolm Atkinson, Rosa Filgueira Vicente) in the School of Informatics, University of Edinburgh was recently featured in the Communications of the ACM and HPC Wire.

The paper focuses on container technology and argues that a number of “second generation” high-performance computing applications with heterogeneous, dynamic and data-intensive properties have an extended set of requirements, which are not met by the current production HPC platform models and policies. These applications (and users) require a new approach to supporting infrastructure, which draws on container-like technology and services. The paper then goes on to describe cHPC: an early prototype of an implementation based on Linux Containers (LXC).

Ali Khajeh-Hosseini, Co-founder of AbarCloud and former co-founder of ShopForCloud (acquired by RightScale as PlanForCloud) said of this research, “Containers have helped speed-up the development and deployment of applications in heterogeneous environments found in larger enterprises. It’s interesting to investigate their applications in similar types of environments in newer HPC applications.

Data and the User Experience in Retail

Event details

  • When: 6th March 2017 15:00 - 16:00
  • Where: Honey 110 - John Honey Teaching Lab
  • Format: Seminar

The Hut Group develop and manage a proprietary eCommerce platform that handled over half a billion pounds of revenue last year. UX within the company is responsible for optimising user flows through the website, and working with Design departments to deliver user delight. With over 30 distinct site brands internally, and several external clients, the team attempt to strike a balance between optimising sites for revenue and user delight. This talk is about the challenges of UX within a wider business organisation, and the role that Computer Science graduates can play in a multidisciplinary UX team.

Bio:
Elliott joined The Hut Group in June, starting in the Research and Development department. He worked on developing a dashboard for use inside the business, and developed a series of prototypes to show users Social Media content on-site. He now heads the User Experience (UX) department. Prior to joining THG, Elliott worked at Skyscanner as a front-end developer whilst graduating from St Andrews in Computer Science with several modules in HCI.