摘要：本文首先把边着色问题转化成可满足性问题，然后利用Lipton解决SAT思想来解决边着色问题，最后应用一个实例来说明算法。
关键词：SAT问题；边着色；DNA计算
中图分类号：TP301.6文献标识码：A文章编号：1007-9599 (2013) 07-0000-02
1引言
近年来，随着在校学生人数逐年增多，高校排课安排成为一项复杂的工作。课表问题是运筹学中的时间表问题，课表问题涉及到众多因素，包括：教师、班级、教室和授课时间等。
1995年Princeton大学的Lipton解决了SAT问题。本文从图论的角度采用DNA计算来对简单课表问题进行解决。DNA计算一般由两个步骤构成：第一步，建立一个大的可行解集合的数据库；第二步，将那些不满足所给定问题的解的数据逐一删除。
2基于图论的排课模型
2.1简单排课表问题
假设教学要求的关联矩阵如表1所示，其中， 表示教师， 表示班级， 教师表示教师 需要给 上课的次数。
表1对应的关联矩阵可表示成一个图 ，如图1所示。
图1
由图1可知：图 是以一个以 为顶点集，授课关系 为边集的二分图，边集 表示。
2.2用边着色理论分配课时
定义：设 是无环图，若能用 种颜色给 的边着色，使相邻边具有不同颜色，则称 是 边可着色的，边着色数称为图 的一个正常 边着色。图 的正常 边着色的最小值，称为 的边色数，用 表示。
定理1：设 是无环图，则 。
证：因为相邻边具有不同颜色，所以与顶点 关联的边必须着不同颜色，故 。
定理2：设 是二部图，则 。
3排课问题的算法设计
3.1问题描述
本文将图 的边着色问题转化为SAT问题来解决。引入以下定理：
定理1 图的边着色问题可以转化成为SAT问题。
证明：令 ，其中 。则图 的每一种着色方案对应于向量 的一种赋值方案。则：
（1）每一条边 着一种颜色。等价于： 。
（2）相邻的边着不同的颜色。等价于：对于 ，对应的边为 ， ，其中 表示边 和 的相邻关系，（1表示相邻，0表示不相邻）， 则对于 ，满足 。
因此，图 一种着色方案是否为正常着色问题的问题等价于合取范式 是否为真的问题。
3.2边着色问题的DNA计算。具体算法如下：步骤1：对图 的每条边进行DNA编码，生成图 的所有 边着色，即得到初始数据池试管 ；步骤2：删除有边没有着色的DNA序列，保留图G的所有 边着色；步骤3：以顶点关联的边为约束条件通过删除实验，得到 边着色。
4一个实例
下面用上述算法来求解7个顶点、7条边的无向简单图 （如图1）的边3-着色问题。其中颜色集合为 。对于图1所对应的邻接矩阵为 ，元素 ，如下：
该简单图3-着色问题可以转化成21个变量， 个子句的可满足性问题：
对应算法如下：
（1）将编码顶点和边的DNA分子放入初始试管 ，经过充分反应后生成各种有向路；（2）删除包含有 中任一条边未着色的方案；（3）删除相邻边着同种颜色的方案；（4） 中的DNA串即为正常着色方案，对其进行PRC扩增，测出结果值；（5）检测试管 ，如有DNA分子存在，则其为该SAT问题的解；否则，该问题无解。
虽然编码繁琐了些，但理论上是可行的。最终可求出一种着色方法：
第一学时 ，第二学时 ，第三学时 。
5结论
本文直接给出了边着色问题的解法，而没有化成顶点着色问题。将图的 边着色问题转化为SAT问题，并给出了一个实例。该算法中编码方式虽然简单，但也存在着编码量较大的问题。
参考文献：
[1]王丽娜,仲国强.基于生物芯片技术的地图四着色问题的DNA算法[J].湖北师范学报（自然科学版）,2008,28(2）.
[2]马季兰,杨玉星.基于粘贴模型的图顶点着色问题的DNA算法[J]计算机应用.
[作者简介]马莹（1981.11-），女，在安徽理工大学理学院信息与计算科学任教，从事高等数学，线性代数等教学工作，研究方向：DNA计算及图论。
[基金项目]安徽理工大学校青年基金，编号：QN201122
