Show simple item record

dc.contributor.authorHolden, Sean
dc.date.accessioned2021-10-27T23:30:30Z
dc.date.available2021-10-27T23:30:30Z
dc.date.issued2021
dc.identifier.issn1935-8237
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/329963
dc.description.abstractThe decision problem for Boolean satisfiability, generally referred to as SAT, is the archetypal NP-complete problem, and encodings of many problems of practical interest exist allowing them to be treated as SAT problems. Its generalization to quantified SAT (QSAT) is PSPACE-complete, and is useful for the same reason. Despite the computational complexity of SAT and QSAT, methods have been developed allowing large instances to be solved within reasonable resource constraints. These techniques have largely exploited algorithmic developments; however machine learning also exerts a significant influence in the development of state-of-the-art solvers. Here, the application of machine learning is delicate, as in many cases, even if a relevant learning problem can be solved, it may be that incorporating the result into a SAT or QSAT solver is counterproductive, because the run-time of such solvers can be sensitive to small implementation changes. The application of better machine learning methods in this area is thus an ongoing challenge, with characteristics unique to the field. This work provides a comprehensive review of the research to date on incorporating machine learning into SAT and QSAT solvers, as a resource for those interested in further advancing the field.
dc.publisherNow Publishers
dc.rightsAll rights reserved
dc.rights.urihttp://www.rioxx.net/licenses/all-rights-reserved
dc.titleMachine learning for automated theorem proving: Learning to solve SAT and QSAT
dc.typeArticle
prism.publicationDate2021
prism.publicationNameFoundations and Trends in Machine Learning
dc.identifier.doi10.17863/CAM.77407
dcterms.dateAccepted2021-10-07
rioxxterms.versionofrecord10.1561/2200000081
rioxxterms.versionAM
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserved
rioxxterms.licenseref.startdate2021-10-26
dc.contributor.orcidHolden, Sean [0000-0001-7979-1148]
dc.identifier.eissn1935-8245
rioxxterms.typeJournal Article/Review
cam.orpheus.success2021-10-27 - Embargo set during processing via Fast-track
rioxxterms.freetoread.startdate2022-04-26


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record