摘要
ExplainingthecausesofinfeasibilityofBooleanformulashasmanypracticalapplicationsinelectronicdesignautomationandformalverificationofhardware.Furthermore,aminimumexplanationofinfeasibilitythatexcludesallirrelevantinformationisgenerallyofinterest.Asmallest-cardinalityunsatisfiablesubsetcalledaminimumunsatisfiablecorecanprovideasuccinctexplanationofinfea-sibilityandisvaluableforapplications.However,littleattentionhasbeenconcentratedonextractionofminimumunsatisfiablecore.Inthispaper,therelationshipbetweenmaximalsatisfiabilityandmini-mumunsatisfiabilityispresentedandproved,thenanefficientantcolonyalgorithmisproposedtoderiveanexactornearlyexactminimumunsatisfiablecorebasedontherelationship.Finally,ex-perimentalresultsonpracticalbenchmarkscomparedwiththebestknownapproacharereported,andtheresultsshowthattheantcolonyalgorithmstronglyoutperformsthebestpreviousalgorithm.
出版日期
2008年05月15日(中国期刊网平台首次上网日期,不代表论文的发表时间)