A new algorithm for the quantified satisfiability problem, based on zero-suppressed binary decision diagrams and memoization [Elektronische Ressource] / by: Mohammad Ghasemzadeh

A NEW ALGORITHM FOR THE QUANTIFIED SATISFIABILITYPROBLEM, BASED ON ZERO-SUPPRESSED BINARY DECISIONDIAGRAMS AND MEMOIZATION.by:Mohammad GhasemzadehA Dissertation Submitted to the COMPUTER SCIENCE DEPARTMENTof the faculty of MATHEMATHICS AND SCIENCESin Partial Fulflllment of the Requirementsfor the DEGREE OF Ph.D. IN COMPUTER SCIENCEin the GRADUATE DIVISION of theUNIVERSITY OF POTSDAM, Germany2 0 0 52The dissertation of Mohammad Ghasemzadeh is approved.|||||||||||||||||||||||{Chair DateDate|||||||||||||||||||||||{DateUniversity of Potsdam, Germany.20053STATEMENT BY AUTHORThis dissertation has been submitted in partial fulflllment of requirementsfor an advanced degree at The University of Potsdam and is deposited in the Uni-versity Library to be made available to borrowers under rules of the library.Brief quotations from this dissertation are allowable without special per-mission, provided that accurate acknowledgment of source is made. Requests forpermissionforextendedquotationfromorreproductionofthismanuscriptinwholeor in part may be granted by the head of the major department or the Dean of theGraduate College when in his or her judgment the proposed use of the material isin the interests of scholarship. In all other instances, however, permission must beobtained from the author.Mohammad GhasemzadehSIGNED:4ACKNOWLEDGEMENTSMysupervisorsprofessorChristophMeinelprovidedconsistentandvaluablesupportinallaspectsofthework.