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