5篇
您的检索式：作者名="Manya Felip"
|
|
|
题名
|
作者
|
年代
|
出处
|
被引量
|
| 1 | Reso-lution based lower bounds in MAXSAT显示文摘 | CHUMIN LI MANYA FELIP NOUREDINE MOHAMEDOU | 2010 | Journal of Con- straints2010，15，4： | 1 |
| 2 | Re- solution based lower bounds in MaxSAT 显示文摘 | Li Chumin Manya Felip Nouredine Mohamedou | 2010 | Journal of Con- straints2010，15，4： | 1 |
| 3 | New inference rules for Max-SAT 显示文摘 | Li Chumin Manya Felip Planes Jordi | 2007 | Journal of Artificial Intelligenee Research2007，30，： | 1 |
| 4 | A branching heuristic for SAT solvers based on complete implication graphs显示文摘The performance of modern conflict-driven clause learning(CDCL) SAT solvers strongly depends on branching heuristics. State-of-the-art branching heuristics, such as variable state independent decaying sum(VSIDS) and learning rate branching(LRB), are computed and maintained by aggregating the occurrences of the variables in conflicts. However, these heuristics are not sufficiently accurate at the beginning of the search because they are based on very few conflicts. We propose the distance branching heuristic, which,given a conflict, constructs a complete implication graph and increments the score of a variable considering the longest distance between the variable and the conflict rather than the simple presence of the variable in the graph. We implemented the proposed distance branching heuristic in Maple LCM and Glucose-3.0, two of the best CDCL SAT solvers, and used the resulting solvers to solve instances from the application and crafted tracks of the 2014 and 2016 SAT competitions and the main track of the 2017 SAT competition. The empirical results demonstrate that using the proposed distance branching heuristic in the initialization phase of Maple LCM and Glucose-3.0 solvers improves performance. The Maple LCM solver with the proposed distance branching heuristic in the initialization phase won the main track of the 2017 SAT competition. | Fan XIAO Chu-Min LI Mao LUO Felip MANYA Zhipeng Lü Yu LI | 2019 | Science China(Information Sciences)2019，62，7： | 0 |
| 5 | Parallel Bounded Search for the Maximum Clique Problem显示文摘Given an undirected graph,the Maximum Clique Problem(MCP)is to find a largest complete subgraph of the graph.MCP is NP-hard and has found many practical applications.In this paper,we propose a parallel Branch-and-Bound(BnB)algorithm to tackle this NP-hard problem,which carries out multiple bounded searches in parallel.Each search has its upper bound and shares a lower bound with the rest of the searches.The potential benefit of the proposed approach is that an active search terminates as soon as the best lower bound found so far reaches or exceeds its upper bound.We describe the implementation of our highly scalable and efficient parallel MCP algorithm,called PBS,which is based on a state-of-the-art sequential MCP algorithm.The proposed algorithm PBS is evaluated on hard DIMACS and BHOSLIB instances.The results show that PBS achieves a near-linear speedup on most DIMACS instances and a superlinear speedup on most BHOSLIB instances.Finally,we give a detailed analysis that explains the good speedups achieved for the tested instances. | 江华 白珂 刘海姣 李初民 Felip Manya 付樟华 | 2023 | Journal of Computer Science & Technology2023，38，5： | 0 |
您所在的机构暂未开通此部分的功能，请联系管理员