English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/156055
logo share SHARE logo core CORE   Add this article to your Mendeley library MendeleyBASE

Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL
Exportar a otros formatos:


Connecting ABT with a SAT Solver

AuthorsGiráldez-Crú, Jesús ; Martin-Sanchez, Guillermo; Meseguer, Pedro
KeywordsClause learning
Distributed SAT
Issue Date29-Aug-2016
PublisherIOS Press
Citation48th European Starting AI Researcher Symposium, STAIRS 2016; Frontiers in Artificial Intelligence and Applications, 284, 2016: 179-184
AbstractMany real-world problems are encoded into SAT instances and efficiently solved by CDCL (Conflict-Driven Clause Learning) SAT solvers. However, some scenarios require distributed problem solving approaches. Privacy is often the main reason. This motivates the need to solve distributed SAT problems We analyze how this problem can be tacked in an efficient way, and present ABTSAT, a new version of the ABT (Asynchronous Backtracking) algorithm adapted to solve distributed SAT instances. It combines ABT execution with calls to CDCL SAT solvers and clause learning. ABTSAT is sound and complete, properties inherited from ABT, and solves local problems efficiently by using CDCL SAT solvers. © 2016 The authors and IOS Press.
Identifiersdoi: 10.3233/978-1-61499-682-8-179
issn: 09226389
isbn: 978-161499681-1
Appears in Collections:(IIIA) Comunicaciones congresos
Files in This Item:
File Description SizeFormat 
STAIRS 2016_FAIA284(179-84).pdf186,09 kBAdobe PDFThumbnail
Show full item record
Review this work

WARNING: Items in Digital.CSIC are protected by copyright, with all rights reserved, unless otherwise indicated.