Coprocessor 2.0 – A Flexible CNF Simplifier

1. Manthey, N.: Coprocessor – a Standalone SAT Preprocessor. In: Proceedings of the 25th Workshop on Logic Programming, WLP 2011, Infsys Research Report 1843-11-06, Technische Universität Wien, 99–104 (2011)

   Google Scholar 

2. Eén, N., Biere, A.: Effective Preprocessing in SAT Through Variable and Clause Elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005)

   Chapter  Google Scholar 

3. Järvisalo, M., Biere, A., Heule, M.: Blocked Clause Elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129–144. Springer, Heidelberg (2010)

   Chapter  Google Scholar 

4. Heule, M., Järvisalo, M., Biere, A.: Clause Elimination Procedures for CNF Formulas. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 357–371. Springer, Heidelberg (2010)

   Chapter  Google Scholar 

5. Berre, D.L., Parrain, A.: The Sat4j library, release 2.2. JSAT 7(2-3), 56–59 (2010)

   Google Scholar 

6. Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci. 89(4), 543–560 (2003)

   Article  Google Scholar 

7. Lynce, I., Marques-Silva, J.: Probing-Based Preprocessing Techniques for Propositional Satisfiability. In: Proceedings of the 15th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2003. IEEE Computer Society (2003)

   Google Scholar 

8. Li, C.M.: A constraint-based approach to narrow search trees for satisfiability. Inf. Process. Lett. 71, 75–80 (1999)

   Article  MATH  Google Scholar 

9. Piette, C., Hamadi, Y., Saïs, L.: Vivifying propositional clausal formulae. In: 18th European Conference on Artificial Intelligence (ECAI 2008), Patras, Greece, pp. 525–529 (2008)

   Google Scholar 

10. Heule, M.J.H., Järvisalo, M., Biere, A.: Efficient CNF Simplification Based on Binary Implication Graphs. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol. 6695, pp. 201–215. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

11. Van Gelder, A.: Toward leaner binary-clause reasoning in a satisfiability solver. Ann. Math. Artif. Intell. 43(1), 239–253 (2005)

    Article  MathSciNet  MATH  Google Scholar 

12. Manthey, N., Steinke, P.: Quadratic Direct Encoding vs. Linear Order Encoding. Technical Report 3, Knowledge Representation and Reasoning Group, Technische Universität Dresden, 01062 Dresden, Germany (2011)

    Google Scholar 

13. Chen, J.: A New SAT Encoding of the At-Most-One Constraint. In: Proceedings of ModRef 2011 (2011)

    Google Scholar 

14. Wernhard, C.: Computing with Logic as Operator Elimination: The ToyElim System. In: Proceedings of the 25th Workshop on Logic Programming, WLP 2011, Infsys Research Report 1843-11-06, Technische Universität Wien, pp. 94–98 (2011)

    Google Scholar 

15. Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical Report 10/1, Institute for Formal Models and Verification, Johannes Kepler University (2010)

    Google Scholar 

16. Soos, M.: CryptoMiniSat 2.5.0. In: SAT Race Competitive Event Booklet (2010)

    Google Scholar 

17. Manthey, N.: Solver Description of riss and priss. Technical Report 2, Knowledge Representation and Reasoning Group, Technische Universität Dresden, 01062 Dresden, Germany (2012)

    Google Scholar 

18. Brummayer, R., Biere, A.: Fuzzing and delta-debugging smt solvers. In: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, SMT 2009, pp. 1–5. ACM, New York (2009)

    Chapter  Google Scholar 

Download references