Ziyi Yang

Ziyi Yang

Ph.D. Student in HKUST(GZ)

Sitemap

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

Pages

Posts

MiniSAT

less than 1 minute read

Published:

Solver.h

  • newVar 方法用于创建新的布尔变量，允许用户定义变量的极性和是否作为决策变量。
  • addClause 方法用于向求解器添加不同形式的子句（如单位子句、二元子句、三元子句等）。
  • solve 系列方法实现了不同的求解方式，可以传入假设条件，也可以不带任何假设地搜索解。
  • value, modelValue 等方法可以用于获取当前求解过程中的变量和文字的状态。
  • 提供 setConfBudget 和 setPropBudget 等方法用于设置求解器的冲突和传播预算，帮助控制资源消耗。
  • 内部数据结构
    • clauses 和 learnts 分别存储问题的原始子句和学习到的子句。
    • trail 和 trail_lim 用于保存分配给文字的决策顺序，帮助在搜索中进行回溯。
    • activity 是用于启发式搜索的变量活动度，用于决定哪些变量将被优先选中。
    • order_heap 是一个优先队列，管理当前待决策变量的顺序。
  • 求解器的几个核心功能
    • 子句附加和分离: attachClause 和 detachClause 实现了对子句的附加与删除。
    • 冲突分析: analyze 方法实现了冲突子句的回溯分析，计算出学习子句，并决定回溯的层次。
    • 启发式决策: pickBranchLit 方法选择下一个用于分支的变量。
    • 垃圾收集: garbageCollect 和 checkGarbage 方法用于管理内存，确保在必要时进行垃圾回收。

Modern C++学习笔记(三)

1 minute read

Published:

智能指针与内存管理

  • std::shared_ptr
    • 它能够记录多少个 shared_ptr 共同指向一个对象，从而消除显式的调用 delete，当引用计数变为零的时候就会将对象自动删除。std::make_shared 就能够用来消除显式的使用 new，所以std::make_shared 会分配创建传入参数中的对象， 并返回这个对象类型的std::shared_ptr指针
      #include <iostream>
#include <memory>
void foo(std::shared_ptr<int> i) {
    (*i)++;
}
int main() {
    // auto pointer = new int(10); // illegal, no direct assignment
    // Constructed a std::shared_ptr
    auto pointer = std::make_shared<int>(10);
    foo(pointer);
    std::cout << *pointer << std::endl; // 11
    // The shared_ptr will be destructed before leaving the scope
    return 0;
}

SMT Switch API 总结

less than 1 minute read

Published:

首先假设我们有一个 TransitionSystem 叫做sts

Combinational Equivalence Checking

less than 1 minute read

Published:

Improvements to Combinational Equivalence Checking: ICCAD 2006

  • main contributions:
    • use of fast logic synthesis
    • development of “intelligent simulation”
    • use of CNF-based SAT fot circuits

GPT好用的指令

less than 1 minute read

Published:

翻译中文，并且润色指令

I am writing a paper for a prestigious academic journal. I have expressed these sentences in the following section. Please translate them into English for me, and please reword them so that the text is clear, coherent, concise, and make sure that they flow smoothly from paragraph to paragraph. Remove jargon. Use a professional tone and provide me with the results in tabular form, with the original text in the first column and the embellished results followed in the second column

形式化方法综述

less than 1 minute read

Published:

论文题目

硬件设计的形式化验证研究进展及趋势

约束求解公开课笔记

less than 1 minute read

Published:

两种计算思维

  • 符号主义（约束求解）：问题可以清晰描述 Typical：定理证明
  • 连接主义（机器学习）：问题难以清晰描述 Typical：模式识别

portfolio

publications

talks

teaching