光子计算挑战赛

## **QUBO 问题求解 (题目一)** 赛题一 markdown文件格式 下载 qubo.md， CNF格式示例数据 下载 cnf_data.zip ### **背景介绍** 当代集成电路设计既精密又复杂。在芯片设计流程中，电子设计自动化（Electronic Design Automation, EDA）软件是至关重要的。其中，芯片设计验证过程扮演着非常重要的角色，它对芯片设计的正确性和安全性进行检查，占据了芯片设计成本和时间的近一半。
形式验证在芯片和电路设计中起着重要的作用。通过对硬件电路进行形式验证，可以发现和解决设计错误、时序问题、电路不变性等。形式验证已经成为确保芯片正确性和安全性的重要手段，也是EDA软件的关键模块。
然而，形式验证也面临一些挑战。对于复杂的电路设计，形式验证需要大量的计算资源和时间。近年来，集成电路规模不断增大，芯片中使用的晶体管数量也在不断增加。例如，像苹果的双芯片M1 Ultra片上系统集成了1140亿个晶体管，英伟达最新的H100芯片则有800亿个晶体管，这对形式验证的计算能力和时间要求提出了新的挑战。
形式验证问题可以在数学上转化成为QUBO问题，而基于光的并行性和高速性，光计算可用于解决QUBO问题。通过将QUBO问题转化为光学信号的处理过程，可以利用光的并行性实现对多个变量和逻辑门的并行计算。同时，光信号的高速传输和处理速度也可以提高SAT问题的求解效率。
### **赛题描述** #### **SAT问题** SAT（Satisfiability）问题是计算机科学和数理逻辑中的一个基本问题。它涉及确定是否可以通过为其变量分配布尔值来满足给定的逻辑公式。开发用于解决 SAT 问题的高效算法对人工智能、工程和密码学等各个领域具有重大意义。应用包括硬件和软件验证、规划、调度和其他优化问题。
SAT问题通常有多个布尔变量和多个变量构成的子句，例如
f=(-x1 ∨ -x2 ∨ x3) ∧ (-x3 ∨ x4)
其中x1,x2,x3,x4是四个布尔变量（True/False），变量前如果有符号“-“，表示取反。f包含了两个子句，用符号∧（与）连接，表示两者必须同时满足（True），子句内部用符号∨（或）连接，表示至少有一个满足。
这个例子的一个可行解为
x1 = x2 = x3 = x4 = True
SAT问题是一个NP完备问题。当变量子句数量增加，问题的求解复杂度会以指数级增长。
SAT问题通常以合取范式(Conjunctive Normal Form,CNF) 的格式作为输入，CNF的格式遵循以下规则： 1. 文件由注释块，标记行和子句块组成，注释块用作变量声明；标记行标记变量个数和子句块个数，分割注释和子句块，标记行前为注释块，标记行后为子句块；子句块书写问题条件。 2. 注释块中每行声明一个变量，以小写字母c 开头，形式如“c {var_id} {var_name}”, var_id 为变量序号，需从1开始且连续，var_name是变量的名称。 3. 标记行形如 `p cnf {number_of_variables} {number_of_clauses}`，其中number_of_variables是变量个数，number_of_clauses表示子句个数， 4. 子句块，每一行表示一个析取子句，仅包含或操作，且以数字0结尾。数字前的符号表示非。子句块所有的行用与操作就是CNF。 5. SAT中，要使最终CNF结果为真，要求每一行的析取子句为真。 例如上面的例子可以表示成 ``` c 1 a c 2 b c 3 c c 4 d p cnf 4 2 -1 -2 3 0 -3 4 0 ``` 其中1-4行为注释块，第5行为标记行，表示有4个变量，2个子句，，6-7行为子句块 #### **问题** 我们将提供一组CNF格式的数据作为输入，参赛者需要利用我们提供的光计算模拟器实现该问题的求解。其中文件见附件cnf_data.zip。 #### **参考思路** 基于光计算芯片中矩阵乘法计算优势，可以采用一种启发式的求解策略。具体如下：
**1. 将SAT问题用QUBO的形式来建模，这里介绍一个最直观的建模方法**

**2. 将QUBO问题转成Ising的形式**
### **注意事项** - 示例算法中，可能需要在迭代过程中添加扰动来防止被困在局部最优点的情况； - 示例算法中，可能需要对Ising矩阵M做特征处理来加速收敛； - SAT问题可能存在多个解，验证比较简单这里不再赘述； - 利用提供的光计算模拟器求解问题，oMAC模拟器的矩阵大小为256x256，当矩阵规模大于这个的时候需要自行做拆分。 - 详细描述所使用的算法，我们将在给定测试数据上完成测试评估。


开放赛题 (题目二)

赛题二 markdown文件格式 下载 qubo2.md

光计算具有高带宽，低延迟，低功耗等特性，在大规模矩阵计算中有独到的优势，然后受限于生态发展问题，光计算的应用还存在局限。在本题，我们希望参赛者发挥聪明才智，打开视野，寻找一个应用领域问题，利用曦智科技提供的光计算模拟器实现该问题的求解。 ### 答题要求 1. 1 要求详细描述该应用背景，应用行业。 2. 2 详细描述问题建模过程，建模的方法。 3. 3 利用曦智科技提供的光计算模拟器求解该问题，并提供算法说明。


模拟器（用于解题）使用说明

欢迎大家踊跃报名，因模拟器占用空间较大(~6GB)。报名成功后，曦智科技将会以邮件方式提供模拟器docker文件下载方式。
模拟器docker文件安装说明 下载 docker_image_instruction.md
oMAC_matmul.md 下载 readme.md