UCSC Baskin School of Engineering: People: Allen Van Gelder

University of California at Santa Cruz
		Faculty

avg
@
cs.ucsc.edu

Office: E2-355 (831)459-4611

ALLEN VAN GELDER

Professor of Computer Science

Education:
B.S., Mathematics, Massachusetts Institute of Technology
Ph.D., Computer Science, Stanford University

Allen Van Gelder's research interests include development of algorithms for propositional satisfiability and quantified boolean formulas, methods for verifiable software, theorem proving, analysis of algorithms, parallel algorithms, computer graphics, and scientific visualization. He received a National Science Foundation Presidential Young Investigator Award in 1989 to investigate the use of logic programming for problems in database and artificial intelligence systems.

CMPS 101 Spring 2012 web page Algorithms and Abstract Data Types

Papers by Allen Van Gelder Papers by Title

Review-Period Papers by Title by Allen Van Gelder

indexPapersPdf.html by Allen Van Gelder

Various software (ftp)

ColorSat misc files related to graph coloring with SAT

CarefulRanking documentation and code related to SAT 2011 paper.

ProofChecker documentation and code

WildBenches2009 has 20 benchmarks from the Application section of the SAT 2009 competition, phase 2.
The reason these are called wild is that their behavior seems to be rather unpredicatable. It might be that solver A solves instance 1 in a minute or so while solver B times out at 5 hours, and at the same time, solver B solves instance 2 in a minute or so while solver A times out at 5 hours. In some cases, slightly jiggling an instance or a parameter of the solver changes the time by a large factor. I am talking about good solvers that did well in this competition and/or earlier competitions.
The selection is heuristic, not scientific. My intention is to have a set of benchmarks that a researcher can conceivably solve completely without ANY timeouts. Some instances are SAT, some are UNSAT.
Also see the main web page http://www.satcompetition.org.

purse-poster.pdf SAT 2005 and 2007 Competition Scoring Rules
purse-poster.ps and some 2005 results

JSAT System Description Papers
Call (unofficial)
Proposal and Motivation
Allen Van Gelder and Daniel LeBerre

CMPS201, Analysis of Algorithms, Fall 2009:
Fall 2009 web page

SAT 2007 Lisboa/Lisbon Map (jpg)

Information on Winter 2011 CMPS 290A

Office Hours, Winter 2011: MW 2:00-3:00, plus drop-in or appt.

c-adt.ps c-adt.pdf

For information about Computer Algorithms, Third Edition by Sara Baase and myself, please click here to see Supplements (including errata, clarifications, sample code, javaToC hints)
or shift-click to download Supplements.tar (about 320 KB)
or visit these links to other servers, and use the Back button on your browser if you want to return to this page.
Prof. Baase's web site: http://www-rohan.sdsu.edu/faculty/baase
AWL Publisher's information
Prof. Ben Choi's web site at Louisiana Tech University for PowerPoint slides to accompany the text. He offered to make them available to other instructors.
http://www2.latech.edu/~choi/Bens/Teaching/Csc520/

Please click here to see TPTPparser (lex/yacc sources, linux/intel binary, sample input, README, tarball)

Please click here to see http://jsat.ewi.tudelft.nl (Journal of Satisfiability home page)

ssh-cookbook Text file, what to do at soe to use ssh from outside soe. NOT KEPT UP.

Information on dbx for C programs on Solaris machines
Undergrads not in my course are welcome to use these files, but please consult your course's TAs and tutors with questions. Sorry, but there are hundreds of you.
Grads, instructors, visitors, I'll try to answer questions.

student-dbx-guide Text file, basics of using dbx. See CASE 3 for why to use cc/dbx rather than gcc/gdb.
student.dbxrc Sample dbx startup file, text, hopefully self-explanatory.

WhyIavoidGcc Judge for yourself.

Please click here to see Poster directory with some examples of using latex to make a poster.

My Erdös number is 3, e.g. through the path AVG - Jeff Ullman - Ron Graham - PE. Also, my Erdös number of the second kind (where only two-authored papers count) is ???, through the path AVG - ??? - PE. Thanks to Jan Johannsen for publicizing how to figure this out. Don't miss other interesting stuff on his home page, such as the Proof Complexity Theme Song.