Publications by Martin Henz

The most significant publications are listed below; for abstract and full paper, click on the paper title. For the more obscure papers, search in Google Scholar or dblp.
2016

2015

2014

2013

Earlier

User-defined Difficulty Levels for Automated Question Generation

Rahul Singhal, Shubham Goyal, Martin Henz

28th International Conference on Tools with Artificial Intelligence, San Jose, CA, USA, 2016.

We propose a difficulty model for generating questions across formal domains according to the difficulty level provided by the user. Our model is interactive and adaptive to user input. The model uses predefined factors for measuring the difficulty and a user defines the difficulty level by ordering these factors. We use lexicographical ordering to compare the difficulty of questions based on a user-defined ordering of factors and a concomitant algorithm for handling these factors. Further, we provide a feature called scenario guidance, which allows users to change the scenario at run time. We develop a software using the proposed model, which generates new questions according to a user-defined difficulty level. In order to evaluate the proposed framework, we conducted a pilot test of the software, in which teachers generate questions according to their chosen desired input including the difficulty level. The results show that the system is effective, helpful and robust. Overall, the framework shows promising benefits for teachers and organizations involved in setting questions for standardized tests.

Accepted for publication.


Designing in a University and Start-up Context: An Analysis of Engineering Change Propagation

Edward Koh, Roberto Duran-Novoa, Jörg Weigl, and Martin Henz

14th International Design Conference, Cavtat, Dubrovnik, Croatia, 2016.

This work aims to examine how engineering change propagation can be analysed efficiently in an entrepreneurial context. In particular, we studied how changes occurred, propagated, and influenced each other during an electrical motorcycle modification project, using a Function-Behaviour-Structure (FBS) framework within a Design Structure Matrix (DSM). The analysis shows that 61% of the modification requirements seek to address Functional issues. 21% of these changes propagated further, requiring changes in other components that were not initially planned for change. 85% of change propagation between components is direct (1-step) and the most frequent type of change dependency between components is Structural (67%). The findings suggest that a 1-step change propagation analysis is sufficient in detecting the majority of change propagation and can thus make a difference between project success and failure, especially for start-ups with limited resources.

Accepted for publication.


Snowstorm - Design and Construction of an Electric Recreational Flying Machine

Prerak Agarwal, Jean-Pierre Castillo, Martin Henz, Liu Shengmu, Shawn Sim, Sre Vinod, Wang Yuyao, Joerg Dieter Weigl, Xue Yushu, Xu Zan

Eleventh International Conference on Ecological Vehicles and Renewable Energies, EVER 2016. 6-8 April 2016, Grimaldi Forum, Monaco.

Powered recreational locomotion has recently experienced a massive wave of innovation, due to advances in battery and electric motor technology. Electric scooters, inline and coaxial two-wheelers and mono-wheels proliferate and contribute to the quality of life of millions. This project explores indoor flying as a recreational activity. Form the onset, indoor flying requires no or very low local emissions and low levels of noise, which strongly suggests electric propulsion. Considerations of safety and cost lead to a multicopter design. This abstract describes the design of Snowstorm, an experimental recreational flying machine developed at the National University of Singapore. Innovative features include a conducive propeller, seat and landing gear arrangement, triply-redundant power management, mechanical, electrical and electronic safety measures and a motor control architecture that re-uses proven multi-copter control software and hardware.

Available: PDF


A Framework for Automated Generation of Questions Based on First-Order Logic

Rahul Singhal, Shubham Goyal, and Martin Henz

Artificial Intelligence in Education, ed. Cristina Conati, Neil Heffernan, Antonija Mitrovic, M. Felisa Verdejo. Lecture Notes in Computer Science, vol. 9112: 776-780. Berlin, Heidelberg, New York: Springer, 2015

In this work, questions are tasks posed to students to help them understand a subject, or to help educators assess their level of competency in it. Automated question generation is important today as content providers in education try to scale their efforts. In particular, MOOCs need a continuous supply of new questions in order to offer educational content to thousands of students, and to provide a fair assessment process. In this paper we establish first-order logic as a suitable formal tool to describe question scenarios, questions and answers. We apply this approach to the domain of mechanics (physics) in high school education.

Available: PDF


Solar-Powered Sailing Yachts in the Tropics

Martin Henz, Jörg Weigl, Evan Lowell, and Eric Yee

Empowering Maritime Resources beyond Asia: Directions, Issues and Challenges, ed. Satiria Agust, Gatot Subroto, Risandi Dwirama Putra, Eko Prayetno, L.N. Firdaus (2015): 132-137. Tanjungpinang, Bintan: UMRAH Press. Keynote paper, First International Conference on Maritime Development, 4 - 6 Sep 2015, Aston Hotel, Tanjungpinang, Bintan, Indonesia

Sailing yachts require an additional propulsion source beside the sails for emergencies to be manoeuvrable in absence of wind or in tight conditions such as ports. Typically, small inboard or outboard combustion engines serve this purpose. In the tropics, solar energy is abundantly available throughout the year, and therefore solarpowered electric motors are attractive alternatives to combustion engines. We explore the dimensioning of solar panels for such a boat and conclude that for a fixed desired range under electric power and a fixed available charging time, the required solar panel surface grows roughly proportional to the cube of the length of the boat, whereas the available surface for solar panels grows proportional to its square. Even in the tropics, solar power therefore ceases to be feasible as exclusive auxiliary power from a certain length of the boat upwards.

To verify these conclusions, our team has converted one of the smallest available sailing yachts, a 7.7m long motorised sailing yacht to a carbon-neutral vessel by retrofitting it with a 2.0kW electric outboard motor and two 24V 200Ah marinised lithium-ion phosphate battery sets. Three 275 W mono-crystalline solar panels serve as cockpit roof and are mounted on a custom-built stainless steel truss. The battery lasts for 5 hours of continuous full throttle operations and can be fully charged by the solar panels in less than four days under typical light conditions in Singapore. The solar charging data can be monitored remotely by a newly developed web interface. The boat was converted in October 2014 and is currently the only carbon-neutral motorized sailing yacht in Singapore.

Available: PDF


Converting Motorised Sailing Yachts to Carbon-neutral Vessels

Martin Henz, Jörg Weigl, Evan Lowell, and Eric Yee

28th International Electric Vehicle Symposium and Exhibition 2015 EVS28, ed. Korean Society of Automotive Engineers (2015): 2438-2442. Red Hook, NY: Curran Associates. 3-6 May 2015, KINTEX, Goyang, South Korea

The conversion of motorised sailing yachts to carbon-neutral electric vehicles poses unique opportunities as well as challenges from business, design and engineering viewpoints. The reduced noise and smell that comes with electric propulsion attracts environmentally conscious sailors, who usually also have sufficient resources to finance such a conversion. The long lifetime of sailing yachts make conversion economically attractive, and keeping the sails as the main method of propulsion means that the demands on the electric drive are relatively modest.

Sufficiently dimensioned solar panels can solve the requirement of carbon-neutral propulsion, but their installation within the functional and aesthetic constraints of a sailing yacht poses considerable challenges. The harsh environment of the open sea requires ruggedised designs that can withstand the movement of the boat, high wind speeds and prolonged exposure to salt water. Another challenge is to provide reliable electricity supply for on-board appliances, which typically come at 12V DC and 240V AC.

Our team has converted a motorised sailing yacht to a carbon-neutral vessel by retrofitting it with a 2.5kW electric outboard motor and a 24V 200Ah marinised lithium-ion phosphate battery set. Three 275W mono-crystalline solar panels serve as cockpit roof and are mounted on a custombuilt stainless steel truss. The battery lasts for 2 1/2 hours of continuous operation. At daytime, the solar panels allow for docking manoeuvres even without any batteries. They can fully charge the battery set in less than two days under typical light conditions in Singapore. DC-DC converters, in combination with an auxiliary battery, supplies 12V DC for navigational equipment and 240V AC for household appliances. The auxiliary battery can also serve as an emergency power source for the motor.

The boat was converted in October 2014 and is currently the only carbon-neutral motorized sailing yacht in Singapore.

Available: PDF


Automated generation of region-based geometric questions

Rahul Singhal, Martin Henz, Kevin McGee

IEEE 26th International Conference on Tools with Artificial Intelligence, ICTAI 2014. 10-12 Nov 2014, Limassol, Cyprus, pages 838-845.

We extend our previously proposed framework that combines a combinatorial approach, pattern matching and automated deduction to generate geometry questions which, directly or indirectly, require finding the congruent regions formed by the intersection of geometric objects. The extension involves proposing a knowledge representation for regions and a rule-based algorithm for generation of region-based knowledge representation. In addition, several algorithms such as circle/arc projection to straight line(s) are proposed to avoid numerical reasoning for proving congruent regions, making the solution eligible for high school geometry domain. Furthermore, we propose the integration of this framework with our previously proposed framework to generate questions involving both implicit construction and congruent regions. The system is able to generate the solution(s) of the questions for their validation. Such a system would help teachers to quickly generate large numbers of questions based on several properties of geometric objects such as length, angle, area and perimeter. Students can explore, revise and master specific topics covered in classes and textbooks based on generated questions. This system may also help standardize tests such as Primary School Leaving Exam (PSLE), GMAT and SAT. Our methodology uses (i) a combinatorial approach for generating geometric figures (ii) Pattern matching and rule-based approach for region generation (iii) automated deduction for checking equality of properties of geometric objects (iv) linear equation solver to generate new questions and solutions. By combining these methods, we are able to generate questions involving finding or proving congruence relationships between the regions generated by the geometric objects based on a various specifications such as objects and concepts. Experimental results show that a large number of questions can be generated in a short time. A survey shows that the generated questions and the solutions are useful and fulfills the high school criteria.

Available: PDF


Automated generation of geometry questions for high school mathematics

Rahul Singhal, Martin Henz, and Kevin McGee

Proceedings of the 6th International Conference on Computer Supported Education CSEDU 2014, ed. Susan Zvacek, James Uhomoibhi. INSTICC: SciTePress. 23-25 May 2014, Barcelona, Spain, pages 14-25.

We describe a framework that combines a combinatorial approach, pattern matching and automated deduction to generate and solve geometry problems for high school mathematics. Such a system would help teachers to quickly generate large numbers of questions on a geometry topic. Students can explore and revise specific topics covered in classes and textbooks based on generated questions. The system can act as a personalized instructor - it can generate problems that meet users specific weaknesses. This system may also help standardize tests such as GMAT and SAT. Our novel methodology uses (i) a combinatorial approach for generating geometric figures (ii) a pattern matching approach for generating questions and (iii) automated deduction to generate new questions and solutions. By combining these methods, we are able to generate questions involving finding or proving relationships between geometric objects based on a specification of the geometry objects, concepts and theorems to be covered by the questions. Experimental results show that a large number of questions can be generated in a short time. We have tested our generated questions on an existing geometry question solving software JGEX, verifying the validity of the generated questions.

Available: PDF


Automated Generation of High School Geometric Questions Involving Implicit Construction

Rahul Singhal, Martin Henz, and Kevin McGee

Proceedings of the 6th International Conference on Computer Supported Education CSEDU 2014, ed. Susan Zvacek, James Uhomoibhi. INSTICC: SciTePress. 23-25 May 2014, Barcelona, Spain, pages 467-472.

We describe a framework that combines a combinatorial approach and automated deduction to generate geometry problems which require implicit constructions for their solution. This is an extension of our framework developed for generating geometric questions without construction. Such a system would help teachers to quickly generate large numbers of questions involving implicit construction on a geometry topic. Students can explore, revise and master specific topics covered in classes and textbooks based on construction-based generated questions. This system may also help standardize tests such as GMAT and SAT. Our novel methodology uses (i) a combinatorial approach for generating geometric figures and objects for construction (ii) automated deduction to generate new questions and solutions. By combining these methods, we are able to generate questions involving finding or proving relationships between geometric objects based on a specification of the geometry objects, concepts, theorems and construction object to be covered by the questions. Experimental results show that a large number of questions can be generated in a short time.

Available: PDF


Geometry Question Generator: Question and Solution Generation, Validation and User Evaluation

Rahul Singhal and Martin Henz

Susan Zvacek, Maria Teresa Restivo, James Onohuome Uhomoibhi, Markus Helfert: Computer Supported Education - 6th International Conference, CSEDU 2014 Barcelona, Spain, April 1-3, 2014, Revised Selected Papers. Communications in Computer and Information Science 510, Springer 2015, ISBN 978-3-319-25767-9, pages 196-210.

Current massively open online courses (MOOCs) are providing several technical challenges for educators. One of these challenges is automated generation of questions, along with the solutions, in order to deal with a large number of students. Geometry is an important part of the high school curriculum. Hence, in this paper, we have focused on the high school geometry domain. We have proposed a framework that combines a combinatorial approach, pattern matching and automated deduction to generate and solve geometry problems for high school mathematics. The system would help teachers to quickly generate large numbers of questions on a geometry topic and may also support the setting of standardized tests such as PSLE, GMAT and SAT.

Our novel methodology uses (i) a combinatorial approach for generating geometric figures from the user input, (ii) a pattern matching approach for generating questions, and (iii) automated deduction to generate new questions and solutions. By combining these methods, we are able to generate questions involving finding or proving relationships between geometric objects based on a specification of the geometry objects, concepts and theorems to be covered by the questions. We propose several algorithms to avoid generation of repeated questions and to avoid questions having redundant information, which increases the effectiveness of our system. We have tested our generated questions on an existing geometry question solving software JGEX, verifying the validity of the generated questions. A survey with the real users such as high school teachers and students on generated questions and solutions shows that our system is effective and useful.

Available: PDF


Environmental Impact of Converted Electrical Motorcycle

Yang-Xuan Pek, Martin Henz, and Jörg Weigl

Proceedings of the 27th International Electric Vehicle Symposium, EVS27, ed. Joeri van Mierlo. 17-20 Nov 2013, Barcelona, Spain, 2013.

This study explores the environmental impact of the conversion of an internal combustion engine (ICE) sports motorcycle into a converted battery-powered electric vehicle (CBEV). Zero tailpipe emissions might lead to the assumption that such an ICE-to-BEV conversion will always yield net positive environmental benefits in life cycle greenhouse gas (GHG) emissions and energy reductions, but energy inputs and materials impacts associated with the conversion of a CBEV are weighed against savings during postconversion usage. It was found that conversion would reduce the life cycle energy consumed and emissions produced of a typical motorcycle by 72% and 45% respectively. These findings have important considerations for the current global transportation landscape.

Available: PDF


To produce or convert: A case for large scale electric motorcycle conversion in Singapore

Brian Teo, Aloysius Seah, Shreyas Rao, Martin Henz, and Jörg Weigl

Proceedings of the 27th International Electric Vehicle Symposium, EVS27, ed. Joeri van Mierlo. 17-20 Nov 2013, Barcelona, Spain.

This paper explores the economic viability of the electrical conversion of motorcycles in Singapore. The vehicle market is regulated through Certificate of Entitlement (COE) and road tax. These mechanisms do not cover converted electric motorcycles yet. Large-scale conversion allows for the production of 2500 motorcycles per year with an estimated workforce of 20 people. Electric motorcycles are cheaper to run compared to ICE motorcycles and these cost savings can recoup the price of the motorcycle in a short period. A policy innovation in this area could further spur large scale electric motorcycle conversion and make it a viable business.

Available: PDF


Introducing Logic and Formal Methods with Coq

Martin Henz and Aquinas Hobor

First International Conference on Certified Programs and Proofs, CPP 2011. Heidelberg: Springer LNCS 7086, 7-9 Dec 2011, Howard Beach Hotel, Kenting, Taiwan.

During the past three years we have been integrating mechanized theorem proving into a traditional introductory course on formal methods. We explain our goals for adding mechanized provers to the course, and illustrate how we have integrated the provers into our syllabus to meet those goals.We also document some of the teaching materials we have developed for the course to date, and what our experiences have been like.

Available: PDF


SudokuSat-A Tool for Analyzing Difficult Sudoku Puzzles

Martin Henz and Hoang-Minh Truong

In Constantinos Koutsojannis and Spiros Sirmakessis, editors, Tools and Applications with Artificial Intelligence, volume 166 of Studies in Computational Intelligence. Springer-Verlag, Berlin, 2009.

Sudoku puzzles enjoy world-wide popularity, and a large community of puzzlers is hoping for ever more difficult puzzles. A crucial step for generating difficult Sudoku puzzles is the fast assessment of the difficulty of a puzzle. In a study in 2006, it has been shown that SAT solving provides a way to efficiently differentiate between Sudoku puzzles according to their difficulty, by analyzing which resolution technique solves a given puzzle. This paper shows that one of these techniques---unit resolution with failed literal propagation---does not solve a recently published Sudoku puzzle called AI Escargot, claimed to be the world's most difficult. The technique is also unable to solve any of a list of difficult puzzles published after AI Escargot, whereas it solves all previously studied Sudoku puzzles. We show that the technique can serve as an efficient and reliable computational method for distinguishing the most difficult Sudoku puzzles. As a proof-of-concept for an efficient difficulty checker, we present the tool SudokuSat that categorizes Sudoku puzzles with respect to the resolution technique required for solving them.

Available: PDF BibTeX Entry.


QuikFix—A Repair-based Timetable Solver

Michael Clark, Martin Henz, and Bruce Love

Proceedings of the Seventh International Conference on the Practice and Theory of Automated Timetabling, PATAT 2008, August 19-22 2008, Montreal, Canada.

QuikFix is a software program for solving timetabling problems. The software adapts repair-based heuristic search known in SAT solving to the timetabling domain. A high-level timetabling-specific model enforces structural constraints and allows for meaningful moves in the search space, such as swaps of the time slots or venues of events. QuikFix uses known techniques to improve the search performance, such as multi-starts, tabu lists, and strategic oscillation. The software is easily extensible through the use of object-oriented programming techniques and has been employed for the timetabling of a Singapore K-12 international school, and as an entry to the ITC 2007 timetabling competition.

Available: PDF BibTeX Entry.


M2ICAL: A Tool for Analyzing Imperfect Comparison Algorithms

Wee-Chong Oon and Martin Henz

Proceedings of the Nineteenth IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2007, October 29-31 2007, Patras, Greece.

Practical optimization problems often have objective functions that cannot be easily calculated. As a result, comparison-based algorithms that solve such problems use comparison functions that are imperfect (i.e. they may make errors). Machine learning algorithms that search for game-playing programs are typically imperfect comparison algorithms. This paper presents M2ICAL, an algorithm analysis tool that uses Monte Carlo simulations to derive a Markov Chain model for Imperfect Comparison ALgorithms. Once an algorithm designer has modeled an algorithm using M2ICAL as a Markov chain, it can be analyzed using existing Markov chain theory. Information that can be extracted from the Markov chain include the estimated solution quality after a given number of iterations; the standard deviation of the solutions' quality; and the time to convergence.

Available: PDF BibTeX Entry.


M2ICAL analyzes HC-Gammon

Wee-Chong Oon and Martin Henz

Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, AAAI 2007, July 22-26 2007, Vancouver, British Columbia.

We analyse Pollack and Blair's HC-Gammon backgammon program using a new technique that performs Monte Carlo simulations to derive a Markov Chain model for Imperfect Comparison ALgorithms, called the M2ICAL method, which models the behavior of the algorithm using a Markov chain, each of whose states represents a class of players of similar strength. The Markov chain transition matrix is populated using Monte Carlo simulations. Once generated, the matrix allows fairly accurate predictions of the expected solution quality, standard deviation and time to convergence of the algorithm. This allows us to make some observations on the validity of Pollack and Blair's conclusions, and also shows the application of the M2ICAL method on a previously published work.

Available: PDF BibTeX Entry.


Towards a Framework for Observing Artificial Life Forms

Martin Henz and Janardan Misra

Proceedings of the First IEEE Symposium on Artificial Life, IEEE-ALife 2007, April 1-5 2007, Honolulu, Hawaii.

Evolutionary processes have emerged as the defining feature of "life" in Artificial Life (Alife). When studying the behavior of a particular Alife form, the question naturally arises, whether a particular run of an Alife experiment exhibits evolutionary behavior or not. This paper presents the Observer Framework, a formal framework for answering this question, based upon the notion of observations made in the Alife model at hand. Starting with defining entities and their relationships observed during the runs, the framework prescribes a series of definitions (decisions) that the observer of the Alife form needs to make, followed by axioms (conditions) that must be met in order to establish evolutionary behavior in particular runs. We use the example of Cellular Automata based Langton Loops to illustrate the Observer Framework, and suggest directions for further Alife research, based upon the framework design and the case study analysis.

Available: PDF BibTeX Entry.


Playing with Constraint Programming and Large Neighborhood Search

Martin Henz

Proceedings of the Fifth International Conference on the Practice and Theory of Automated Timetabling, PATAT 2004, August 18-20 2004.

Constraint programming can be used to solve small tournament scheduling problems to optimality. Beyonds its low size limits, local search techniques have been shown to yield close-to-optimal schedules, when augmented with simulated annealing, reheating, strategic oscillation and other techniques. In these approaches, the local moves are relatively small, making the moves fast, but requiring sophisticated mechanisms to escape local minima. This paper explores the possibility of making use of constraint programming as a technique for achieving large moves in local search. The proposed technique falls within the algorithm scheme known as very large scale neighborhood search.

Available: PDF BibTeX Entry.


Global Constraints for Round Robin Tournament Scheduling

Martin Henz, Tobias Müller, Sven Thiel

European Journal of Operational Research (EJORS), 153(1), pp 92-101, February 2004.

In the presence of side-constraints and optimization criteria, round robin tournament problems are hard combinatorial problems, commonly tackled with tree search and branch-and-bound optimization. Recent results indicate that constraint-based tree search has crucial advantages over integer programming-based tree search for this problem domain by exploiting global constraint propagation algorithms during search. In this paper, we analyze arc-consistent propagation algorithms for the global constraints "all-different" and "one-factor" in the domain of round robin tournaments. The best propagation algorithms allow us to compute all feasible perfectly mirrored pattern sets with minimal breaks for intermural tournaments of realistic size, and to improve known lower bounds for intramural tournaments balanced with respect to carry-over effects.

Available: PDF (revised submitted version), online version from publisher, BibTeX Entry.


Solving Hierarchical Constraints over Finite Domains

Martin Henz, Yun Fong Lim, Seet Chong Lua, Xiao Ping Shi, J. Paul Walser, and Roland H. C. Yap

Annals of Mathematics and Artificial Intelligence (AMAI), 40(3), pp 283-302, March 2004.

Many real world problems have requirements and constraints which conflict with each other. One approach for dealing with such over-constrained problems is with constraint hierarchies. In the constraint hierarchy framework, constraints are classified into ranks, and appropriate solutions are selected using a comparator which takes into account the constraints and their ranks. In this paper, we present a local search solution to solving hierachical constraint problems over finite domains (HCPs). This is an extension of local search for over-constrained integer programs WSAT(OIP) to constraint hierarchies and general finite domain constraints.

The motivation for this work arose from solving large airport gate allocation problems. We show how gate allocation problems can be formulated as HCPs using typical gate allocation constraints. Using the gate allocation benchmarks, we investigate how constraints hierarchy selection strategies and the problem formulation using two models: a 0-1 linear constraint hierarchy model and a nonlinear finite domain constraint hierarchy model.

Available: BibTeX Entry.


Hardware Implementations of Real-time Reconfigurable WSAT Variants

Roland Yap, Stella Wang, and Martin Henz

Proceedings of the International Conference on Field Programmable Logic and Applications, 2003, Lisbon, Portugal, LNCS 2778.

Local search methods such as WSAT have proven to be successful for solving SAT problems. In this paper, we propose two host-FPGA (Field Programmable Gate Array) co-implementations, which use modified WSAT algorithms to solve SAT problems. Our implementations are reconfigurable in real-time for different problem instances. On an XCV1000 FPGA chip, SAT problems up to 100 variables and 220 clauses can be solved. The first implementation is based on a random strategy and achieves one flip per clock cycle through the use of pipelining. The second uses a greedy heuristic at the expense of FPGA space consumption, which precludes pipelining. Both of the two implementations avoid re-synthesis, placement, routing for different SAT problems, and show improved performance over previously published reconfigurable SAT implementations on FPGAs.

Available: PDF, BibTeX Entry.


Logic programming in the context of multiparadigm programming: the Oz experience

Peter Van Roy, Per Brand, Denys Duchier, Seif Haridi, Martin Henz, Christian Schulte

Journal of Theory and Practice of Logic Programming (TPLP), 3(6), pp 715-763, November 2003.

Oz is a multiparadigm language that supports logic programming as one of its major paradigms. A multiparadigm language is designed to support different programming paradigms (logic, functional, constraint, object-oriented, sequential, concurrent, etc.) with equal ease. This article has two goals: to give a tutorial of logic programming in Oz and to show how logic programming fits naturally into the wider context of multiparadigm programming. Our experience shows that there are two classes of problems, which we call algorithmic and search problems, for which logic programming can help give practical solutions. Algorithmic problems have known efficient algorithms. Search problems do not have known efficient algorithms but can be solved with search. The Oz support for logic programming targets these two classes specifically, using the concepts needed for each. This is in contrast to the Prolog approach, which targets both classes with one set of concepts, which results in less than optimal support for both problem classes. We give examples that can be run interactively on the Mozart system, which implements Oz. To explain the essential difference between algorithmic and search programs, we define the Oz execution model. This model subsumes both concurrent logic programming (committed-choice-style) and search-based logic programming (Prolog-style). Furthermore, as consequences of its multiparadigm nature, the model supports new abilities such as first-class top levels, deep guards, active objects, and sophisticated control of the search process. Instead of Horn clause syntax, Oz has a simple, fully compositional, higher-order syntax that accommodates the abilities of the language. We give a brief history of Oz that traces the development of its main ideas and we summarize the lessons learned from this work. Finally, we give many entry points into the Oz literature.

Available: PDF (revised version), BibTeX Entry.


Real-time Reconfigurable Hardware WSAT Variants

Roland Yap, Stella Wang, and Martin Henz

Proceedings of the International Conference on Theory and Applications of Satisfiability (SAT), 2003, LNCS, poster (to appear).

Local search methods such as WSAT have proven to be successful for solving SAT problems. In this paper, we propose two real-time host-FPGA (Field Programmable Gate Array) co-implementations, which use modified WSAT algorithms to solve SAT problems. Our implementations are reconfigurable in real-time for different problem instances. On an XCV1000 FPGA chip, SAT problems up to 100 variables and 220 clauses can be solved. The first implementation is based on a random strategy and achieves one flip per clock cycle through the use of pipelining. The second uses a greedy heuristic at the expense of FPGA space consumption, which precludes pipelining. Both of the two implementations avoid re-synthesis, placement, routing for different SAT problems, and show improved performance over previously published reconfigurable SAT implementations on FPGAs.

Available: PDF, BibTeX Entry


A Software Engineering Approach to Constraint Programming Systems

Chiu Wo Choi, Martin Henz, Ka Boon Ng

Proceedings of the Asian-Pacific Conference on Software Engineering, APSEC 2002, Gold Coast, Australia, Dec 2002.

Constraint programming (CP) systems are useful for solving real-life combinatorial problems, such as scheduling, planning, rostering and routing problems. The design of modern CP systems has evolved from a monolithic to an open design in order to meet the increasing demand for application specific customization. It is widely accepted that a CP system needs to balance various design factors such as efficiency versus customizability and flexibility versus maintenance. This paper captures our experience with a software engineering approach to the development of constraint programming systems. This allows us to systematically investigate the different factors that affect the performance of a CP system. In particular, we study the application of reuse techniques, such as toolkits, framework and patterns, to the design and implementation of a finite-domain CP system.

Available: PDF, BibTeX Entry


Implementing CSAT Local Search on FPGAs

Martin Henz, Edgar Tan, and Roland Yap.

Proceedings of the International Conference on Field Programmable Logic and Applications, 2002, Montpellier, France, LNCS 2438, short paper, pp 1156-1159.

Stochastic local search methods such as GSAT, WalkSAT and their variants have been used successfully at solving propositional satisfiability problems (SAT). The key operation in these local search algorithms is the speed of variable flipping. We present a parallel FPGA designs for CSAT capable of one flip per clock cycle which is achieved by exploiting maximal parallelism and multi-try pipelining. Experimental results show that a speedup of two orders of magnitude over software implementations can be achieved.

Available: PDF, BibTeX Entry


GNOPL - An Implementation of OPL Search in Oz

Martin Henz, Tan Woon Kiong

Proceedings of the workshop Techniques foR Implementing Constraint programming Systems, TRICS 2002, Ithaca, USA, Sept 2002.

Available: PDF, BibTeX Entry


Components for State Restoration in Tree Search

Chiu Wo Choi, Martin Henz, Ka Boon Ng

Proceedings of the Seventh International Conference on Principles and Practice of Constraint Programming, CP2001, Cyprus, Nov/Dec 2001.

Constraint programming systems provide software architectures for the fruitful interaction of algorithms for constraint propagation, branching and exploration of search trees. Search requires the ability to restore the state of a constraint store. Today's systems use different state restoration policies. Upward restoration undoes changes using a trail, and downward restoration (recomputation) reinstalls information along a downward path in the search tree. In this paper, we present an architecture that isolates the state restoration policy as an orthogonal software component. Applications of the architecture include three novel state restoration policies, called lazy copying, coarse-grained trailing, and batch recomputation, a detailed comparison of these and existing restoration policies with ``everything else being equal'', and a novel class of engines that uses different restoration policies in different parts of the search tree. The architecture allows the user to optimize time and space consumption of applications by choosing existing or designing new state restoration policies in response to application-specific characteristics.

Available: PDF, BibTeX Entry


A Compositional Framework for Search

Chiu Wo Choi, Martin Henz, Ka Boon Ng

Proceedings of the Colloquium on Implementation of Constraint and Logic Programming Systems, CICLOPS 2001, Paphos, Cyprus, Dec 2001.

Recent developments in constraint programming systems show an increasing emphasis on providing abstractions for configuring search. Existing frameworks for tree search offer customized exploration, branching and state restoration policies. We argue, however, that most of these frameworks do not provide adequate abstractions for more complex search scenarios, where different search techniques are used in different phases of the search, where parts of search trees are systematically discarded, or where tree search is embedded in a context of local optimization. In this paper, we propose to describe complex search scenarios using a compositional framework, realized in the Figaro library, with an abstraction called engine. We demonstrate its expressivity by re-formulating two complex search scenarios from the literature.

Available: PDF, BibTeX Entry


One Flip per Clock Cycle

Martin Henz, Edgar Tan, Roland Yap

Proceedings of the Seventh International Conference on Principles and Practice of Constraint Programming, CP2001, Cyprus, Nov/Dec 2001.

Local search methods such as GSAT have proven to be successful for finding solving propositional satisfiability problems (SAT). In this paper, we show how GSAT can be implemented to be as fast as possible in hardware. Our implementation using field programmable gate arrays (FPGAs) achieves one flip per clock cycle by exploiting maximal parallelism and at the same time avoiding excessive hardware cost in terms of gates. Experimental evaluation of our prototype implementation shows a speedup of two orders of magnitude over optimized software implementations and one order of magnitude over existing hardware schemes. As far as we are aware, this is the fastest known implementation of GSAT. We also introduce in this paper a high level algorithmic notation which is convenient for describing the implementation of such algorithms in hardware as well as their analysis.

Available: PDF, BibTeX Entry


Scheduling a Major College Basketball Conference---Revisited

Martin Henz

Operations Research, 49(1), Jan/Feb 2001.

Nemhauser and Trick presented the problem of finding a timetable for the 1997/98 Atlantic Coast Conference (ACC) in basketball. Their solution, found with a combination of integer programming and exhaustive enumeration, was accepted by the ACC.

Finite-domain constraint programming is another programming technique that can be used for solving combinatorial search problems such as sports tournament scheduling. This paper presents a solution of round robin tournament planning based on finite-domain constraint programming. The approach yields a dramatic performance improvement, which makes an integrated interactive software solution feasible.

Note that in the journal version there is an error in the first (almost trivial) scheduling phase. Two pattern constraints were omitted, which leads to 46 patterns instead of the 38 patterns in the paper. The PostScript version available here fixes this problem. See Constraint 2 on page 5 and Constraint 3 in Table 1 on page 7. Thanks to Zhou Jingtao and Hantao Zhang for pointing out the error.

Available: PDF, BibTeX Entry


An Overview of Finite Domain Constraint Programming

Martin Henz, Tobias Müller

Proceedings of the Fifth Conference of the Association of Asia-Pacific Operational Research Societies, APORS 2000.

In recent years, the repertoire of available techniques for solving combinatorial problems has seen a significant addition: constraint programming. Constraint programming is best seen as a framework for combining software components to achieve problem-specific solvers. The strength of constraint programming depends on the synergy that can be achieved between these components. In this tutorial introduction, we give an overview of constraint programming for solving combinatorial problems.

Available: PDF, BibTeX Entry


GIFT: A Generic Interface for reusing Filtering Algorithms

Ka Boon Ng, Chui Wo Choi, Martin Henz, Tobias Müller

Proceedings of the TRICS Workshop "Techniques foR Implementing Constraint programming Systems", CP 2000.

Many different constraint programming (CP) systems exist today. For each CP system, there are many different filtering algorithms. Researchers and developers usually choose a CP system of their choice to implement their filtering algorithms. To use these filtering algorithms on another system, we have to port the code over. This situation is clearly not desirable. In this paper, we propose a generic C++ interface for writing filtering algorithms called GIFT (Generic Interface for FilTers). By providing the generic interface on different CP systems, we can reuse any filtering algorithms easily. A case study on reusing scheduling filtering algorithms between Mozart and Figaro further highlights the feasibility of this approach.

Available: PDF, BibTeX Entry


Solving Hierarchical Constraints over Finite Domains

Martin Henz, Yun Fong Lim, Seet Chong Lua, Xiao Ping Shi, J. Paul Walser, Roland H. C. Yap

Sixth International Symposium on Artificial Intelligence and Mathematics, January 5-7, 2000, Fort Lauderdale, Florida.

Many real world problems have requirements and constraints which conflict with each other and are not well defined. One framework for dealing with such over-constrained/fuzzy problems is provided by constraint hierarchies, where constraints are divided into ranks, and where a comparator selects preferred solutions over others. In this paper, we present a framework for formulating hierarchical constraint problems over finite domains (HCPs). We show, how the recent framework of over-constrained integer programs (OIPs) can be extended to handle non-linear constraints and to exploit constraint hierarchies.

The motivation for this work arose from solving large airport gate allocation problems. We show how gate allocation problems can be formulated as HCPs using typical gate allocation constraints. Using gate allocation benchmarks with varying problem characteristics, we compare local search on the given HCPs with local search and integer programming on linear reformulations of the HCPs.

Available: PDF, BibTeX Entry


Friar Tuck - A Constraint-Based Tournament-Scheduling Tool

Martin Henz

IEEE Intelligent Systems, 15(1):5-7, 2000.

This is a note on the system Friar Tuck, which appeared in the department Intelligencer of IEEE Intelligent Systems. This issue of IEEE Intelligent Systems has the focus "Constraints".

Available: PDF (from IEEE), BibTeX Entry


A Toolkit for Constraint-based Inference Engines

Tee Yong Chew, Martin Henz, Ka Boon Ng

Practical Aspects of Declarative Languages, Second International Workshop, PADL'00, LNCS 1753.

Solutions to combinatorial search problems can benefit from custom-made constraint-based inference engines that go beyond depth-first search. Several constraint programming systems support the programming of such inference engines through programming abstractions. For example, the Mozart system for Oz comes with several engines, extended in dimensions such as interaction, visualization, and optimization. However, so far such extensions are monolithic in their software design, not catering for systematic reuse of components.

We present an object-oriented modular architecture for building inference engines that achieves high reusability and supports rapid prototyping of search algorithms and their extensions. For the sake of clarity, we present the architecture in the setting of a C++ constraint programming library. The SearchToolKit, a search library for Oz based on the presented architecture, provides evidence for the practicality of the design.

Available: PDF, BibTeX Entry


Constraint-based Round Robin Tournament Planning

Martin Henz

Proceedings of the 1999 International Conference on Logic Programming, Las Cruces, NM.

Sport tournament planning becomes a complex task in the presence of heterogeneous requirements from teams, media, fans and other parties. Existing approaches to sport tournament planning often rely on precomputed tournament schemes which may be too rigid to cater for these requirements. Existing work on sport tournaments suggests a separation of the planning process into three phases. In this work, it is shown that all three phases can be solved using finite-domain constraint programming. The design of Friar Tuck, a generic constraint-based round robin planning tool, is outlined. New numerical results on round robin tournaments obtained with Friar Tuck underline the potential of constraints over finite domains in this area.

Available: PDF, BibTeX Entry


Figaro: Yet Another Constraint Programming Library

Martin Henz, Tobias Müller and Ng Ka Boon

Workshop on Parallelism and Implementation Technology for Constraint Logic Programming, 1999.

Existing libraries and languages for finite domain constraint programming usually have depth-first search (with branch and bound) built-in as the only search algorithm. Exceptions are the languages CLAIRE and Oz, which support the programming of different search algorithms through special purpose programming language constructs. The goal of this work is to make abstractions for programming search algorithms available in a language-independent setting.

Figaro is an experimentation platform being designed to study non-standard search algorithms, different memory policies for search (trailing vs copying), consistency algorithms, failure handling and support for modeling. This paper focuses on the use and implementation of such abstractions for investigating programmable search algorithms and memory policies in a C++ constraint programming library.

Available: PDF, BibTeX Entry


Objects for Concurrent Constraint Programming

Martin Henz

Monograph, Kluwer Academic Publishers, October 1997.

Object-oriented programming had a tremendous impact on the world of software in the last 15 years. Numerous approaches have been proposed to support this successful programming paradigm in other programming language families such as logic and functional programming. Concurrent constraint programming (ccp) is a recent development in programming language design. Its central contribution is the notion of partial information provided by a shared constraint store. The constraint store serves as communication medium between concurrent threads of control and as vehicle for their synchronization.

In this work, we analyse the possibilities to support object-oriented programming in ccp. Starting from known approaches, we cover various object models and discuss their properties. As model language for the analysis, we use the language Small Oz, a sublanguage of the ccp language Oz. We present a general-purpose object system for Small Oz, describe its implementation and its expressivity for concurrent computation.

The book is written for programming language researchers with interest in programming language aspects of concurrency, object-oriented programming or constraint programming. Programming language implementors will benefit from the rigorous treatment of the efficient implementation of Small Oz. Oz programmers get a first-hand view of the design decisions that lie behind the Oz object system.

From the perspective of ccp, this work intoduces the notion of passive objects - the central notion of object-oriented programming - to the ccp framework. It builds a bridge from essential ideas of ccp to main-stream programming languages. From the perspective of object-oriented and functional languages, a central contribution is that partial information as provided by logic variables can be integrated in the framework of both of these paradigms in a straightforward manner. From this intergration, concurrent objects benefit through simple and elegant synchronization techniques.

The language Oz was designed in the Programming Systems Lab, Saarbrücken, Germany, as an attempt to integrate essential aspects of the paradigms of constraint (logic), object-oriented and functional programming. This book gives account of this integration from the perspective of (concurrent) object-oriented programming. It is based on the author's doctoral thesis ``Objects in Oz,'' accepted by the Universität des Saarlandes in June 1997.

Available: Information provided by the publisher BibTeX Entry


Objects in Oz

Martin Henz

doctoral dissertation, accepted by the Universität des Saarlandes, Saarbrücken, Germany, in June 1997.

The programming language Oz integrates the paradigms of imperative, functional and concurrent constraint programming in a computational framework of unprecedented breadth, featuring stateful programming through cells, lexically scoped higher-order programming, and explicit concurrency synchronized by logic variables.

Object-oriented programming is another paradigm that provides a set of concepts useful in software practice. In this thesis we address the question how object-oriented programming can be suitably supported in Oz. As a lexically scoped higher-order language, Oz can express a wide range of object-oriented concepts. We present a simple yet expressive object system, demonstrate its usability and outline an efficient implementation. A central aspect of Oz is its support for concurrent computation. We examine the impact of concurrency on the design of an object system and explore the use of objects in concurrent programming.

Available: PDF BibTeX Entry


Constraint-based Time Tabling - A Case Study

Martin Henz, Jörg Würtz

Applied Artificial Intelligence, 10:439-453, 1996

In this paper, we concentrate on a typical scheduling problem: the computation of a time table for a German college. Like many other scheduling problems, this problem contains a variety of complex constraints and necessitates special-purpose search strategies. Techniques from Operations Research and traditional constraint logic programming are not able to express these constraints and search strategies on a sufficiently high level of abstraction. We show that the higher-order concurrent constraint language Oz provides this high-level expressivity, and can serve as a useful programming tool for college time tabling.

Available: BibTeX Entry


COMPOzE - Intention-based Music Composition through Constraint Programming

Martin Henz, Stefan Lauer, and Detlev Zimmermann

Proceedings of the 8th IEEE International Conference on Tools with Artificial Intelligence, November 16-19 1996, Toulouse, France.

The goal of this work is to generate four-voice compositions from given musical plans, which describe the desired intentions of the compositions. We developed the experimentation platform COMPOzE for intention-based composition. COMPOzE is based on concurrent constraint programming (ccp) on finite domains of integers. We argue that ccp provides a suitable technology for this task and that the constraint programming libraries and tools available for the ccp language Oz effectively support the implementation of COMPOzE.

This work links the research areas of of automatic music composition on one hand and finite domain constraint programming on the other, and contributes the tool COMPOzE, which practically demonstrates the potential of ccp to open up new areas of application for automatic music composition.

Available: PDF BibTeX Entry


Don't Be Puzzled!

Martin Henz

Workshop on Constraint Programming Applications, August 19, 1996, in conjunction with the Second International Conference on Principles and Practice of Constraint Programming (CP96), Cambridge, Massachusetts, USA

This paper is about how to solve a class of puzzles, called self-referential quizzes (srq), with constraint programming. An srq is a sequence of multiple choice questions that are about the puzzle itself. srqs are an attractive pastime, when they provide the possibility of drawing non-trivial conclusions on the way to the solution.

We introduce a typical srq, and represent it as a propositional satisfiability problem. Its straightforward clausal representation is too big for effective treatment using standard methods. Instead, we solve it with finite domain constraint programming. For this application of constraint programming, support of logic connectives such as conjunction and disjunction is crucial. With their small problem descriptions, \srq s are ideal candidates for benchmarks covering the implementation of 0/1 variables in constraint programming languages.

Available: PDF BibTeX Entry


Using Oz for College Time Tabling

Martin Henz, Jörg Würtz

The Practice and Theory of Automated Time Tabling: The Selected Proceedings of the 1st International Conference on the Practice and Theory of Automated Timetabling, Edinburgh 1995, LNCS 1153

In this paper, we concentrate on a typical scheduling problem: the computation of a time table for a German college. Like many other scheduling problems, this problem contains a variety of complex constraints and necessitates special-purpose search strategies. Techniques from Operations Research and traditional constraint logic programming are not able to express these constraints and search strategies on a sufficiently high level of abstraction. We show that the higher-order concurrent constraint language Oz provides this high-level expressivity, and can serve as a useful programming tool for college time tabling.

Available: PDF BibTeX Entry


Object-Oriented Concurrent Constraint Programming in Oz

Martin Henz, Gert Smolka, Jörg Würtz

Chapter 2 of: P. van Hentenryck and V. Saraswat (eds.), Principles and Practice of Constraint Programming, The MIT Press, pages 29-48, 1995.

Oz is a higher-order concurrent constraint programming system under development at DFKI. It combines ideas from logic and concurrent programming in a simple yet expressive language. From logic programming Oz inherits logic variables and logic data structures, which provide for a programming style where partial information about the values of variables is imposed concurrently and incrementally. A novel feature of Oz is the support of higher-order programming without sacrificing that denotation and equality of variables are captured by first-order logic. Another new feature of Oz are cells, a concurrent construct providing a minimal form of state fully compatible with logic data structures. These two features allow to express objects as procedures with state, avoiding the problems of stream communication, the conventional communication mechanism employed in concurrent logic programming.

Based on cells and higher-order programming, Oz readily supports concurrent object-oriented programming including object identity, late method binding, multiple inheritance, ``self'', ``super'', batches, synchronous and asynchronous communication.

Available: PDF BibTeX Entry


Glinda: A Meta-circular Interpreter for Oz

Martin Henz, Michael Mehl

Proceedings of the International Workshop on Oz Programming, November/December 1995.

Executing computer programs means interpreting the instructions coded in a programming language. Most implementations of high-level languages, such as DFKI Oz, use an intermediate step of compilation: The source code is compiled to a machine code which is then interpreted by the hardware or a more abstract machine. We show the advantages and problems that occur when one tries to directly interprete Oz source code. We present an implementation of a meta-circular Oz interpreter, i.e. an interpreter for Oz written in Oz and demonstrate its application to source-level profiling, execution visualization and language design.

Available: PDF BibTeX Entry


Munchkins: A Shell for Distributed Multi-User Games

Martin Henz, Martin Müller, Markus Wolf

Proceedings of the International Workshop on Oz Programming, November/December 1995.

Multi-user dungeons (MUDs) are text-based computer games being played over the Internet. They are usually based on a simple client-server architecture, allowing for their wide availability, but also imposing serious limitations upon their users. In this paper, we propose an implementation of a MUD as a truly distributed application using the concurrent object-oriented programming language Oz to overcome these limitations.

Available: PDF BibTeX Entry


Objects in Higher-order Concurrent Constraint Programming with State

Martin Henz, Gert Smolka

Proceedings of the Workshop on Coordination Models and Languages for Parallelism and Distribution (in connection with ECOOP 94), Bologna, Italy, July 1994.

Concurrent constraint programming (ccp) languages allow to express concurrency on a clean semantic base. Since objects are an attractive abstraction for describing concurrent activity, the goal of several ccp languages has been to provide object-oriented programming (oop). The traditional way to express the notion of objects in ccp languages is by describing an object as the consumer of a communication medium, e.g. a message stream, bag, channel, or port.

We propose a new model for objects in higher-order ccp languages like Oz: Objects are (dynamically created) procedures that take messages as arguments. While in previous proposals for objects in Oz a communication medium was still involved, we show in this paper that the right notion of concurrent state suffices to express oop in ccp. In contrast to the traditional approach, where communication, synchronization and buffering messages are all provided by the communication medium, the new model expresses them by orthogonal language constructs, allowing for a cleaner and more flexible conceptual base for objects, and a more efficient implementation in the case of light-weight objects.

Available: PDF BibTeX Entry


Oz - A Programming Language for Multi-Agent Systems

Martin Henz, Gert Smolka, Jörg Würtz

Proceedings of the 13th International Joint Conference on Artificial Intelligence, Morgan Kaufmann, pages 404-409, August 1993.

Oz is an experimental higher-order concurrent constraint programming system under development at DFKI. It combines ideas from logic and concurrent programming in a simple yet expressive language. From logic programming Oz inherits logic variables and logic data structures, which provide for a programming style where partial information about the values of variables is imposed concurrently and incrementally. A novel feature of Oz is that it accommodates higher-order programming without sacrificing that denotation and equality of variables are captured by first-order logic. Another new feature of Oz is constraint communication, a new form of asynchronous communication exploiting logic variables. Constraint communication avoids the problems of stream communication, the conventional communication mechanism employed in concurrent logic programming. Constraint communication can be seen as providing a minimal form of state fully compatible with logic data structures.

Based on constraint communication and higher-order programming, Oz readily supports a variety of object-oriented programming styles including multiple inheritance.

Available: PDF BibTeX Entry


Term Rewriting in Associative Commutative Theories with Identities

Martin Henz

State University of New York at Stony Brook, Master's Thesis, December 1991.

Versions of constraint rewriting for completion of rewrite systems in the presence of associative commutative operators with identities have been proposed, in which constraints are used to limit the applicability of rewrite rules. We extend these approaches such that the initially given equations can contain constraints, and such that a suitable version of unification modulo associativity, commutativity and identity can be interleaved with the process of completion.

Available: PDF BibTeX Entry


Back to top