摘要翻译：
代码优化和高级综合可以归结为约束满足和优化问题，如寄存器分配中的图着色问题。图着色也被用来建模与人工智能相关的更传统的CSP，如计划、时间安排和调度。可证明的最优解决方案可能是商业和国防应用所需要的。此外，对于寄存器分配和代码优化等应用程序，自然发生的图着色实例通常很小，可以最优地解决。近年来布尔可满足性(SAT)和0-1整数线性规划(ILP)算法的一波改进提出了一般的问题约简方法，而不是针对问题的启发式，因为（1）启发式可能会被新的约束扰乱，(2)启发式往往忽略结构，(3)许多相关问题是可证明的不可逼近的。问题简化通常导致高度对称的SAT实例，而对称性已知会减慢SAT求解器的速度。在这项工作中，我们比较了几种对称破缺的方法，特别是当某些类型的对称存在于所有生成的实例中时。我们专注于将CSP减少到SAT使我们能够利用SAT求解器最近的显著改进，并自动从未来的进步中受益。我们可以在不修改源代码的情况下使用各种黑盒SAT求解器，因为我们的对称破缺技术是静态的，即在预处理过程中检测对称并添加对称破缺谓词。我们工作的一个重要结果是，在我们研究的与实例无关的SBP类型及其组合中，最简单和最不完整的构造是最有效的。我们的实验还清楚地表明，与实例无关的对称性应该与实例特定的对称性一起处理，而不是在规范级别处理，这与文献中所建议的相反。
---
英文标题：
《Breaking Instance-Independent Symmetries In Exact Graph Coloring》
---
作者：
F. A. Aloul, I. L. Markov, A. Ramani, K. A. Sakallah
---
最新提交年份：
2011
---
分类信息：

一级分类：Computer Science        计算机科学
二级分类：Artificial Intelligence        人工智能
分类描述：Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域，除了视觉、机器人、机器学习、多智能体系统以及计算和语言（自然语言处理），这些领域有独立的学科领域。特别地，包括专家系统，定理证明（尽管这可能与计算机科学中的逻辑重叠），知识表示，规划，和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--

---
英文摘要：
  Code optimization and high level synthesis can be posed as constraint satisfaction and optimization problems, such as graph coloring used in register allocation. Graph coloring is also used to model more traditional CSPs relevant to AI, such as planning, time-tabling and scheduling. Provably optimal solutions may be desirable for commercial and defense applications. Additionally, for applications such as register allocation and code optimization, naturally-occurring instances of graph coloring are often small and can be solved optimally. A recent wave of improvements in algorithms for Boolean satisfiability (SAT) and 0-1 Integer Linear Programming (ILP) suggests generic problem-reduction methods, rather than problem-specific heuristics, because (1) heuristics may be upset by new constraints, (2) heuristics tend to ignore structure, and (3) many relevant problems are provably inapproximable.   Problem reductions often lead to highly symmetric SAT instances, and symmetries are known to slow down SAT solvers. In this work, we compare several avenues for symmetry breaking, in particular when certain kinds of symmetry are present in all generated instances. Our focus on reducing CSPs to SAT allows us to leverage recent dramatic improvement in SAT solvers and automatically benefit from future progress. We can use a variety of black-box SAT solvers without modifying their source code because our symmetry-breaking techniques are static, i.e., we detect symmetries and add symmetry breaking predicates (SBPs) during pre-processing.   An important result of our work is that among the types of instance-independent SBPs we studied and their combinations, the simplest and least complete constructions are the most effective. Our experiments also clearly indicate that instance-independent symmetries should mostly be processed together with instance-specific symmetries rather than at the specification level, contrary to what has been suggested in the literature.
---
PDF链接：
https://arxiv.org/pdf/1109.2347