My Java program generates a large CNF instance from its data. The instance contains mostly (>95% in most case) exclusive 2-clauses: (!a v !b). Currently I use Sat4j's default solver. When I enable all of the conditions in the program, then the solver runs indefinitely. I have tried carry out some experiences to optimize the heuristic and configuration, with no luck. What are the appropriate heuristic set to solve such instances?
Asked
Active
Viewed 56 times
