| id |
ndltd-OhioLink-oai-etd.ohiolink.edu-ucin1100895652
|
| record_format |
oai_dc
|
| spelling |
ndltd-OhioLink-oai-etd.ohiolink.edu-ucin11008956522021-08-03T06:10:00Z EXTENDING EXISTENTIAL QUANTIFICATION IN CONJUNCTIONS OF BDDs WEAVER, SEAN A. This thesis describes some elementary conditions under which the existential quantification of a variable, or even a set of variables, may be distributed over a conjunction of BDDs and not change the satisfiability of the conjunction. Some practical operations based on these conditions are introduced and can be integrated into the existing framework of both search-oriented and constraint-oriented methods of satisfiability. This thesis describes how a search-oriented method can be enhanced by introducing a BDD operation that can eliminate a variable v, occurring in one or more BDDs, without conjoining any of the BDDs containing v, and safely set its value before or during search. This thesis describes how the constraint-oriented method can be enhanced by introducing a BDD operation that can also eliminate a variable v, occurring in one or more BDDs, without conjoining any of the BDDs containing v, by existentially quantifying away v before or during the conjoining process. These are done by distributing the existential quantification over the conjunction of BDDs, while leaving the satisfiability of the conjunction unchanged. The worst-case complexity of these operations is linear in the total number of BDD nodes of the subset of all BDDs containing v. However, the operations may fail to eliminate v. This thesis describes a search operation that can find a partial assignment to a set of variables which will not change the satisfiability of the conjunction. The worst-case complexity of this operation is exponential in the total number of variables used in the search. However, This search may fail to find a partial assignment. This thesis then compares and contrasts the relationship of these operations to previous ones such as the pure literal rule and autarkies. 2004 English text University of Cincinnati / OhioLINK http://rave.ohiolink.edu/etdc/view?acc_num=ucin1100895652 http://rave.ohiolink.edu/etdc/view?acc_num=ucin1100895652 unrestricted This thesis or dissertation is protected by copyright: all rights reserved. It may not be copied or redistributed beyond the terms of applicable copyright laws.
|
| collection |
NDLTD
|
| language |
English
|
| sources |
NDLTD
|
| author |
WEAVER, SEAN A.
|
| spellingShingle |
WEAVER, SEAN A.
EXTENDING EXISTENTIAL QUANTIFICATION IN CONJUNCTIONS OF BDDs
|
| author_facet |
WEAVER, SEAN A.
|
| author_sort |
WEAVER, SEAN A.
|
| title |
EXTENDING EXISTENTIAL QUANTIFICATION IN CONJUNCTIONS OF BDDs
|
| title_short |
EXTENDING EXISTENTIAL QUANTIFICATION IN CONJUNCTIONS OF BDDs
|
| title_full |
EXTENDING EXISTENTIAL QUANTIFICATION IN CONJUNCTIONS OF BDDs
|
| title_fullStr |
EXTENDING EXISTENTIAL QUANTIFICATION IN CONJUNCTIONS OF BDDs
|
| title_full_unstemmed |
EXTENDING EXISTENTIAL QUANTIFICATION IN CONJUNCTIONS OF BDDs
|
| title_sort |
extending existential quantification in conjunctions of bdds
|
| publisher |
University of Cincinnati / OhioLINK
|
| publishDate |
2004
|
| url |
http://rave.ohiolink.edu/etdc/view?acc_num=ucin1100895652
|
| work_keys_str_mv |
AT weaverseana extendingexistentialquantificationinconjunctionsofbdds
|
| _version_ |
1719432036108730368
|
