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.
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.
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.
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.
Armin Biere (2010):
Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010.
Technical Report 10/1.
FMV Reports Series.
Armin Biere, Marijn Heule, Hans van Maaren & Toby Walsh (2009):
Handbook of Satisfiability.
Frontiers in Artificial Intelligence and Applications 185.
IOS Press.
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.
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.
Wahid Chrabakh & Rich Wolski (2003):
GrADSAT: A Parallel SAT Solver for the Grid.
Technical Report.
UCSB Computer Science.
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.
Martin Davis, George Logemann & Donald Loveland (1962):
A machine program for theorem-proving.
Commun. ACM 5,
pp. 394–397,
doi:10.1145/368273.368557.
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.
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.
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.
Chu Gorey & Peter J. Stuckey (2008):
PMiniSAT: a parallelization of MiniSAT 2.0.
Technical Report.
SAT Race.
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.
Youssef Hamadi, Said Jabbour & Lakhdar Sais (2008):
ManySAT: Solver Description.
Microsoft Research Technical Report MSR-TR-2008-83.
Youssef Hamadi, Said Jabbour & Lakhdar Sais (2009):
ManySAT: a Parallel SAT Solver.
J. on Satisfiability, Boolean Modeling and Computation 6,
pp. 245–262.
Guoxiang Huang (1995):
Constructing Craig Interpolation Formulas.
In: Proc. of the Intl. Conf. on Computing and Combinatorics (COCOON),
LNCS 959.
Springer,
pp. 181–190.
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.
Stephan Kottler (2010):
SArTagnan: Solver Description.
Technical Report.
SAT Race 2010.
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.
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.
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.
Kenneth L. McMillan (2003):
Interpolation and SAT-Based Model Checking.
In: Proc. of CAV,
LNCS 2725.
Springer,
pp. 1–13.
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.
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.
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.
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.
Liam Roditty & Uri Zwick (2008):
Improved Dynamic Reachability Algorithms for Directed Graphs.
SIAM J. Comput. 37(5),
pp. 1455–1471,
doi:10.1137/060650271.
Tobias Schubert, Matthew Lewis & Bernd Becker (2010):
Antom: Solver Description.
Technical Report.
SAT Race.
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.
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.
eptcs@eptcs.org