Solving Model-Based Diagnosis Problems with Max-SAT Solvers and Vice Versa

Alexander Feldman, Gregory Provan, Johan de Kleer, Stephan Robert, and Arjan van Gemund
Submission Type: 
Full Paper
phmc_10_085.pdf233.24 KBJuly 1, 2010 - 11:50pm

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.

Publication Control Number: 
Submission Keywords: 
Submitted by: 

follow us

PHM Society on Facebook Follow PHM Society on Twitter PHM Society on LinkedIn PHM Society RSS News Feed