@misc(gccat,
 author       = {Nicolas Beldiceanu and Mats Carlsson and Jean-Xavier Rampon},
 year         = {2021},
 title        = {Global Constraint Catalog},
 note         = {\url{http://sofdem.github.io/gccat/gccat/}},
)
@proceedings(SATHAND,
 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},
)
@article(BomansonGJKS16,
 author       = {Jori Bomanson and Martin Gebser and Tomi Janhunen and Benjamin Kaufmann and Torsten Schaub},
 year         = {2016},
 title        = {Answer Set Programming Modulo Acyclicity},
 journal      = {Fundam. Informaticae},
 volume       = {147},
 number       = {1},
 pages        = {63--91},
 doi          = {10.3233/FI-2016-1398},
)
@article(Bordeaux06,
 author       = {Lucas Bordeaux and Youssef Hamadi and Lintao Zhang},
 year         = {2006},
 title        = {Propositional Satisfiability and Constraint Programming: A comparative survey},
 journal      = {ACM Comput. Surv.},
 volume       = {38},
 number       = {4},
 pages        = {1--54},
 url          = {http://doi.acm.org/10.1145/1177352.1177354},
)
@article(Brewka:2011:ASP,
 author       = {Gerhard Brewka and Thomas Eiter and Miroslaw Truszczy\'{n}ski},
 year         = {2011},
 title        = {Answer Set Programming at a Glance},
 journal      = {Commun. ACM},
 volume       = {54},
 number       = {12},
 pages        = {92--103},
 doi          = {10.1017/S1471068407003250},
)
@inproceedings(DincbasHSAGB88,
 author       = {Mehmet Dincbas and Pascal Van Hentenryck and Helmut Simonis and Abderrahmane Aggoun and Thomas Graf and Fran{\c{c}}oise Berthier},
 year         = {1988},
 title        = {The Constraint Logic Programming Language {CHIP}},
 booktitle    = {{FGCS}},
 pages        = {693--702},
)
@inproceedings(DymchenkoM15,
 author       = {Sergii Dymchenko and Mariia Mykhailova},
 year         = {2015},
 title        = {Declaratively Solving Google Code Jam Problems with Picat},
 booktitle    = {{PADL}},
 pages        = {50--57},
 doi          = {10.1007/978-3-319-19686-2\_4},
)
@article(FourerG02,
 author       = {Robert Fourer and David M. Gay},
 year         = {2002},
 title        = {Extending an Algebraic Modeling Language to Support Constraint Programming},
 journal      = {{INFORMS} J. Comput.},
 volume       = {14},
 number       = {4},
 pages        = {322--344},
 doi          = {10.1287/ijoc.14.4.322.2825},
)
@article(Hentenryck02,
 author       = {Pascal Van Hentenryck},
 year         = {2002},
 title        = {Constraint and Integer Programming in {OPL}},
 journal      = {{INFORMS} J. Comput.},
 volume       = {14},
 number       = {4},
 pages        = {345--372},
 doi          = {10.1287/ijoc.14.4.345.2826},
)
@inproceedings(HertelHU07,
 author       = {Alexander Hertel and Philipp Hertel and Alasdair Urquhart},
 year         = {2007},
 title        = {Formalizing Dangerous {SAT} Encodings},
 booktitle    = {{SAT}},
 volume       = {4501},
 pages        = {159--172},
 doi          = {10.1007/978-3-540-72788-0\_18},
)
@inproceedings(Heule21,
 author       = {Marijn J. H. Heule},
 year         = {2021},
 title        = {Chinese Remainder Encoding for Hamiltonian Cycles},
 booktitle    = {{SAT}},
 pages        = {216--224},
 doi          = {10.1007/978-3-030-80223-3\_15},
)
@inproceedings(Huang08,
 author       = {Jinbo Huang},
 year         = {2008},
 title        = {Universal Booleanization of Constraint Models},
 booktitle    = {{CP}},
 pages        = {144--158},
 doi          = {10.1007/978-3-540-85958-1\_10},
)
@article(JeavonsP12,
 author       = {Peter Jeavons and Justyna Petke},
 year         = {2012},
 title        = {Local Consistency and SAT-Solvers},
 journal      = {J. Artif. Intell. Res.},
 volume       = {43},
 pages        = {329--351},
 doi          = {10.1613/jair.3531},
)
@misc(Johnson14,
 author       = {Andrew Johnson},
 year         = {2014},
 title        = {Quasi-linear reduction of {Hamiltonian} cycle problem ({HCP}) to satisfiability problem ({SAT})},
 note         = {Available at https://priorart.ip.com/IPCOM/000237123},
)
@book(Knuth15,
 author       = {Donald Knuth},
 year         = {2015},
 title        = {The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability},
 publisher    = {Addison-Wesley},
)
@article(MalikZ09,
 author       = {Sharad Malik and Lintao Zhang},
 year         = {2009},
 title        = {Boolean satisfiability from theoretical hardness to practical success},
 journal      = {Commun. {ACM}},
 volume       = {52},
 number       = {8},
 pages        = {76--82},
 doi          = {10.1145/1536616.1536637},
)
@inproceedings(NethercoteSBBDT07,
 author       = {Nicholas Nethercote and Peter J. Stuckey and Ralph Becket and Sebastian Brand and Gregory J. Duck and Guido Tack},
 year         = {2007},
 title        = {{MiniZinc}: Towards a Standard {CP} Modelling Language},
 booktitle    = {{CP}},
 pages        = {529--543},
 doi          = {10.1007/978-3-540-74970-7\_38},
)
@article(Prestwich03,
 author       = {Steven David Prestwich},
 year         = {2003},
 title        = {{SAT} problems with chains of dependent variables},
 journal      = {Discret. Appl. Math.},
 volume       = {130},
 number       = {2},
 pages        = {329--350},
 doi          = {10.1016/S0166-218X(02)00410-9},
)
@article(StojadinovicM14,
 author       = {Mirko Stojadinovic and Filip Maric},
 year         = {2014},
 title        = {meSAT: multiple encodings of {CSP} to {SAT}},
 journal      = {Constraints An Int. J.},
 volume       = {19},
 number       = {4},
 pages        = {380--403},
 doi          = {10.1007/s10601-014-9165-7},
)
@misc(minizinchandbook,
 author       = {Peter J. Stuckey and Kim Marriott and Guido Tack},
 year         = {2021},
 title        = {The {MiniZinc} Handbook},
 note         = {\url{https://www.minizinc.org/doc-2.5.5/en/index.html}},
)
@article(TamuraTKB09,
 author       = {Naoyuki Tamura and Akiko Taga and Satoshi Kitagawa and Mutsunori Banbara},
 year         = {2009},
 title        = {Compiling finite linear {CSP} into {SAT}},
 journal      = {Constraints An Int. J.},
 volume       = {14},
 number       = {2},
 pages        = {254--272},
 doi          = {10.1007/s10601-008-9061-0},
)
@inproceedings(VelevG09,
 author       = {Miroslav N. Velev and Ping Gao},
 year         = {2009},
 title        = {Efficient {SAT} Techniques for Absolute Encoding of Permutation Problems: Application to Hamiltonian Cycles},
 booktitle    = {{SARA}},
 publisher    = {{AAAI}},
 url          = {http://www.aaai.org/ocs/index.php/SARA/SARA09/paper/view/837},
)
@inproceedings(Walsh00,
 author       = {Toby Walsh},
 year         = {2000},
 title        = {{SAT} v {CSP}},
 booktitle    = {{CP}},
 pages        = {441--456},
 doi          = {10.1007/3-540-45349-0\_32},
)
@inproceedings(Zhou20,
 author       = {Neng{-}Fa Zhou},
 year         = {2020},
 title        = {In Pursuit of an Efficient {SAT} Encoding for the Hamiltonian Cycle Problem},
 booktitle    = {{CP}},
 pages        = {585--602},
 doi          = {10.1007/978-3-030-58475-7\_34},
)
@inproceedings(ZhouF17,
 author       = {Neng{-}Fa Zhou and Jonathan Fruhman},
 year         = {2017},
 title        = {Canonicalizing High-Level Constructs in Picat},
 booktitle    = {{PADL}},
 pages        = {19--33},
 doi          = {10.1007/978-3-319-51676-9\_2},
)
@inproceedings(ZhouK17,
 author       = {Neng{-}Fa Zhou and H{\r a}kan Kjellerstrand},
 year         = {2017},
 title        = {Optimizing {SAT} Encodings for Arithmetic Constraints},
 booktitle    = {{CP}},
 pages        = {671--686},
 doi          = {10.1007/978-3-319-66158-2\_43},
)
@book(PicatBook15,
 author       = {Neng{-}Fa Zhou and H{\r a}kan Kjellerstrand and Jonathan Fruhman},
 year         = {2015},
 title        = {Constraint Solving and Planning with {Picat}},
 series       = {Springer Briefs in Intelligent Systems},
 publisher    = {Springer},
 doi          = {10.1007/978-3-319-25883-6},
)