Abstract | ||
---|---|---|
Boolean satisfiability (SAT) is a well-known problem in computer science, artificial intelligence, and operations research. This paper focuses on the satisfiability problem of Model RB structure that is similar to graph coloring problems and others. We propose a translation method and three effective complete SAT solving algorithms based on the characterization of Model RB structure. We translate clauses into a graph with exclusive sets and relative sets. In order to reduce search depth, we determine search order using vertex weights and clique in the graph. The results show that our algorithms are much more effective than the best SAT solvers in numerous Model RB benchmarks, especially in those large benchmark instances. |
Year | DOI | Venue |
---|---|---|
2013 | 10.1007/s11390-013-1326-4 | J. Comput. Sci. Technol. |
Keywords | Field | DocType |
clique,complete search,Boolean satisfiability,set,local search | Maximum satisfiability problem,WalkSAT,#SAT,Clique,Computer science,Boolean satisfiability problem,Algorithm,Local search (optimization),And-inverter graph,Graph coloring | Journal |
Volume | Issue | ISSN |
28 | 2 | 1860-4749 |
Citations | PageRank | References |
1 | 0.35 | 31 |
Authors | ||
8 |
Name | Order | Citations | PageRank |
---|---|---|---|
Wensheng Guo | 1 | 25 | 5.82 |
Guowu Yang | 2 | 309 | 42.99 |
郭文生 | 3 | 1 | 0.35 |
杨国武 | 4 | 1 | 0.35 |
William N. N. Hung | 5 | 304 | 34.98 |
William N. N. Hung | 6 | 304 | 34.98 |
xiaoyu | 7 | 82 | 12.85 |
xiaoyu | 8 | 82 | 12.85 |