Hyunjung Park visiting Webdam

December 1st, 2010
Comments Off

Hyunjung Park is visiting webdam Friday 17 December. He is a Ph.D. student in the Department of Electrical Engineering at Stanford University. His advisor is Jennifer Widom. He is the winner of the SIGMOD 2010 Programming Contest, organized by Pierre Senellart and Serge Abiteboul. Teams of contestants from degree-granting institutions had to develop an efficient distributed query engine on top of an in-memory index. The competition received much attention, with 29 teams from 23 different institutions over the world. H. Park will give a talk on its experience of the SIGMOD 2010 Programming Contest at 2pm in the meeting room G008 of INRIA-Saclay .

Title: SIGMOD 2010 Programming Contest

Abstract: Student teams have competed to build a distributed query engine in the SIGMOD 2010 Programming Contest. In this talk, H. Park will describe the task briefly and present the winning system. Specifically, he will cover the design choices and implementation issues for the query planner and executor. Also, he will discuss several optimizations and their effectiveness.

News

Moshe Vardi visiting Webdam

October 13th, 2010
Comments Off

Moshe Y. Vardi is visiting Webdam Wednesday 3 November. He is Karen Ostrum George Professor in Computational Engineering and Director of the Computer and Information Technology Institute ((Rice University, Houston, Texas). His interests focus on applications of logic to computer science, including database theory, finite-model theory, knowledge in multi-agent systems, computer-aided verification and reasoning, and teaching logic across the curriculum. He will present his work on propositional satisfiability in the meeting room of ENS Cachan (Pavillon des Jardins) at 11:00am.

Title: Symbolic Techniques in Propositional Satisfiability Solving

Abstract: Search-based techniques in propositional satisfiability (SAT) solving have been enormously successful, leading to what is becoming known as the “SAT Revolution”. Essentially all state-of-the-art SAT solvers are based on the Davis-Putnam-Logemann-Loveland (DPLL) technique, augmented with backjumping and conflict learning. Much of current research in this area involves refinements and extensions of the DPLL technique. Yet, due to the impressive success of DPLL, little effort has gone into investigating alternative techniques. This work focuses on symbolic techniques for SAT solving, with the aim of stimulating a broader research agenda in this area.

Refutation proofs can be viewed as a special case of constraint propagation, which is a fundamental technique in solving constraint-satisfaction problems. The generalization lifts, in a uniform way, the concept of refutation from Boolean satisfiability problems to general constraint-satisfaction problems. On the one hand, this enables us to study and characterize basic concepts, such as refutation width, using tools from finite-model theory. On the other hand, this enables us to introduce new proof systems, based on representation classes, that have not been considered up to this point. We consider ordered binary decision diagrams (OBDDs) as a case study of a representation class for refutations, and compare their strength to well-known proof systems, such as resolution, the Gaussian calculus, cutting planes, and Frege systems of bounded alternation-depth. In particular, we show that refutations by ODBBs polynomially simulate resolution and can be exponentially stronger.

We then describe an effort to turn OBDD refutations into OBBD decision procedures. The idea of this approach, which we call “symbolic quantifier elimination”, is to view an instance of propositional satisfiability as an existentially quantified propositional formula. Satisfiability solving then amounts to quantifier elimination; once all quantifiers have been eliminated we are left with either 1 or 0. Our goal here is to study the effectiveness of symbolic quantifier elimination as an approach to satisfiability solving. To that end, we conduct a direct comparison with the DPLL-based ZChaff, as well as evaluate a variety of optimization techniques for the symbolic approach. In comparing the symbolic approach to ZChaff, we evaluate scalability across a variety of classes of formulas. We find that no approach dominates across all classes. While ZChaff dominates for many classes of formulas, the symbolic approach is superior for other classes of formulas.

Finally, we turn our attention to Quantified Boolean Formulas (QBF) solving. Much recent work has gone into adapting techniques that were originally developed for SAT solving to QBF solving. In particular, QBF solvers are often based on SAT solvers. Most competitive QBF solvers are search-based. Here we describe an alternative approach to QBF solving, based on symbolic quantifier elimination. We extend some symbolic approaches for SAT solving to symbolic QBF solving, using various decision-diagram formalisms such as OBDDs and ZDDs. In both approaches, QBF formulas are solved by eliminating all their quantifiers. Our first solver, QMRES, maintains a set of clauses represented by a ZDD and eliminates quantifiers via multi-resolution. Our second solver, QBDD, maintains a set of OBDDs, and eliminate quantifiers by applying them to the underlying OBDDs. We compare our symbolic solvers to several competitive search-based solvers. We show that QBDD is not competitive, but QMRESS compares favorably with search-based solvers on various benchmarks consisting of non-random formulas.

News

Proceedings Dagstuhl 2010

August 20th, 2010
Comments Off

The proceedings of the

Dagstuhl Seminar 10151 “Enabling Holistic Approaches to Business Process Lifecycle Management”
S. Abiteboul, A. Koschmider, A. Oberweis, J. Su (Eds.)

have been published.  They can be accessed through
http://drops.dagstuhl.de/portals/10151/

News ,

Webdam at Dagstuhl (2)

June 21st, 2010
Comments Off

Webdam and the Fox European project will organize a Dagstuhl workshop on Foundations of Distributed Data Management, 17-21 October 2011.
Please, if you want to attend, block the dates and stay tuned.

Events, News ,

Webdam at Yearly LSV Meeting

June 17th, 2010
Comments Off

Yannis Kastis gave a presentation of Webdam Current Research Directions, Wednesday 16 june 2010, at the Yearly LSV Meeting “Barbizon 2010″.

News ,

Balder ten Cate visiting Webdam

June 17th, 2010
Comments Off

Balder ten Cate is visiting Webdam from Monday 5 July to Saturday 10 july 2009 and from Saturday 17 July to Saturday 24 July. He is a postdoctoral researcher in the database theory group at UC Santa Cruz.

News

Bruno Marnette joining Webdam

May 25th, 2010
Comments Off

Webdam is very happy that Bruno Marnette, who previously visited us for 2 months, joined the team for a post doc.

Bruno Marnette was doing his PhD at Oxford University under the direction of Georg Gottlob.

News

Fabian & Yannis & Summer School

May 19th, 2010
Comments Off
  1. Fabian Suchanek who recently joined Webdam received the Honorable Mention at ACM Sigmod  Dissertion Awards.
  2. Yannis Papakonstantinou will be visiting Webdam for 3 weeks in July.
  3. The BDA summer school co-organized by Webdam is happening now in Les Houches. An important part of the Webdam textbook is being tested.

News , ,

Gerome Miklau visiting Webdam

April 21st, 2010
Comments Off

Gerome Miklau is visiting Webdam Wednesday 2 June at 2pm. He is an Assistant Professor at the Computer Science Department of University of Massachusetts, Amherst. He will present his work on differential privacy in the meeting room of LSV at ENS Cachan.

Title: Optimizing Linear Counting Queries Under Differential Privacy

Abstract: Differential privacy is a rigorous privacy standard that protects against powerful adversaries, offers precise accuracy guarantees, and has been successfully applied to a range of data analysis tasks. When differential privacy is satisfied, participants in a dataset enjoy the compelling assurance that information released about the dataset is virtually indistinguishable whether or not their personal data is included.

Differential privacy is achieved by introducing randomness into query answers. The original algorithm for achieving differential privacy, commonly called the Laplace mechanism, returns the true answer after the addition of random noise drawn from a Laplace distribution. If an analyst requires only the answer to a single query about the database, then the Laplace mechanism is known to be optimal. But the Laplace mechanism can be highly suboptimal when a set of correlated queries are submitted, and despite much recent work, optimal strategies for answering a collection of correlated queries are not known in general.

In this talk I will review the basic principles of differential privacy and then describe the “matrix mechanism”, a new algorithm for answering a workload of predicate counting queries. Given a workload, the mechanism first requests answers to a different set of queries, called a query strategy, which are answered using the standard Laplace mechanism. Noisy answers to the workload queries are then derived from the noisy answers to the strategy queries.

When the strategy queries are chosen appropriately, this two stage process increases accuracy (with no cost in privacy) by answering the workload queries using a more complex, correlated noise distribution. I will show that two recently-proposed algorithms, which provide accurate answers for the set of all range queries, can be seen as instances of the matrix mechanism. I will then present results on optimally choosing the query strategy to minimize the error for any given workload.

This talk is based on forthcoming work that will appear in PODS 2010 and VLDB 2010, and is joint with Chao Li, Michael Hay, Vibhor Rastogi, Andrew McGregor, and Dan Suciu.

News

Meghyn Bienvenu joining Webdam

April 20th, 2010
Comments Off

Webdam is very happy to announce that Meghyn Bienvenu is joining the project.

She is currently at University of Bremen. She is ranked 1st at CNRS, candidate at LRI, University Orsay.

News