Harvard University Computer Science Colloquium Series 33 Oxford St., Cambridge, MA 02138 Colloquium Solving #SAT Fahiem Bacchus Department of Computer Science University of Toronto http://www.cs.toronto.edu/~fbacchus/ Thursday, April 5, 2007 4:00PM Maxwell Dworkin G125 (Ice Cream at 3:30PM - Maxwell Dworkin 2nd Floor Lounge Area) Abstract #SAT is the problem of counting the number of models of a propositional formula expressed in Conjunctive Normal Form. The important practical problem of Bayesian Inference is the slight generalization of #SAT to weighted model counting. Traditional approaches to this problem employ a dynamic programming technique called variable elimination, and are able to achieve tree-width bounds when supplied with a good variable ordering. In this talk I will demonstrate how the problem can be solved using backtracking search. If caching is employed (in essence adding dynamic programming to backtracking) similar computational bounds can be achieved. If dynamic decompostion is employed in addition to caching, backtracking can be shown to perform a 1-1 emulation of the operations of variable elimination, except in a different order. However, there are a number of advantages to using backtracking, one of which is that different branches can employ different variable orderings. It can be proved that this can yield a super-polynomial speedup over variable elimination (even when variable elimination is supplied with the best possible ordering). Host: Professor Avi Pfeffer -- Carol Harlow Harvard University Maxwell Dworkin 343 33 Oxford Street Cambridge, MA 02138 _______________________________________________ Colloquium mailing list Colloquium(a)deas.harvard.edu https://lists.deas.harvard.edu/mailman/listinfo/colloquium _______________________________________________ iic-seminars mailing list iic-seminars(a)calists.harvard.edu http://calists.harvard.edu/mailman/listinfo/iic-seminars