132
O. Keszocze et al.
This fact was exploited by preprocessing SAT instances before handing them to
other solvers. While a lot of open questions—like the duration of the preprocessing
or which clauses to import—exist, the experiments indicate that the preprocessing
can be very benefiting and improve the performance of established SAT solvers. As
this result also indicates that other solvers can benefit from importing the clauses
learned by our solver, we will investigate whether using the MCTS-based CDCL
solver in a portfolio approach can be beneficial. This could be done either using
the MCTS-based solver exclusively or by integrating it in a more diverse portfolio
employing a range of different solvers. In its current development stage, our solver
is not capable of competing with established SAT solvers as a stand-alone solver.
Therefore we additionally will pursue the obvious next step of improving the solver
by means of software engineering.
References
1. Browne, C., Powley, E., Whitehouse, D., Lucas, S.M., Cowling, P.I., Rohlfshagen, P., Tavener,
S., Perez, D., Samothrakis, S., Colton, S.: A survey of Monte Carlo tree search methods. IEEE
Trans. Comput. Intell. AI Games 4(1), 1–43 (2012)
2. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–
215 (1960)
3. Goffinet, J., Ramanujan, R.: Monte-Carlo tree search for the maximum satisfiability problem.
In: Principles and Practice of Constraint Programming, pp. 251–267 (2016)
4. Gupta, A., Ganai, M.K., Wang, C.: SAT-based verification methods and applications in
hardware verification. In: Formal Methods for Hardware Verification, pp. 108–143 (2006)
5. Knuth, D.E.: Fascicle 6: Satisfiability, the Art of Computer Programming. Combinatorial
Algorithms, vol. 4. Addison-Wesley, Boston (2015)
6. Le Berre, D., Parrain, A.: The SAT4J library, release 2.2, system description. J. Satisfiabil.
Boolean Model. Comput. 7, 59–64 (2010)
7. Liang, J.H., Ganesh, V., Zulkoski, E., Zaman, A., Czarnecki, K.: Understanding VSIDS
branching heuristics in conflict-driven clause-learning SAT solvers. In: Haifa Verification
Conference, pp. 225–241. Springer, Berlin (2015)
8. Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for
SAT solvers. In: International Conference on Theory and Applications of Satisfiability Testing,
pp. 123–140. Springer, Berlin (2016)
9. Loth, M., Sebag, M., Hamadi, Y., Schoenauer, M.: Bandit-based search for constraint programming. In: International Conference on Principles and Practice of Constraint Programming,
pp. 464–480. Springer, Berlin (2013)
10. Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In:
Handbook of Satisfiability, pp. 131–153 (2009)
11. Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient
SAT solver. In: Design Automation Conference, pp. 530–535 (2001)
12. Munos, R.: From bandits to Monte-Carlo tree search: the optimistic principle applied to
optimization and planning. Tech. Rep. (2014). https://hal.archives-ouvertes.fr/hal-00747575
13. Previti, A., Ramanujan, R., Schaerf, M., Selman, B.: Monte-Carlo style UCT search for
Boolean satisfiability. In: AI*IA 2011: Artificial Intelligence Around Man and Beyond,
pp. 177–188 (2011)
O. Keszocze et al.
This fact was exploited by preprocessing SAT instances before handing them to
other solvers. While a lot of open questions—like the duration of the preprocessing
or which clauses to import—exist, the experiments indicate that the preprocessing
can be very benefiting and improve the performance of established SAT solvers. As
this result also indicates that other solvers can benefit from importing the clauses
learned by our solver, we will investigate whether using the MCTS-based CDCL
solver in a portfolio approach can be beneficial. This could be done either using
the MCTS-based solver exclusively or by integrating it in a more diverse portfolio
employing a range of different solvers. In its current development stage, our solver
is not capable of competing with established SAT solvers as a stand-alone solver.
Therefore we additionally will pursue the obvious next step of improving the solver
by means of software engineering.
References
1. Browne, C., Powley, E., Whitehouse, D., Lucas, S.M., Cowling, P.I., Rohlfshagen, P., Tavener,
S., Perez, D., Samothrakis, S., Colton, S.: A survey of Monte Carlo tree search methods. IEEE
Trans. Comput. Intell. AI Games 4(1), 1–43 (2012)
2. Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–
215 (1960)
3. Goffinet, J., Ramanujan, R.: Monte-Carlo tree search for the maximum satisfiability problem.
In: Principles and Practice of Constraint Programming, pp. 251–267 (2016)
4. Gupta, A., Ganai, M.K., Wang, C.: SAT-based verification methods and applications in
hardware verification. In: Formal Methods for Hardware Verification, pp. 108–143 (2006)
5. Knuth, D.E.: Fascicle 6: Satisfiability, the Art of Computer Programming. Combinatorial
Algorithms, vol. 4. Addison-Wesley, Boston (2015)
6. Le Berre, D., Parrain, A.: The SAT4J library, release 2.2, system description. J. Satisfiabil.
Boolean Model. Comput. 7, 59–64 (2010)
7. Liang, J.H., Ganesh, V., Zulkoski, E., Zaman, A., Czarnecki, K.: Understanding VSIDS
branching heuristics in conflict-driven clause-learning SAT solvers. In: Haifa Verification
Conference, pp. 225–241. Springer, Berlin (2015)
8. Liang, J.H., Ganesh, V., Poupart, P., Czarnecki, K.: Learning rate based branching heuristic for
SAT solvers. In: International Conference on Theory and Applications of Satisfiability Testing,
pp. 123–140. Springer, Berlin (2016)
9. Loth, M., Sebag, M., Hamadi, Y., Schoenauer, M.: Bandit-based search for constraint programming. In: International Conference on Principles and Practice of Constraint Programming,
pp. 464–480. Springer, Berlin (2013)
10. Marques-Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In:
Handbook of Satisfiability, pp. 131–153 (2009)
11. Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient
SAT solver. In: Design Automation Conference, pp. 530–535 (2001)
12. Munos, R.: From bandits to Monte-Carlo tree search: the optimistic principle applied to
optimization and planning. Tech. Rep. (2014). https://hal.archives-ouvertes.fr/hal-00747575
13. Previti, A., Ramanujan, R., Schaerf, M., Selman, B.: Monte-Carlo style UCT search for
Boolean satisfiability. In: AI*IA 2011: Artificial Intelligence Around Man and Beyond,
pp. 177–188 (2011)