@mastersthesis{muise-mastersthesis,
  author       = {Christian Muise},
  title        = {Exploiting Modern \#SAT-Solving Techniques to Generate Implicants},
  school       = {University of Toronto},
  year         = 2009,
  keywords     = {thesis},
  url          = {http://www.haz.ca/papers/Muise-Masters-Thesis.pdf},
  abstract     = {An implicant of a propositional boolean formula is a conjunction of propositions that entails a the formula. Implicants play an important role for many tasks in AI such as knowledge compilation, circuit minimization, and diagnosis. There are many classes of implicants that are of interest including prime, irredundant, and orthogonal implicants. In general, implicants are hard to compute because the size of both the intermediate and/or final results can be exponentially large. In this work we focus on how advances in modern #SAT solvers can be exploited to effectively compute a complete set of orthogonal implicants. We develop an orthogonal implicant compiler and demonstrate its potential through experimental evaluation. Preliminary results indicate that this approach is effective at generating the orthogonal implicants of a propositional theory represented in Conjunctive Normal Form.}
}

{"_id":"PgCWYaEMJLSuRjhPp","authorIDs":["f4LpZ8LcDrvDyGuip"],"author_short":["Muise, C."],"bibbaseid":"muise-exploitingmodernsatsolvingtechniquestogenerateimplicants-2009","bibdata":{"bibtype":"mastersthesis","type":"mastersthesis","author":[{"firstnames":["Christian"],"propositions":[],"lastnames":["Muise"],"suffixes":[]}],"title":"Exploiting Modern #SAT-Solving Techniques to Generate Implicants","school":"University of Toronto","year":"2009","keywords":"thesis","url":"http://www.haz.ca/papers/Muise-Masters-Thesis.pdf","abstract":"An implicant of a propositional boolean formula is a conjunction of propositions that entails a the formula. Implicants play an important role for many tasks in AI such as knowledge compilation, circuit minimization, and diagnosis. There are many classes of implicants that are of interest including prime, irredundant, and orthogonal implicants. In general, implicants are hard to compute because the size of both the intermediate and/or final results can be exponentially large. In this work we focus on how advances in modern #SAT solvers can be exploited to effectively compute a complete set of orthogonal implicants. We develop an orthogonal implicant compiler and demonstrate its potential through experimental evaluation. Preliminary results indicate that this approach is effective at generating the orthogonal implicants of a propositional theory represented in Conjunctive Normal Form.","bibtex":"@mastersthesis{muise-mastersthesis,\n author = {Christian Muise},\n title = {Exploiting Modern \\#SAT-Solving Techniques to Generate Implicants},\n school = {University of Toronto},\n year = 2009,\n keywords = {thesis},\n url = {http://www.haz.ca/papers/Muise-Masters-Thesis.pdf},\n abstract = {An implicant of a propositional boolean formula is a conjunction of propositions that entails a the formula. Implicants play an important role for many tasks in AI such as knowledge compilation, circuit minimization, and diagnosis. There are many classes of implicants that are of interest including prime, irredundant, and orthogonal implicants. In general, implicants are hard to compute because the size of both the intermediate and/or final results can be exponentially large. In this work we focus on how advances in modern #SAT solvers can be exploited to effectively compute a complete set of orthogonal implicants. We develop an orthogonal implicant compiler and demonstrate its potential through experimental evaluation. Preliminary results indicate that this approach is effective at generating the orthogonal implicants of a propositional theory represented in Conjunctive Normal Form.}\n}\n\n","author_short":["Muise, C."],"key":"muise-mastersthesis","id":"muise-mastersthesis","bibbaseid":"muise-exploitingmodernsatsolvingtechniquestogenerateimplicants-2009","role":"author","urls":{"Paper":"http://www.haz.ca/papers/Muise-Masters-Thesis.pdf"},"keyword":["thesis"],"metadata":{"authorlinks":{"muise, c":"https://haz.ca/academic-publications.html"}}},"bibtype":"mastersthesis","biburl":"www.haz.ca/publications.bib","creationDate":"2015-01-27T23:19:15.156Z","downloads":3,"keywords":["thesis"],"search_terms":["exploiting","modern","sat","solving","techniques","generate","implicants","muise"],"title":"Exploiting Modern #SAT-Solving Techniques to Generate Implicants","year":2009,"dataSources":["94txRcb2YKX3ChmqR","DprwGzu9heN5GXy3u"]}