Meeting Agenda

Wednesday, February 10, 1999

Location:

DC1304

Time:

1:30

Chair:

Ian Bell 

1. Adoption of the Agenda - additions or deletions

2. Coffee Hour

Coffee hour this week:

Viet-Tam Luu

Coffee hour next week:

?

3. Next meeting

Date:

Wednesday, February 17, 1999

Location:

DC1304

Time:

1:30

Chair:

Blair Conrad 

Technical presentation:

Ian Bell 

4. Forthcoming

Chairs:

1. Bill Cowan 
2. Erik Demaine

Tech Presenters:

1. Blair Conrad 
2. Bill Cowan 

5. Technical Presentation

Presenter:

• Daming Yao 

Virtual human is an important part of a virtual environment. I have tried to build a small virtual environment with a virtual human on each computer. The system includes the following parts:

1. The geometrical model of human;
2. The network model for transportation;
3. A prediction algorithm to reduce the network transportation.

6. General Discussion Items

• CD-R and piracy (Blair)
• mud downtime (Blair)

 

7. Action List

Cables (Eric, Blair)

DGP visit, end of March (Ian)

Alias/Side Effects talks (Mike)

Individual pictures for the cgl agenda/minutes

Group photo on the web page (Mark)

8. Director's Meeting

9. Seminars

St. Jerome's University, Waterloo ON - Richard M. Stallman writes sophisticated computer software for free. Stallman's software is free to copy, free to redistribute, and free to change so long as the source code to all modifications is also made available for free.

On Monday, 22 February 1999 at 3:30 pm, Stallman will present "Free Software! The GNU Project" in Siegfried Hall, St. Jerome's University, University of Waterloo. Admission is free and all are welcome.

   -Thursday, February 11, 1999 *NOTE DATE CHANGE*

Toniann Pitassi, Dept. Comp. Sci., University of Arizona, will speak on ``Satisfiability and the Efficiency of
Resolution''.

TIME:                10:30-11:30 a.m.
ROOM:                DC 1304

ABSTRACT

The  importance  of  the  satisfiability  problem (SAT) permeates  all  areas  of computer science. In the last three  decades,  there  has been a tremendous amount of research  in  trying  to  understand  the mathematical structure   of   the   satisfiability  problem  and  in developing    good   heuristics   for   SAT   and   the complementary problem of propositional theorem proving. In  fact,  there is a resurgence within AI of trying to solve  planning and reasoning problems by reductions to (variants  of)  SAT.  The  oldest and most well-studied class  of  algorthms for SAT are resolution-based, with the  Davis-Putnam  procedure  being  the  most  typical example.

We   are   motivated  by  trying  to  uncover  a  clean combinatorial characterization of the class of formulas exhibiting short resolution refutations. A related goal is  to  study  specific resolution-based algorithms for SAT,  and  again find a clean characterization of those formulas   that   are   efficiently   decided   (to  be satisfiable  or  not)  by the algorithm. In particular, exactly  when  will  the popular Davis-Putnam procedure find    a    refutation    efficiently?   Under   which distributions  will various heuristics perform well? Is there  a  ``most efficient'' resolution-based algorithm for  SAT?  Obtaining strong lower bounds for resolution necessarily underlies the answers to these questions.

In  this  talk, we present several new and simple upper and  lower  bounds for Resolution for specific formulas as well as for randomly generated formulas. Many of our bounds  are  nearly  tight, and our methods reveal that minimum  clause  size  is  an  important  parameter for studying  proof  length.  This idea was used explicitly by  Ben-Sassoon  and  Wigderson very recently to obtain simpler proofs of our results. We will also discuss the related question of whether there is a universal search algorithm for resolution.

This  is  joint  work with Paul Beame, Richard Karp and Mike Saks.
 
 

10. Lab Cleanup