Explaining the causes of infeasibility of Boolean formulas has many practical applications in electronic design automation and formal verification of hardware.Furthermore,a minimum explanation of infeasibility that ex...Explaining the causes of infeasibility of Boolean formulas has many practical applications in electronic design automation and formal verification of hardware.Furthermore,a minimum explanation of infeasibility that excludes all irrelevant information is generally of interest.A smallest-cardinality unsatisfiable subset called a minimum unsatisfiable core can provide a succinct explanation of infea-sibility and is valuable for applications.However,little attention has been concentrated on extraction of minimum unsatisfiable core.In this paper,the relationship between maximal satisfiability and mini-mum unsatisfiability is presented and proved,then an efficient ant colony algorithm is proposed to derive an exact or nearly exact minimum unsatisfiable core based on the relationship.Finally,ex-perimental results on practical benchmarks compared with the best known approach are reported,and the results show that the ant colony algorithm strongly outperforms the best previous algorithm.展开更多
针对说话人确认中,各目标话者模型输出评分分布不一致而导致系统确认阈值设置的困难,本文采取了通过评分规整确定系统最小检测代价函数(DCF)确认阈值的方法。在分析了已有的两种评分规整方法Z norm a l-ization和T norm a lization的基...针对说话人确认中,各目标话者模型输出评分分布不一致而导致系统确认阈值设置的困难,本文采取了通过评分规整确定系统最小检测代价函数(DCF)确认阈值的方法。在分析了已有的两种评分规整方法Z norm a l-ization和T norm a lization的基础上,提出了一种结合两者优点的组合规整方法——TZ norm a lization,并据此给出了一种阈值动态修正方法,有效地提高了系统的性能和阈值选取的鲁棒性。对历年的N IST(手机电话语音)评测语料库进行了实验,表明了该方法的有效性。展开更多
基金the National Natural Science Foundation of China (No.60603088)
文摘Explaining the causes of infeasibility of Boolean formulas has many practical applications in electronic design automation and formal verification of hardware.Furthermore,a minimum explanation of infeasibility that excludes all irrelevant information is generally of interest.A smallest-cardinality unsatisfiable subset called a minimum unsatisfiable core can provide a succinct explanation of infea-sibility and is valuable for applications.However,little attention has been concentrated on extraction of minimum unsatisfiable core.In this paper,the relationship between maximal satisfiability and mini-mum unsatisfiability is presented and proved,then an efficient ant colony algorithm is proposed to derive an exact or nearly exact minimum unsatisfiable core based on the relationship.Finally,ex-perimental results on practical benchmarks compared with the best known approach are reported,and the results show that the ant colony algorithm strongly outperforms the best previous algorithm.
文摘针对说话人确认中,各目标话者模型输出评分分布不一致而导致系统确认阈值设置的困难,本文采取了通过评分规整确定系统最小检测代价函数(DCF)确认阈值的方法。在分析了已有的两种评分规整方法Z norm a l-ization和T norm a lization的基础上,提出了一种结合两者优点的组合规整方法——TZ norm a lization,并据此给出了一种阈值动态修正方法,有效地提高了系统的性能和阈值选取的鲁棒性。对历年的N IST(手机电话语音)评测语料库进行了实验,表明了该方法的有效性。
