SAT ソルバー SAT4J を使用して、部分加重最大充足可能性問題を解こうとしています。
私の .wcnf ファイルは大きく、約 100 万の制約が含まれています。
ソルバーを実行すると、出力の一部として次のようになります(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
ありがとう