@inproceedings(AlagiWeidenbach15,
 author       = {G{\'{a}}bor Alagi and Christoph Weidenbach},
 year         = {2015},
 title        = {{NRCL} - {A} Model Building Approach to the Bernays-Sch{\"{o}}nfinkel Fragment},
 editor       = {Carsten Lutz and Silvio Ranise},
 booktitle    = {Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9322},
 publisher    = {Springer},
 pages        = {69--84},
 doi          = {10.1007/978-3-319-24246-0_5},
)
@article(BachmairGanzinger94b,
 author       = {Leo Bachmair and Harald Ganzinger},
 year         = {1994},
 title        = {Rewrite-based Equational Theorem Proving with Selection and Simplification},
 journal      = {Journal of Logic and Computation},
 volume       = {4},
 number       = {3},
 pages        = {217--247},
 doi          = {10.1093/logcom/4.3.217},
 note         = {Revised version of Max-Planck-Institut f\"{u}r Informatik technical report, MPI-I-91-208, 1991},
)
@incollection(BachmairGanzinger01handbook,
 author       = {Leo Bachmair and Harald Ganzinger},
 year         = {2001},
 title        = {Resolution Theorem Proving},
 editor       = {Alan Robinson and Andrei Voronkov},
 booktitle    = {Handbook of Automated Reasoning},
 chapter      = {2},
 volume       = {I},
 publisher    = {Elsevier},
 pages        = {19--99},
 doi          = {10.1016/B978-044450813-3/50004-7},
)
@inproceedings(BaumgartnerFuchsTinelli06,
 author       = {Peter Baumgartner and Alexander Fuchs and Cesare Tinelli},
 year         = {2006},
 title        = {Lemma Learning in the Model Evolution Calculus},
 booktitle    = {LPAR},
 series       = {Lecture Notes in Computer Science},
 volume       = {4246},
 publisher    = {Springer},
 pages        = {572--586},
 doi          = {10.1016/0004-3702(94)90077-9},
)
@article(BernaysSchoenfinkel28,
 author       = {Paul Bernays and Moses Sch\"{o}nfinkel},
 year         = {1928},
 title        = {Zum Entscheidungsproblem der mathematischen Logik},
 journal      = {Mathematische Annalen},
 volume       = {99},
 pages        = {342--372},
 doi          = {10.1007/BF014591101},
)
@book(BiereEtAl09handbook,
 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(BlanchetteEtAl16,
 author       = {Jasmin Christian Blanchette and Mathias Fleury and Christoph Weidenbach},
 year         = {2016},
 title        = {A Verified {SAT} Solver Framework with Learn, Forget, Restart, and Incrementality},
 editor       = {Nicola Olivetti and Ashish Tiwari},
 booktitle    = {Automated Reasoning - 8th International Joint Conference, {IJCAR} 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9706},
 publisher    = {Springer},
 pages        = {25--44},
 doi          = {10.1007/978-3-319-43144-4},
)
@article(BonacinaPlaisted16,
 author       = {Maria Paola Bonacina and David A. Plaisted},
 year         = {2016},
 title        = {Semantically-Guided Goal-Sensitive Reasoning: Model Representation},
 journal      = {Journal of Automated Reasoning},
 volume       = {56},
 number       = {2},
 pages        = {113--141},
 doi          = {10.1007/s10817-015-9334-4},
)
@book(BradleyManna2007,
 author       = {Aaron R. Bradley and Zohar Manna},
 year         = {2007},
 title        = {{T}he {C}alculus of {C}omputation -- {D}ecision {P}rocedures with {A}pplications to {V}erification},
 publisher    = {Springer},
 doi          = {10.1007/978-3-540-74113-8},
)
@inproceedings(Bromberger18,
 author       = {Martin Bromberger},
 year         = {2018},
 title        = {A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems},
 editor       = {Didier Galmiche and Stephan Schulz and Roberto Sebastiani},
 booktitle    = {Automated Reasoning - 9th International Joint Conference, {IJCAR} 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {10900},
 publisher    = {Springer},
 pages        = {329--345},
 doi          = {10.1145/322276.322287},
)
@inproceedings(BrombergerEtAl15,
 author       = {Martin Bromberger and Thomas Sturm and Christoph Weidenbach},
 year         = {2015},
 title        = {Linear Integer Arithmetic Revisited},
 editor       = {Amy P. Felty and Aart Middeldorp},
 booktitle    = {Automated Deduction - {CADE-25} - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {9195},
 publisher    = {Springer},
 pages        = {623--637},
 doi          = {10.1016/S0747-7171(08)80051-X},
)
@article(BrombergerWeidenbach17,
 author       = {Martin Bromberger and Christoph Weidenbach},
 year         = {2017},
 title        = {New techniques for linear arithmetic: cubes and equalities},
 journal      = {Formal Methods in System Design},
 volume       = {51},
 number       = {3},
 pages        = {433--461},
 doi          = {10.1007/s10703-017-0278-7},
)
@article(FermuellerPilcher07,
 author       = {Christian G. Ferm{\"u}ller and Reinhard Pichler},
 year         = {2007},
 title        = {Model Representation over Finite and Infinite Signatures},
 journal      = {J. Log. Comput.},
 volume       = {17},
 number       = {3},
 pages        = {453--477},
 doi          = {10.1093/logcom/exm008},
)
@inproceedings(FioriWeidenbach19,
 author       = {Alberto Fiori and Christoph Weidenbach},
 year         = {2019},
 title        = {{SCL} -- Clause Learning from Simple Models},
 booktitle    = {Automated Deduction - CADE-27, 27th International Conference on Automated Deduction},
 series       = {Lecture Notes in Artificial Intelligence},
 volume       = {11716},
 publisher    = {Springer},
 pages        = {233--249},
 doi          = {10.1007/978-3-030-29436-6\_14},
)
@inproceedings(GanzingerKorovinEtAl03,
 author       = {Harald Ganzinger and Konstantin Korovin},
 year         = {2003},
 title        = {New Directions in Instatiation--Based Theorem Proving},
 editor       = {Samson Abramsky},
 booktitle    = {18th Annual IEEE Symposium on Logic in Computer Science, LICS'03},
 series       = {LICS'03},
 publisher    = {IEEE Computer Society},
 pages        = {55--64},
 doi          = {10.1109/LICS.2003.1210045},
)
@inproceedings(HeuleEtAl19,
 author       = {Marijn J. H. Heule and Benjamin Kiesl and Armin Biere},
 year         = {2019},
 title        = {Encoding Redundancy for Satisfaction-Driven Clause Learning},
 editor       = {Tom{\'{a}}s Vojnar and Lijun Zhang},
 booktitle    = {Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, {TACAS} 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part {I}},
 series       = {Lecture Notes in Computer Science},
 volume       = {11427},
 publisher    = {Springer},
 pages        = {41--58},
 doi          = {10.1007/978-3-030-17462-0},
)
@inproceedings(Karp72,
 author       = {Richard M. Karp},
 year         = {1972},
 title        = {Reducibility Among Combinatorial Problems},
 editor       = {Raymond E. Miller and James W. Thatcher},
 booktitle    = {Proceedings of a symposium on the Complexity of Computer Computations, held March 20-22, 1972, at the {IBM} Thomas J. Watson Research Center, Yorktown Heights, New York.},
 series       = {The {IBM} Research Symposia Series},
 publisher    = {Plenum Press, New York},
 pages        = {85--103},
 doi          = {10.1007/978-1-4684-2001-2\_9},
)
@book(KroeningStrichmann08,
 author       = {Daniel Kroening and Ofer Strichman},
 year         = {2008},
 title        = {Decision Procedures An Algorithmic Point of View},
 series       = {Texts in Theoretical Computer Science},
 publisher    = {Springer},
 note         = {Second Edition 2016},
)
@inproceedings(MoskewiczMadiganZhaoZhangMalik01,
 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    = {Design Automation Conference, 2001. Proceedings},
 publisher    = {ACM},
 pages        = {530--535},
 doi          = {10.1145/378239.379017},
)
@incollection(NieuwenhuisRubio01handbook,
 author       = {Robert Nieuwenhuis and Albert Rubio},
 year         = {2001},
 title        = {Paramodulation-Based Theorem Proving},
 editor       = {Alan Robinson and Andrei Voronkov},
 booktitle    = {Handbook of Automated Reasoning},
 chapter      = {7},
 volume       = {I},
 publisher    = {Elsevier},
 pages        = {371--443},
 doi          = {10.1016/B978-044450813-3/50009-6},
)
@article(Papadimitriou81,
 author       = {Christos H. Papadimitriou},
 year         = {1981},
 title        = {On the complexity of integer programming},
 journal      = {Journal of the ACM},
 volume       = {28},
 number       = {4},
 pages        = {765--768},
 doi          = {10.1145/322276.322287},
)
@inproceedings(PerezVoronkov08,
 author       = {Juan Antonio Navarro P{\'e}rez and Andrei Voronkov},
 year         = {2008},
 title        = {Proof Systems for Effectively Propositional Logic},
 editor       = {Alessandro Armando and Peter Baumgartner and Gilles Dowek},
 booktitle    = {Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings},
 series       = {LNCS},
 volume       = {5195},
 publisher    = {Springer},
 pages        = {426--440},
 doi          = {10.1023/A:1005806324129},
)
@inproceedings(PipatsrisawatDarwiche09,
 author       = {Knot Pipatsrisawat and Adnan Darwiche},
 year         = {2009},
 title        = {On the Power of Clause-Learning SAT Solvers with Restarts},
 booktitle    = {CP},
 series       = {Lecture Notes in Computer Science},
 volume       = {5732},
 publisher    = {Springer},
 pages        = {654--668},
 doi          = {10.1007/11591191_40},
)
@article(PiskacEtAl10,
 author       = {Ruzica Piskac and Leonardo Mendon{\c{c}}a de Moura and Bj{\o}rner, Nikolaj},
 year         = {2010},
 title        = {Deciding Effectively Propositional Logic Using {DPLL} and Substitution Sets},
 journal      = {Journal of Automated Reasoning},
 volume       = {44},
 number       = {4},
 pages        = {401--424},
 doi          = {10.1007/s10817-009-9161-6},
)
@article(Plaisted84,
 author       = {David A. Plaisted},
 year         = {1984},
 title        = {Complete Problems in the First-Order Predicate Calculus},
 journal      = {Journal of Computer and System Sciences},
 volume       = {29},
 pages        = {8--35},
 doi          = {10.1016/0022-0000(84)90010-2},
)
@inproceedings(MSS96,
 author       = {Jo{\~a}o P. Marques Silva and Karem A. Sakallah},
 year         = {1996},
 title        = {GRASP - a new search algorithm for satisfiability},
 booktitle    = {International Conference on Computer Aided Design, ICCAD},
 publisher    = {IEEE Computer Society Press},
 pages        = {220--227},
 doi          = {10.1109/ICCAD.1996.569607},
)
@inproceedings(SuchanekKW07,
 author       = {Fabian M. Suchanek and Gjergji Kasneci and Gerhard Weikum},
 year         = {2007},
 title        = {Yago: a core of semantic knowledge},
 editor       = {Carey L. Williamson and Mary Ellen Zurko and Patel-Schneider, Peter F. and Prashant J. Shenoy},
 booktitle    = {Proceedings of the 16th International Conference on World Wide Web, WWW 2007, Banff, Alberta, Canada, May 8-12, 2007},
 publisher    = {ACM},
 pages        = {697--706},
 doi          = {10.1145/1242572.1242667},
)
@inproceedings(SudaEtAl10,
 author       = {Martin Suda and Christoph Weidenbach and Patrick Wischnewski},
 year         = {2010},
 title        = {On the Saturation of YAGO},
 booktitle    = {Automated Reasoning, 5th International Joint Conference, IJCAR 2010},
 series       = {LNAI},
 volume       = {6173},
 publisher    = {Springer},
 address      = {Edinburgh, United Kingdom},
 pages        = {441--456},
 doi          = {10.1007/978-3-642-14203-1\_38},
)
@inproceedings(Weidenbach17,
 author       = {Christoph Weidenbach},
 year         = {2017},
 title        = {Do Portfolio Solvers Harm?},
 editor       = {Giles Reger and Dmitriy Traytel},
 booktitle    = {{ARCADE} 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017},
 series       = {EPiC Series in Computing},
 volume       = {51},
 publisher    = {EasyChair},
 pages        = {76--81},
 doi          = {10.29007/vpxm},
)