Heinz Kredel
Rechenzentrum
Universität Mannheim

The Java Algebra System (JAS) is an object oriented, type safe and multi-threaded approach to computer algebra. JAS provides a well designed software library using generic types for algebraic computations implemented in the Java programming language. The library can be used as any other Java software package or it can be used interactively or interpreted through an jython (Java Python) front end. The focus of JAS is at the moment on commutative and solvable polynomials, Groebner bases and applications. By the use of Java as implementation language JAS is 64-bit and multi-core cpu ready and can make use of distributed computing systems.

• Heinz Kredel; Parallel and distributed Groebner bases computation in JAS; online
• Heinz Kredel; Distributed hybrid Groebner bases computation; online
• Heinz Kredel; Distributed parallel Groebner bases computation; online

Area: Parallel and Distributed Computer Algebra

Software:

• Java Library and jython front-end krum.rz.uni-mannheim.de/jas/download.html

Links:

• http://krum.rz.uni-mannheim.de/jas/

Franz-Josef Pfreundt
Fraunhofer Institut für Techno- und Wirtschaftsmathematik (ITWM)
Fraunhofer Gesellschaft www.itwm.fhg.de

Heinz Kredel
Rechenzentrum
Universität Mannheim www.uni-mannheim.de/rum/

Alfred Geiger
T-Systems, Solutions for Research GmbH
T-Systems www.t-systems.de

Djamshid Tavangarian
Institut für Technische Informatik
Universität Rostock wwwtec.informatik.uni-rostock.de

IPACS wants to define a new basis for benchmarks measuring system performance of distributed systems. The goal is to develop methods of measurement based on new applications, low level, and grid benchmarks, which also allow performance prediction. A further significant element of the new benchmark environment is represented in the usability of the benchmarks. Mechanisms for the automatic installation and execution of benchmarks are being strived for and grid benchmarks, which also allow performance prediction.

• Michael Krietemeyer; Matthias Merz [Eds.]; IPACS-Benchmark - Integrated Performance Analysis of Computer Systems (IPACS) print
• Heinz Kredel; Matthias Merz; 'The Design of the IPACS Distributed Software Architecture' pdf

Area: Performance analysis

Software:

• Benchmark result data base

Links:

• http://www.ipacs-benchmark.org

Adrian Balint
Institute of Theoretical Computer Science
Ulm University

Andreas Fröhlich
Institute of Theoretical Computer Science
Ulm University

The propositional satisfiability problem (SAT) is one of the most studied NP-complete problems in computer science. One reason for that is the wide range of SAT's practical applications ranging from hardware verification to planning and scheduling. Given a propositional formula in conjunctive normal form (CNF) with variables x1,...,xN the SAT-problem consists in finding an assignment for the variables so that all clauses are satisfied. In this work we focus on SLS-solvers for SAT and describe how their performance can be improved with a new probability distribution. We implemented a new algorithm called Sparrow and compared it with the state of art solvers on a wide range of problems from the SAT Competition benchmark. All experiments were conducted on the BWGrid. Our results show the superior performance of Sparrow over all its competitors.

• Improving Stochastic Local Search for SAT with a New Probability Distribution in the proceedings of SAT2010 Springer LNCS 6175 p.10

Adrian Balint
Institute of Theoretical Computer Science
Universität Ulm

Michael Henn
Institute of Theoretical Computer Science
Universität Ulm

Oliver Gableske
Institute of Theoretical Computer Science
Universität Ulm

We developed a hybrid SAT solver (using SLS and DPLL mechanics) to attack the satisfiability problem. With the help of the BWgrid, we were able to provide empirical results, that such a hybrid solver is superior on satisfiable formulas.

• Adrian Balint, Michael Henn, Oliver Gableske: "A novel approach to combine a SLS- and a DPLL-solver for the satisfiability problem". In Oliver Kullmann (Ed.). Theory and Applications of Satisfiability Testing - SAT 2009, LNCS 5584, pp. 284-297, Springer 2009.

Michael Kaufmann
Wilhelm-Schickard-Institut für Informatik
Paralleles Rechnen
Universtät Tübingen

Wolfgang Küchlin
Wilhelm-Schickard-Institut für Informatik
Symbolisches Rechnen
Universtät Tübingen

Stephan Kottler
Wilhelm-Schickard-Institut für Informatik
Paralleles Rechnen
Universtät Tübingen

Given a boolean formula the satisfiability problem (SAT) asks if there exists a truth assignment to the variables of the formula such that the formula evaluates to true. Even though this problem seems to be purely theoretical there are several real-world problems that can be formulated as a SAT problem like hardware and software verification, planning, automotive product configuration and problems in bioinformatics. From the theoretical point of view SAT is NP-complete and should thus be not solvable in feasible time. However, in the last 15 years state-of-the-art SAT Solvers became able to tackle many real-world SAT instances with hundreds and thousands of variables. We aim to improve SAT solving by analysing and enhancing current solving techniques. Our main goal is to allow for more structural analysis of instances during the solving process. Moreover, we implement and evaluate hybrid and parallel solving techniques to combine different successful approaches to one robust solver. This work requires extensive evaluation and verification of the solver on huge sets of benchmarks. In the international SAT-competition 2009 our solver was able to win the silver medal in the category of satisfiable crafted instances.

• S. Kottler: SAT Solving with Reference Points, Theory and Applications of Satisfiability Testing (SAT 2010), 2010
• M. Kaufmann, S. Kottler: Proving or Disproving Planar Straight-Line Embeddability onto given Rectangles, 17th International Symposium on Graph Drawing (GD '09), 2010
• S. Kottler, M. Kaufmann, C. Sinz: Computation of Renameable Horn Backdoors, Theory and Applications of Satisfiability Testing (SAT 2008), 2008