Compactly generating all satisfying truth assignments of a horn formula
| dc.contributor.author | Wild, Marcel | |
| dc.date.accessioned | 2011-08-17T07:05:35Z | |
| dc.date.available | 2011-08-17T07:05:35Z | |
| dc.date.issued | 2012-01 | |
| dc.description | Original article available at http://jsat.ewi.tudelft.nl/ | en_ZA |
| dc.description.abstract | ENGLISH ABSTRACT: While it was known that all models of a Horn formula can be generated in outputpolynomial time, here we present an explicit algorithm as opposed to the rather vague oracle-scheme suggested in the proof of [6, Thm.4]. It is an instance of some principle of exclusion that compactly (thus not one by one) generates all models of certain Boolean formulae given in CNF. The principle of exclusion can be adapted to generate only the models of weight k. We compare and contrast it with constraint programming, 0; 1 integer programming, and binary decision diagrams. | en_ZA |
| dc.description.version | Publishers' Version | |
| dc.format.extent | 20 p. | |
| dc.identifier.citation | Wild, M. 2012. Compactly generating all satisfying truth assignments of a horn formula. Journal on Satis ability, Boolean Modeling and Computation 8, 63-82. | en_ZA |
| dc.identifier.other | 1574-0617 (online) | |
| dc.identifier.uri | http://hdl.handle.net/10019.1/16105 | |
| dc.language.iso | en_ZA | en_ZA |
| dc.publisher | Delft University in cooperation with IOS Press | en_ZA |
| dc.rights.holder | Author retain copyright | en_ZA |
| dc.subject | Horn formula | en_ZA |
| dc.subject | Mathematics | en_ZA |
| dc.subject | Algorithms | en_ZA |
| dc.subject | Output-polynomial algorithm | |
| dc.subject | Fixed-cardinality models | |
| dc.title | Compactly generating all satisfying truth assignments of a horn formula | en_ZA |
| dc.type | Article | en_ZA |