可控制性检查系统与方法;CONTROLLABILITY CHECKING SYSTEMS AND METHODS

摘要

本发明揭示一种智慧型可控制性检查程序，其可智慧审视是否可避免列举一组控制信号输入的某些可能值(例如造成小于要列举的所有可能值)。一改良式智慧型QBF可控制性检查可运用，包括一改良式智慧型QBF解决器。该程序可包括使用可能值指配的大规模或彻底考量，同时避免列举某些可能性之一正式可控制性检查。该正式可控制性检查可审视一证明是否建立有关指配值的一结论，该证明可用来决定可能结果，包括：(1)信号提供可控制性的一结论；(2)信号不提供可控制性的一结论；或(3)无论信号提供或不提供可控制性时皆无法达成一结论。该QBF可控制性检查的结果(例如SAT、UNSAT等等)可经过验证。