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