Meeting
Agenda Meeting
Agenda
Constructive Solid Geometry (CSG) allows us to perform set operations on solids, including union, intersection, and difference. In this talk, the solids being used are defined using closed and oriented triangular meshes.
In ray-tracing, rendering the results of CSG operations between meshes is relatively simple, and does not involve computing a mesh that represents the result of the operation. However, for my purposes, I actually need to compute the resulting mesh, which is a non-trivial task.
I will describe my approach to the problem and present examples.
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)
-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.
- Tuesday, February 9, 1999
Daniel M. Berry, Computer Systems Group, University of Waterloo, visiting from Faculty of Computer Science, Technion, Haifa Israel, will speak on ``Formal Methods, the Very Idea, Some Thoughts''.
TIME: 10:30-11:30 a.m.
ROOM: DC 1304
ABSTRACT
The talk defines formal methods (FMs) and describes economic issues involved in their application. From these considerations and the concepts implicit in ``No Silver Bullet'', it becomes clear that FMs are best applied during requirements engineering. A theory of why formal methods work when they work is offered and it is suggested that FMs help the most when the applier is most ignorant about the problem domain.