Augmenting the power of (partial) MaxSat resolution with extension
Visualitza/Obre
AAAI_20.pdf (221,0Kb) (Accés restringit)
Sol·licita una còpia a l'autor
Què és aquest botó?
Aquest botó permet demanar una còpia d'un document restringit a l'autor. Es mostra quan:
- Disposem del correu electrònic de l'autor
- El document té una mida inferior a 20 Mb
- Es tracta d'un document d'accés restringit per decisió de l'autor o d'un document d'accés restringit per política de l'editorial
Cita com:
hdl:2117/329792
Tipus de documentComunicació de congrés
Data publicació2020
EditorAAAI Press
Condicions d'accésAccés restringit per política de l'editorial
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
ProjecteSOLUCIONES EFECTIVAS BASADAS EN LA LOGICA (MINECO-TIN2015-69175-C4-3-R)
RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES (AEI-RTI2018-094403-B-C33)
RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES (AEI-RTI2018-094403-B-C33)
Abstract
The refutation power of SAT and MaxSAT resolution is challenged by problems like the soft and hard Pigeon Hole Problem PHP for which short refutations do not exist. In this paper we augment the MaxSAT resolution proof system with an extension rule. The new proof system MaxResE is sound and complete, and more powerful than plain MaxSAT resolution, since it can refute the soft and hard PHP in polynomial time. We show that MaxResE refutations actually subtract lower bounds from the objective function encoded by the formulas. The resulting formula is the residual after the lower bound extraction. We experimentally show that the residual of the soft PHP (once its necessary cost of 1 has been efficiently subtracted with MaxResE) is a concise, easy to solve, satisfiable problem.
CitacióLarrosa, J.; Rollón, E. Augmenting the power of (partial) MaxSat resolution with extension. A: AAAI Conference on Artificial Intelligence. "Thirty-Fourth AAAI Conference on Artificial Intelligence. Thirty-Second Conference on Innovative Applications of Artificial Intelligence. The Tenth Symposium on Educational Advances in Artificial Intelligence: February 7–12th, 2020, New York Hilton Midtown, New York, New York, USA (Proceedings of the AAAI Conference on Artificial Intelligence, vol 34, no 02: AAAI-20 technical tracks 2)". AAAI Press, 2020, p. 1561-1568. ISBN 978-1-57735-835-0. DOI 10.1609/aaai.v34i02.5516.
ISBN978-1-57735-835-0
Versió de l'editorhttps://aaai.org/ojs/index.php/AAAI/article/view/5516
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
AAAI_20.pdf | 221,0Kb | Accés restringit |