Files

Abstract

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.

Details

Actions

PDF