L773:9781956792034
Sökning: L773:9781956792034 > Certified CNF Trans...
Certified CNF Translations for Pseudo-Boolean Solving (Extended Abstract)
-
- Gocht, Stephan (författare)
- Lund University,Lunds universitet,Parallella System,Institutionen för datavetenskap,Institutioner vid LTH,Lunds Tekniska Högskola,Parallel Systems,Department of Computer Science,Departments at LTH,Faculty of Engineering, LTH,University of Copenhagen
-
- Martins, Ruben (författare)
- Carnegie Mellon University
-
- Nordström, Jakob (författare)
- Lund University,Lunds universitet,Parallella System,Institutionen för datavetenskap,Institutioner vid LTH,Lunds Tekniska Högskola,LTH profilområde: AI och digitalisering,LTH profilområden,Parallel Systems,Department of Computer Science,Departments at LTH,Faculty of Engineering, LTH,LTH Profile Area: AI and Digitalization,LTH Profile areas,Faculty of Engineering, LTH,University of Copenhagen
- visa fler...
- Elkind, Edith (redaktör/utgivare)
- visa färre...
- (creator_code:org_t)
- 2023
- 2023
- Engelska 6 s.
- Ingår i: Proceedings of the 32nd International Joint Conference on Artificial Intelligence, IJCAI 2023. - 9781956792034 ; , s. 6436-6441
- Konferensbidrag (refereegranskat)
Abstract
Ämnesord
Stäng
- The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the fact that SAT proof logging is performed in conjunctive normal form (CNF) clausal format means that it has not been possible to extend guarantees of correctness to the use of SAT solvers for more expressive combinatorial paradigms, where the first step is an unverified translation of the input to CNF. In this work, we show how cutting-planes-based reasoning can provide proof logging for solvers that translate pseudo-Boolean (a.k.a. 0-1 integer linear) decision problems to CNF and then run CDCL. We are hopeful that this is just a first step towards providing a unified proof logging approach that will extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
- Proceedings of the 32nd International Joint Conference on Artificial Intelligenc... (Sök värdpublikationen i LIBRIS)
Till lärosätets databas
Hitta mer i SwePub
- Av författaren/redakt...
- Gocht, Stephan
- Martins, Ruben
- Nordström, Jakob
- Oertel, Andy
- Elkind, Edith
- Om ämnet
-
- NATURVETENSKAP
- NATURVETENSKAP
- och Data och informa ...
- och Datavetenskap
- Artiklar i publikationen
- Proceedings of t ...
- Av lärosätet
- Lunds universitet
Sök utanför SwePub
- Sök vidare i:
- Google Book Search
- Google Scholar
Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.
- Copyright © LIBRIS - Nationella bibliotekssystem
- LIBRIS.kb.se
