Solving model-based diagnosis problems with max-SAT solvers and vice versa

Feldman, Alexander (Delft University of Technology, Delft, The Netherlands ; School of Management and Engineering Vaud, HES-SO // University of Applied Sciences Western Switzerland) ; Provan, Gregory (University College Cork, Cork, Ireland) ; De Kleer, Johan (Palo Alto Rsearch Center, Palo Alto, California, USA) ; Robert, Stephan (School of Management and Engineering Vaud, HES-SO // University of Applied Sciences Western Switzerland) ; Van Gemund, Arjan (Delft University of Technology, Delft, The Netherlands)

In this paper we bring closer computation of consistency-based cardinality-minimal diagnosis and solving Max-SAT. We propose two algorithms for translating between those: (1) DIORAMA (DIagnOsis-based algoRithm for mAx-sat optiMizAtion) for translating cardinality-minimal consistency based diagnosis to Max-SAT and (2) MERIDIAN (Max-sat-basEd algoRIthm for DIAgNosis) for the other way around. While the former approach has been studied, solving Max-SAT instances with a diagnostic solver is, to the best of our knowledge, novel. We configure MERIDIAN with the Stochastic Local Search (SLS) solvers from the UBCSAT suite, perform extensive experimentation on fault-models of the 74XXX/ISCAS85 circuits and compare the resulting optimality to the one of the stochastic MBD algorithm SAFARI. The results show that the optimality of SAFARI is up to several-orders-of-magnitude better than that of the SLS-based Max-SAT solvers. We configure DIORAMA with SAFARI and experiment on instances from the Max-SAT competitions. While the performance of DIORAMA/SAFARI on crafted Max-SAT problems is slightly worse compared to UBCSAT, DIORAMA/SAFARI outperforms at least several-orders-of-magnitude all UBCSAT algorithms on small industrial Max-SAT instances.

Conference Type:
full paper
Ingénierie et Architecture
IICT - Institut des Technologies de l'Information et de la Communication
Portland, Oregon, 13-16 October 2010
Portland, Oregon
13-16 October 2010
8 p.
Published in:
Proceedings of 21st International Workshop on the Principles of Diagnosis, 13-16 October 2010, Portland, Oregon, USA
Appears in Collection:

 Record created 2020-04-07, last modified 2020-10-27

Download fulltext

Rate this document:

Rate this document:
(Not yet reviewed)