CICLOPS-WLPE on Thursday, July 15th

09:00‑10:00 Session 1
Chair: Neng-Fa Zhou
Location: IF 4.31+4.33
09:00 Naoyuki Tamura (Kobe University, Japan)
Solving Constraint Satisfaction Problems by a SAT Solver

A Boolean Satisfiability Testing Problem (SAT) is a combinatorial problem to find a Boolean variable assignment which satisfies all given Boolean formulas. Recent performance improvement of SAT technologies makes SAT-based approaches applicable for solving hard and practical combinatorial problems, such as planning, scheduling, hardware/software verification, and constraint satisfaction.<br/>

Sugar is a SAT-based constraint solver based on a new encoding method called order encoding which was first used to encode job-shop scheduling problems by Crawford and Baker. In the order encoding, a comparison x<=a is encoded by a different Boolean variable for each integer variable x and integer value a. The Sugar solver shows a good performance for a wide variety of problems, and became the winner of the GLOBAL categories in 2008 and 2009 CSP solver competitions.<br/>

The talk will provide an introduction to modern SAT solvers, SAT encodings, implementation techniques of the Sugar solver, and its performance evaluation.

10:30‑12:30 Session 2
Location: IF 4.31+4.33
10:30 Peter Biener, François Degrave and Wim Vanhoof
A Test Automation Framework for Mercury

In this paper we present a test automation framework for Mercury programs. We developed a method that generates runnable Mercury code from a formalized test suite, and that provides a report on execution about the success of test cases. Our framework also provides a coverage tool which identifies and provides a visualization of coverage degree of the program when executing a given test suite.

11:00 Petra Hofstedt
Realizing evaluation strategies by hierarchical graph rewriting

We discuss the realization of evaluation strategies for the concurrent constraint-based functional language CCFL within the translation schemata when compiling CCFL programs into the hierarchical graph rewriting language LMNtal. The support of LMNtal to express local computations and to describe the migration of processes and rules between local computation spaces allows a clear and simple realization of typical evaluation strategies.

11:30 Nicos Angelopoulos and Paul Taylor
An extensible web interface for databases and its application to storing biochemical data

This paper presents a generic web-based database interface implemented in Prolog. We discuss the advantages of the implementation platform and demonstrate the system's applicability in providing access to integrated biochemical data. Our system exploits two libraries of SWI-Prolog to create a schema-transparent interface within a relational setting. As is expected in declarative programming, the interface was written with minimal programming effort due to the high level of the language and its suitability to the task. We highlight two of Prolog's features that are well suited to the task at hand: term representation of structured documents and relational nature of Prolog which facilitates transparent integration of relational databases. Although we developed the system for accessing in-house biochemical and genomic data the interface is generic and provides a number of extensible features. We describe some of these features with references to our research databases. Finally we outline an in-house library that facilitates interaction between Prolog and the \sw{R} statistical package. We describe how it has been employed in the present context to store output from statistical analysis on to the database.

12:00 Paulo Moura
Meta-Predicate Semantics

We describe and compare design choices for meta-predicate semantics, as found in representative Prolog module systems and in Logtalk. We look at the consequences of these design choices from a pragmatic perspective, discussing explicit qualification semantics, computational reflection support, expressiveness of meta-predicate declarations, safety of meta-predicate definitions, portability of meta-predicate definitions, and meta-predicate performance. Our aim is to provide useful insight for debating meta-predicate semantics and portability issues based on actual implementations and common usage patterns.

14:00‑15:00 Session 3
Chair: German Vidal
Location: IF 4.31+4.33
14:00 Michael Codish (Ben-Gurion University of the Negev, Israel)
Programming with Boolean Satisfaction

In recent years, research on Boolean satisfiability (SAT) is generating remarkably powerful SAT solvers capable of handling larger and larger SAT instances. With the availability of progressively stronger SAT solvers, an accumulating number of applications have been developed which demonstrate that real world problems can often be solved by encoding them into SAT. One of the success stories is the application to termination analysis where we aim to automatically provide proofs of termination for software. Here, in the past five years, Boolean satisfiability has completely revolutionized the field.<br/>

One major obstacle in applying SAT solving to a given problem is to devise a suitable representation of the problem. This involves mapping the problem to a propositional formula in such a way that a model of the formula represents a solution of the original problem. This activity is just like programming (with logic): variables are Booleans and programs are formulas in conjunctive normal form. With expertise in declarative, logic and constraint programming, our community is well situated to join efforts in the development of new SAT encoding techniques and new applications for SAT solving. In this talk I will survey several SAT encoding techniques which come up in the application to termination analysis as well as in other applications.

15:30‑18:00 Session 4
Location: IF 4.31+4.33
15:30 Jan Wielemaker and Vítor Santos Costa
Portability of Prolog programs: theory and case-studies

(Non-)portability of Prolog programs is widely considered as an important factor in the lack of acceptance of the language. Since 1995, the core of the language is covered by the ISO standard 13211-1. Since 2007, YAP and SWI-Prolog have established a basic compatibility framework. This article describes and evaluates this framework. The aim of the framework is running the same code on both systems rather than migrating an application. We show that today, the portability within the family of Edinburgh/Quintus derived Prolog implementations is good enough to allow for maintaining portable real-world applications.

16:00 Dimitar Shterionov, Angelika Kimmig, Theofrastos Mantadelis and Gerda Janssens
DNF Sampling for ProbLog Inference

Inference in probabilistic logic languages such as ProbLog, an extension of Prolog with probabilistic facts, is often based on a reduction to a propositional formula in DNF. Calculating the probability of such a formula involves the disjoint-sum-problem, which is computationally hard. In this work we introduce a new approximation method for ProbLog inference which exploits the DNF to focus sampling. While this DNF sampling technique has been applied to a variety of tasks before, to the best of our knowledge it has not been used for inference in probabilistic logic systems. The paper also presents an experimental comparison with another sampling based inference method previously introduced for ProbLog.

16:30 Vasco Pedro and Salvador Abreu
Distributed Work Stealing for Constraint Solving

With the dissemination of affordable parallel and distributed hardware, parallel and distributed constraint solving has lately been the focus of some attention. To effectually apply the power of distributed computational systems, there must be an effective sharing of the work involved in the search for a solution to a Constraint Satisfaction Problem (CSP) between all the participating agents, and it must happen dynamically, since it is hard to predict the effort associated with the exploration of some part of the search space. We describe and provide an initial assessment of an implementation of a work stealing based approach to distributed CSP solving.

17:00 Paulo André and Salvador Abreu
Casting the WAM as an EAM

Logic programming provides a very high-level view of programming, which comes at the cost of some execution efficiency. Improving performance of logic programs is thus one of the holy grails of Prolog system implementations and a wide range of approaches have historically been taken towards this goal. Designing computational models that both exploit the available parallelism in a given application and that try hard to reduce the explored search space has been an ongoing line of research for many years. These goals in particular have motivated the design of several computational models, one of which is the Extended Andorra Model (EAM). In this paper, we present a preliminary specification and implementation of the EAM with Implicit Control, WAM2EAM, which supplies regular WAM instructions with an EAM-centered interpretation.

17:30 Gopal Gupta, Neda Saeedloei (University of Texas at Dallas)
Logic Programming Foundations of Cyber-Physical Systems

Cyber-physical systems are becoming ubiquitous. Almost every device today has a controller that reads inputs through sensors, does some processing and then performs actions through actuators. Examples include controller systems in cars (Anti-lock Brake System, Cruise Controllers, Collision Avoidance, etc.), automated manufacturing, smart homes, robots, etc. These controllers are discrete digital systems whose inputs are continuous physical quantities (e.g., time, distance, acceleration, temperature, etc.) and whose outputs control physical (analog) devices. Thus, CPSs involve both digital and analog data. In addition, CPSs are assumed to run forever, and many CPSs may run concurrently with each other.

Thus, CPSs have the following four characteristics: (i) they perform discrete computations, (ii) they deal with continuous quantities, (iii) they are concurrent, and (iv) they run forever. Due to the fundamentally discrete nature of computation, researchers have had difficulty dealing with continuous quantities in computations (typical approaches discretize continuous quantities, e.g., time). Likewise, modeling of perpetual computations is not well understood (only recently, techniques such as co-induction have been introduced to formally model rational, infinite computations). Concurrency is reasonably well understood, but when combined with continuous quantities and with perpetual computations, CPSs become extremely hard to model faithfully.

The CPS research community has been looking for formalisms for faithfully modeling and reasoning with CPS. We show how logic programming with its powerful features fills the gap. Our approach is based on using logic programming for modeling computations, constraint logic programming for modeling continuous physical quantities, co-induction for modeling perpetual execution and coroutining for modeling concurrency in CPSs. CPSs are thus represented as coroutined co-inductive constraint logic programs which are subsequently used to elegantly verify cyber-physical properties of the system relating to safety, liveness and utility. This logic program can also be used for automatically generating implementation code for the CPS.