References

  1. Parosh Aziz Abdulla, Per Bjesse & Niklas Eén (2000): Symbolic Reachability Analysis Based on SAT-Solvers. In: Proc. of TACAS, LNCS 1785. Springer, pp. 411–425, doi:10.1007/3-540-46419-0_28.
  2. Fadi A. Aloul, Arathi Ramani, Igor L. Markov & Karem A. Sakallah (2002): Solving difficult SAT instances in the presence of symmetry. In: Proc. of DAC. ACM, pp. 731–736, doi:10.1145/513918.514102.
  3. Bowen Alpern, Roger Hoover, Barry K. Rosen, Peter F. Sweeney & F. Kenneth Zadeck (1990): Incremental Evaluation of Computational Circuits. In: Proc. of the ACM-SIAM Symposium on Discrete Algorithms (SODA). ACM, pp. 32–42.
  4. Bengt Aspvall, Michael F. Plass & Robert Endre Tarjan (1979): A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas. Inf. Process. Lett. 8(3), pp. 121–123, doi:10.1016/0020-0190(79)90002-4.
  5. Armin Biere (2009): Lazy hyper binary resolution. Technical Report. Dagstuhl Seminar 09461.
  6. Armin Biere (2010): Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical Report 10/1. FMV Reports Series.
  7. Armin Biere, Marijn Heule, Hans van Maaren & Toby Walsh (2009): Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications 185. IOS Press.
  8. Per Bjesse, James H. Kukula, Robert F. Damiano, Ted Stanion & Yunshan Zhu (2004): Guiding SAT Diagnosis with Tree Decompositions. In: Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003, Selected Revised Papers, Lecture Notes in Computer Science 2919. Springer, pp. 315–329, doi:10.1007/978-3-540-24605-3_24.
  9. S. Campos, J. Neves, L. Zarate & M. Song (2009): Distributed BMC: A Depth-First Approach to Explore Clause Symmetry. In: Proc. of the Intl. Conf. and Workshop on the Engineering of Computer Based Systems (ECBS 2009). IEEE Press, pp. 89–94, doi:10.1109/ECBS.2009.26.
  10. Wahid Chrabakh & Rich Wolski (2003): GrADSAT: A Parallel SAT Solver for the Grid. Technical Report. UCSB Computer Science.
  11. William Craig (1957): Linear Reasoning. A New Form of the Herbrand-Gentzen Theorem. J. Symb. Log. 22(3), pp. 250–268, doi:10.2307/2963593.
  12. Martin Davis, George Logemann & Donald Loveland (1962): A machine program for theorem-proving. Commun. ACM 5, pp. 394–397, doi:10.1145/368273.368557.
  13. Vijay D'Silva (2010): Propositional Interpolation and Abstract Interpretation. In: Proc. of ESOP, LNCS 6012. Springer, pp. 185–204, doi:10.1007/978-3-642-11957-6_11.
  14. Niklas Eén & Niklas Sörensson (2003): An Extensible SAT-solver. In: Proc. of SAT, LNCS 2919. Springer, pp. 502–518, doi:10.1007/978-3-540-24605-3_37.
  15. Malay K. Ganai, Aarti Gupta, Zijiang Yang & Pranav Ashar (2006): Efficient distributed SAT and SAT-based distributed Bounded Model Checking. Intl. J. on Software Tools for Technology Transfer (STTT) 8(4-5), pp. 387–396, doi:10.1007/s10009-005-0203-z.
  16. Chu Gorey & Peter J. Stuckey (2008): PMiniSAT: a parallelization of MiniSAT 2.0. Technical Report. SAT Race.
  17. Bernhard Haeupler, Telikepalli Kavitha, Rogers Mathew, Siddhartha Sen & Robert Endre Tarjan (2008): Faster Algorithms for Incremental Topological Ordering. In: Proc. of ICALP, LNCS 5125. Springer, pp. 421–433, doi:10.1007/978-3-540-70575-8_35.
  18. Youssef Hamadi, Said Jabbour & Lakhdar Sais (2008): ManySAT: Solver Description. Microsoft Research Technical Report MSR-TR-2008-83.
  19. Youssef Hamadi, Said Jabbour & Lakhdar Sais (2009): ManySAT: a Parallel SAT Solver. J. on Satisfiability, Boolean Modeling and Computation 6, pp. 245–262.
  20. Guoxiang Huang (1995): Constructing Craig Interpolation Formulas. In: Proc. of the Intl. Conf. on Computing and Combinatorics (COCOON), LNCS 959. Springer, pp. 181–190.
  21. Antti Eero Johannes Hyvärinen, Tommi A. Junttila & Ilkka Niemelä (2010): Partitioning SAT Instances for Distributed Solving. In: Proc. of LPAR, LNCS 6397. Springer, pp. 372–386, doi:10.1007/978-3-642-16242-8_27.
  22. Stephan Kottler (2010): SArTagnan: Solver Description. Technical Report. SAT Race 2010.
  23. Stephan Kottler (2010): SAT Solving with Reference Points. In: Proc. of SAT, LNCS 6175. Springer, pp. 143–157, doi:10.1007/978-3-642-14186-7_13.
  24. Jan Kraj\'ıcek (1997): Interpolation Theorems, Lower Bounds for Proof Systems, and Independence Results for Bounded Arithmetic. J. Symb. Log. 62(2), pp. 457–486, doi:10.2307/2275541.
  25. Alberto Marchetti-Spaccamela, Umberto Nanni & Hans Rohnert (1996): Maintaining a Topological Order Under Edge Insertions. Inf. Process. Lett. 59(1), pp. 53–58, doi:10.1016/0020-0190(96)00075-0.
  26. Kenneth L. McMillan (2003): Interpolation and SAT-Based Model Checking. In: Proc. of CAV, LNCS 2725. Springer, pp. 1–13.
  27. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang & Sharad Malik (2001): Chaff: Engineering an Efficient SAT Solver. In: Proc. of DAC. ACM, pp. 530–535.
  28. Robert Nieuwenhuis, Albert Oliveras & Cesare Tinelli (2006): Solving SAT and SAT Modulo Theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). J. ACM 53(6), pp. 937–977, doi:10.1145/1217856.1217859.
  29. David J. Pearce & Paul H. J. Kelly (2006): A dynamic topological sort algorithm for directed acyclic graphs. ACM J. of Experimental Algorithmics 11, doi:10.1145/1187436.1210590.
  30. Pavel Pudlák (1997): Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. J. Symb. Log. 62(3), pp. 981–998, doi:10.2307/2275583.
  31. Liam Roditty & Uri Zwick (2008): Improved Dynamic Reachability Algorithms for Directed Graphs. SIAM J. Comput. 37(5), pp. 1455–1471, doi:10.1137/060650271.
  32. Tobias Schubert, Matthew Lewis & Bernd Becker (2010): Antom: Solver Description. Technical Report. SAT Race.
  33. G.S. Tseitin (1968): On the complexity of derivation in propositional calculus. In: A.O. Slisenko: Structures in Constructive Mathematics and Mathematical Logic, Part II, Seminars in Mathematics (translated from Russian). Steklov Mathematical Institute, pp. 115–íV125.
  34. Christoph M. Wintersteiger, Youssef Hamadi & Leonardo de Moura (2009): A Concurrent Portfolio Approach to SMT Solving. In: Proc. of CAV, Lecture Notes in Computer Science 5643. Springer, pp. 715–720, doi:10.1007/978-3-642-02658-4_60.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org