[发明专利] 基于线性规划的布尔可满足性判定方法 – CN114091392A 全文链接一   全文链接二

 
基本信息
申请号
CN202111391168.6
申请日
20211119
公开(公告)号
CN114091392A
公开(公告)日
20220225
申请(专利权)人
中国科学院重庆绿色智能技术研究院;方成玲
申请人地址
400714 重庆市北碚区水土镇水土高新园方正大道266号
发明人
刘江;方成玲 专利类型 发明专利
摘要
本发明为基于线性规划的布尔可满足性判定方法,属于逻辑电路领域,包括如下步骤:S1提取布尔命题逻辑公式;S2:转换为等可满足的CNF布尔逻辑公式;S3:转化为CNF形式的3‑SAT问题;S4:转化为1‑in‑3‑SAT问题;S5:等效转化为一个线性规划的最优值大小问题;S6:对线性规划的最优值求解问题进行求解精度设定;S7:求解线性规划问题的最优值,并根据最优值大小来判定布尔命题逻辑公式的可满足性;S8:对于可满足的布尔命题逻辑公式,递归地对线性规划问题添加约束并进行求解,得到可满足问题的一个解答。本发明实现了在多项式时间复杂度下的快速判定,能够判定的提高效率,节约能源。
主权项
1.基于线性规划的布尔可满足性判定方法,其特征在于,该方法包含以下步骤:S1:对实际工程问题进行分析,提取布尔命题逻辑公式;S2:通过合取范式,将布尔命题逻辑公式转换为等可满足的CNF布尔逻辑公式;S3:将CNF布尔逻辑公式按照每个子句的文字个数固定为3进行等可满足转化,将CNF布尔逻辑公式的可满足性问题(SAT)转化为3‑CNF形式的3‑SAT问题;S4:将CNF形式的3‑SAT问题按照Schaefer结构进行变体,转化为1‑in‑3‑SAT问题;S5:将1‑in‑3‑SAT问题等效转化为一个线性规划的最优值大小问题;S6:对线性规划的最优值求解问题进行求解精度设定;S7:求解线性规划问题的最优值,并根据最优值大小来判定布尔命题逻辑公式的可满足性;S8:对于可满足的布尔命题逻辑公式,递归地对线性规划问题添加约束并进行求解,得到可满足问题的一个解答。

 

 
IPC信息
IPC主分类号
G06F30/3323
G 物理

G06 计算;推算;计数

G06F 电数字数据处理

 

 
法律状态信息
法律状态公告日
20220225
法律状态
公开 法律状态信息
CN202111391168 20220225 公开 公开

 

 
代理信息
代理机构名称
代理人姓名