我正在尝试使用 SAT 求解器 SAT4J 解决部分加权最大可满足性问题。
我的 .wcnf 文件很大,它包含大约一百万个约束。
当我运行求解器时,我得到以下作为输出的一部分(OutOfMemoryError : Java heap space):
Exception in thread "main" java.lang.OutOfMemoryError: Java heap space
at org.sat4j.minisat.constraints.cnf.WLClause.<init>(WLClause.java:67)
at org.sat4j.minisat.constraints.cnf.LearntWLClause.<init>(LearntWLClause.java:38)
at org.sat4j.pb.constraints.UnitBinaryWLClauseConstructor.constructLearntClause(UnitBinaryWLClauseConstructor.java:66)
at org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure.constructLearntClause(AbstractPBClauseCardConstrDataStructure.java:197)
at org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure.createUnregisteredClause(AbstractPBClauseCardConstrDataStructure.java:75)
at org.sat4j.minisat.core.Solver.analyze(Solver.java:614)
at org.sat4j.minisat.core.Solver.search(Solver.java:1245)
at org.sat4j.minisat.core.Solver.isSatisfiable(Solver.java:2018)
at org.sat4j.tools.SolverDecorator.isSatisfiable(SolverDecorator.java:114)
at org.sat4j.tools.SolverDecorator.isSatisfiable(SolverDecorator.java:114)
at org.sat4j.pb.PseudoOptDecorator.admitABetterSolution(PseudoOptDecorator.java:177)
at org.sat4j.pb.PseudoOptDecorator.admitABetterSolution(PseudoOptDecorator.java:170)
at org.sat4j.ILauncherMode$2.solve(ILauncherMode.java:311)
at org.sat4j.AbstractLauncher.solve(AbstractLauncher.java:278)
at org.sat4j.AbstractLauncher.run(AbstractLauncher.java:245)
at org.sat4j.maxsat.GenericOptLauncher.main(GenericOptLauncher.java:229)
也就是说,堆空间不足错误。如何增加堆空间的大小以及将其增加到什么合适的值?
这就是我在约束文件 constraints.wcnf 上调用 sat4j 求解器的方式:
/usr/bin/java -jar sat4j-maxsat.jar constraints.wcnf
谢谢