Throwing Darts: Random Sampling Helps Tree Search when the Number of Short Certificates Is Moderate
Throwing Darts: Random Sampling Helps Tree Search when the Number of Short Certificates Is Moderate
复制标题
扔飞镖：当短证书数量适中时，随机采样有助于树搜索
DOI：
10.1609/socs.v4i1.18278
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
T. Sandholm
中科院分区：
文献类型：
--
作者：
John P. Dickerson;T. Sandholm
人们通常通过构造树证书来证明可满足性/约束满足（或整数规划中的最优性）的不可行性。然而，决定如何在搜索树中分支是困难的，并且极大地影响搜索时间。我们探索了一个简单范例的力量，即向分配空间投掷随机飞镖，然后使用飞镖收集的信息来指导下一步做什么。这样的指导很容易合并到最先进的求解器中。当不可行的短证书的数量适中时，这种方法似乎工作得很好，这表明投掷飞镖的开销可以通过这些飞镖获得的信息来抵消。我们探索的结果支持这一建议的情况下，从一个新的发电机的大小和数量的短证书可以控制，并在行业的情况下，从每年的SAT比赛。
One typically proves infeasibility in satisfiability/constraint satisfaction (or optimality in integer programming) by constructing a tree certificate. However, deciding how to branch in the search tree is hard, and impacts search time drastically. We explore the power of a simple paradigm, that of throwing random darts into the assignment space and then using information gathered by that dart to guide what to do next. Such guidance is easy to incorporate into state-of-the-art solvers. This method seems to work well when the number of short certificates of infeasibility is moderate, suggesting the overhead of throwing darts can be countered by the information gained by these darts. We explore results supporting this suggestion both on instances from a new generator where the size and number of short certificates can be controlled, and on industral instances from the annual SAT competition.