均为个人笔记，欢迎纠错

一些名词

la linear arithmetic
lp linear programming
dp dynamic programming

LA/LP theory 的背景和基础知识

Syntax

注意，syntax 都是写死的，只有‘ + ’没有‘ - ’就是没有‘ - ’。

Complexity

on domain ration(Q): polynomial
on domain integer(Z), ILP: NPC

LA/LP theory 在 NP-Complete hard problems 方面的应用

n-queen puzzle

subset sum problem

knapsack problem

根据物品是否可重复选择，
分为 0-1 knapsack problem 和 complete knapsack problem；
0-1 knapsack problem 不可重复选择；
complete knapsack 可重复选择；

重量小于某值，价值最大；

linear regression

non-linear arithmetics 的应用

reason constraints on rational domain Q
利用有理数的性质，若 x 是有理数，则 x = p / q，q ≠ 0，且 p，q 均为正数。

比如，求解器 Z3 支持非线性但不支持有理数域，就可用该性质将解限定在有理数域。

LA/LP 相关算法的原理

Fourier-Motzkin variable elimination
Simplex
normal forms;
tableau;
trial and fix;
Branch & Bound(B & B)
用于 ILP，比如要求解在整数域，已求得的解含有小数，就可以使用该算法。
Omega
没学，姑且记着有这么个玩意儿吧。

形式化方法：Linear Arithmetic相关推荐

鉴于现有的形式化方法（简称“桥”系列）有其优点和缺点，特发明新的“秤”系列
鉴于现有的形式化方法及其形式化语言(简称"桥"系列)具有的优点和缺点, 特依据信息基本定律发明新的"秤"系列,以扩充并解决"桥"系列所解决不 ...
形式化方法、《大象：Thinking in UML》
形式化方法英文的名称是formal methods.在逻辑科学中是指分析.研究思维形式结构的方法.它把各种具有不同内容的思维形式(主要是命题和推理)加以比较,找出其中各个部分相互联结的方式,如命题中包 ...
【形式化方法：VDM++系列】4.VDM实战1——铁路费用计算
又有将近2个月没更新博客了啊!winter holiday简直玩儿疯了的说!结果假期前学习的形式化方法已经忘了大半!面对期末作业,大脑一片空白.于是,赶快复习了一下之前学习的姿势! 这次的主要任务是完 ...
形式化方法｜形式化方法对软件开发的挑战：历史与发展
几年前到某著名大学参加学术活动,无意中听到该校两位老师闲聊,现在还记得的一句话就是"形式化方法已经不行了".看来真是隔行如隔山,评价自己不熟悉的领域,而且随便说,难免出错.在对形式 ...
形式化方法-- petri net
形式化方法-Petri net Petri net是由C.A.Petri在其博士论文中提到的,petri net 通常包含以下几个元素,分别是:库所.变迁.流关系.容量函数.初始标识.权值函数.所以p ...
2022 CCF形式化方法工业应用前沿分论坛暨中科国创高可信联合上海控安新品发布会顺利召开！...
11月27日,2022年CCF中国软件大会"形式化方法工业应用前沿"技术分论坛暨中科国创高可信联合上海控安新品发布会于线上顺利召开.本次活动由CCF形式化方法专业委员会主办,华东师 ...
CCF ChinaSoft 2022预告丨形式化方法工业应用前沿分论坛暨中科国创高可信联合上海控安新品发布...
2022年11月25-27日,2022年CCF中国软件大会(CCF ChinaSoft 2022)将于线上举行.大会将围绕"聚焦产教研用协同创新,提升关键软件供给能力"主题,举办包 ...
软件工程——形式化方法概述
目录前言一.形式化方法定义二.形式化方法分类三.形式化方法意义四.形式化方法作用五.形式化方法优缺点 1.优点 2.缺点前言形式化方法英文的名称是formalmethods,形式化方法 ...
【形式化方法】Part B: SAT And Validity（SAT和有效性）
Part B: SAT 和有效性 In Exercise 1, we've learned how to represent propositions in Z3 and how to use Z3 ...

形式化方法：Linear Arithmetic