Cai, Shaowei; Zhang, Xindi Deep cooperation of CDCL and local search for SAT. (English) Zbl 07495566 Li, Chu-Min (ed.) et al., Theory and applications of satisfiability testing – SAT 2021. 24th international conference, Barcelona, Spain, July 5–9, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12831, 64-81 (2021). MSC: 68Q25 68R07 68T20 PDFBibTeX XMLCite \textit{S. Cai} and \textit{X. Zhang}, Lect. Notes Comput. Sci. 12831, 64--81 (2021; Zbl 07495566) Full Text: DOI
Weinzierl, Antonius; Taupe, Richard; Friedrich, Gerhard Advancing lazy-grounding ASP solving techniques – restarts, phase saving, heuristics, and more. (English) Zbl 1468.68228 Theory Pract. Log. Program. 20, No. 5, 609-624 (2020). MSC: 68T30 68N17 68T20 PDFBibTeX XMLCite \textit{A. Weinzierl} et al., Theory Pract. Log. Program. 20, No. 5, 609--624 (2020; Zbl 1468.68228) Full Text: DOI arXiv
Marques-Silva, Joao; Malik, Sharad Propositional SAT solving. (English) Zbl 1392.68380 Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 247-275 (2018). MSC: 68T15 PDFBibTeX XMLCite \textit{J. Marques-Silva} and \textit{S. Malik}, in: Handbook of model checking. Cham: Springer. 247--275 (2018; Zbl 1392.68380) Full Text: DOI
Liang, Jia Hui; Hari Govind, V. K.; Poupart, Pascal; Czarnecki, Krzysztof; Ganesh, Vijay An empirical study of branching heuristics through the lens of global learning rate. (English) Zbl 1496.68304 Gaspers, Serge (ed.) et al., Theory and applications of satisfiability testing – SAT 2017. 20th international conference, Melbourne, VIC, Australia, August 28 – September 1, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10491, 119-135 (2017). MSC: 68T20 68T05 PDFBibTeX XMLCite \textit{J. H. Liang} et al., Lect. Notes Comput. Sci. 10491, 119--135 (2017; Zbl 1496.68304) Full Text: DOI
Loveland, Donald; Sabharwal, Ashish; Selman, Bart DPLL: the core of modern satisfiability solvers. (English) Zbl 1439.68026 Omodeo, Eugenio G. (ed.) et al., Martin Davis on computability, computational logic, and mathematical foundations. Cham: Springer. Outst. Contrib. Log. 10, 315-335 (2016). MSC: 68V15 68-03 68R07 68T20 PDFBibTeX XMLCite \textit{D. Loveland} et al., Outst. Contrib. Log. 10, 315--335 (2016; Zbl 1439.68026) Full Text: DOI
Kroening, Daniel; Strichman, Ofer [Bjørner, Nikolaj; de Moura, Leonardo; Kugler, Hillel] Decision procedures. An algorithmic point of view. 2nd edition. (English) Zbl 1358.68002 Texts in Theoretical Computer Science. An EATCS Series. Berlin: Springer (ISBN 978-3-662-50496-3/hbk; 978-3-662-50497-0/ebook). xxi, 356 p. (2016). MSC: 68-01 68-02 68T15 68T20 68T27 PDFBibTeX XMLCite \textit{D. Kroening} and \textit{O. Strichman}, Decision procedures. An algorithmic point of view. 2nd edition. Berlin: Springer (2016; Zbl 1358.68002) Full Text: DOI
Liang, Jia Hui; Ganesh, Vijay; Poupart, Pascal; Czarnecki, Krzysztof Learning rate based branching heuristic for SAT solvers. (English) Zbl 1475.68348 Creignou, Nadia (ed.) et al., Theory and applications of satisfiability testing – SAT 2016. 19th international conference, Bordeaux, France, July 5–8, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9710, 123-140 (2016). MSC: 68T20 68T05 PDFBibTeX XMLCite \textit{J. H. Liang} et al., Lect. Notes Comput. Sci. 9710, 123--140 (2016; Zbl 1475.68348) Full Text: DOI
Biere, Armin; Fröhlich, Andreas Evaluating CDCL variable scoring schemes. (English) Zbl 1471.68238 Heule, Marijn (ed.) et al., Theory and applications of satisfiability testing – SAT 2015. 18th international conference, Austin, TX, USA, September 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9340, 405-422 (2015). MSC: 68T20 PDFBibTeX XMLCite \textit{A. Biere} and \textit{A. Fröhlich}, Lect. Notes Comput. Sci. 9340, 405--422 (2015; Zbl 1471.68238) Full Text: DOI
Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser A taxonomy of exact methods for partial Max-SAT. (English) Zbl 1280.68243 J. Comput. Sci. Technol. 28, No. 2, 232-246 (2013). MSC: 68T20 68Q25 PDFBibTeX XMLCite \textit{M. E. B. Menai} and \textit{T. N. Al-Yahya}, J. Comput. Sci. Technol. 28, No. 2, 232--246 (2013; Zbl 1280.68243) Full Text: DOI
Van Gelder, Allen Producing and verifying extremely large propositional refutations. (English) Zbl 1273.68329 Ann. Math. Artif. Intell. 65, No. 4, 329-372 (2012). Reviewer: Nail Zamov (Kazan) MSC: 68T15 PDFBibTeX XMLCite \textit{A. Van Gelder}, Ann. Math. Artif. Intell. 65, No. 4, 329--372 (2012; Zbl 1273.68329) Full Text: DOI
Gebser, Martin; Kaufmann, Benjamin; Schaub, Torsten Conflict-driven answer set solving: from theory to practice. (English) Zbl 1251.68060 Artif. Intell. 187-188, 52-89 (2012). MSC: 68N17 68T27 PDFBibTeX XMLCite \textit{M. Gebser} et al., Artif. Intell. 187--188, 52--89 (2012; Zbl 1251.68060) Full Text: DOI
Buss, Samuel R. Towards NP-P via proof complexity and search. (English) Zbl 1257.03086 Ann. Pure Appl. Logic 163, No. 7, 906-917 (2012). Reviewer: Olaf Beyersdorff (Leeds) MSC: 03F20 03B05 03D15 68Q15 68Q17 68T15 PDFBibTeX XMLCite \textit{S. R. Buss}, Ann. Pure Appl. Logic 163, No. 7, 906--917 (2012; Zbl 1257.03086) Full Text: DOI
Sakallah, Karem A.; Marques-Silva, Joao Anatomy and empirical evaluation of modern SAT solvers. (English) Zbl 1258.68137 Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 103, 95-121 (2011). MSC: 68T20 68Q17 68Q32 PDFBibTeX XMLCite \textit{K. A. Sakallah} and \textit{J. Marques-Silva}, Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 103, 95--121 (2011; Zbl 1258.68137)
Marić, Filip; Janičić, Predrag Formalization of abstract state transition systems for SAT. (English) Zbl 1237.68179 Log. Methods Comput. Sci. 7, No. 3, Paper No. 19, 37 p. (2011). MSC: 68T15 68Q60 PDFBibTeX XMLCite \textit{F. Marić} and \textit{P. Janičić}, Log. Methods Comput. Sci. 7, No. 3, Paper No. 19, 37 p. (2011; Zbl 1237.68179) Full Text: DOI arXiv
Balduccini, Marcello Learning and using domain-specific heuristics in ASP solvers. (English) Zbl 1215.68207 AI Commun. 24, No. 2, 147-164 (2011). MSC: 68T15 68N17 68T05 68T20 PDFBibTeX XMLCite \textit{M. Balduccini}, AI Commun. 24, No. 2, 147--164 (2011; Zbl 1215.68207) Full Text: Link
Gebser, Martin; Kaufmann, Benjamin; Kaminski, Roland; Ostrowski, Max; Schaub, Torsten; Schneider, Marius Potassco: the Potsdam answer set solving collection. (English) Zbl 1215.68214 AI Commun. 24, No. 2, 107-124 (2011). MSC: 68T20 68N17 PDFBibTeX XMLCite \textit{M. Gebser} et al., AI Commun. 24, No. 2, 107--124 (2011; Zbl 1215.68214) Full Text: Link
Pipatsrisawat, Knot; Darwiche, Adnan On the power of clause-learning SAT solvers as resolution engines. (English) Zbl 1216.68235 Artif. Intell. 175, No. 2, 512-525 (2011). MSC: 68T15 68T05 PDFBibTeX XMLCite \textit{K. Pipatsrisawat} and \textit{A. Darwiche}, Artif. Intell. 175, No. 2, 512--525 (2011; Zbl 1216.68235) Full Text: DOI
Abío, Ignasi; Deters, Morgan; Nieuwenhuis, Robert; Stuckey, Peter J. Reducing chaos in SAT-like search: finding solutions close to a given one. (English) Zbl 1330.68266 Sakallah, Karem A. (ed.) et al., Theory and applications of satisfiability testing – SAT 2011. 14th international conference, SAT 2011, Ann Arbor, MI, USA, June 19–22, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-21580-3/pbk). Lecture Notes in Computer Science 6695, 273-286 (2011). MSC: 68T20 68Q25 PDFBibTeX XMLCite \textit{I. Abío} et al., Lect. Notes Comput. Sci. 6695, 273--286 (2011; Zbl 1330.68266) Full Text: DOI
Aschinger, Markus; Drescher, Conrad; Friedrich, Gerhard; Gottlob, Georg; Jeavons, Peter; Ryabokon, Anna; Thorstensen, Evgenij Optimization methods for the partner units problem. (English) Zbl 1302.90164 Achterberg, Tobias (ed.) et al., Integration of AI and OR techniques in constraint programming for combinatorial optimization problems. 8th international conference, CPAIOR 2011, Berlin, Germany, May 23–27, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-21310-6/pbk). Lecture Notes in Computer Science 6697, 4-19 (2011). MSC: 90C27 68T20 90C10 PDFBibTeX XMLCite \textit{M. Aschinger} et al., Lect. Notes Comput. Sci. 6697, 4--19 (2011; Zbl 1302.90164) Full Text: DOI
Atserias, A.; Fichte, J. K.; Thurley, M. Clause-learning algorithms with many restarts and bounded-width resolution. (English) Zbl 1214.68340 J. Artif. Intell. Res. (JAIR) 40, 353-373 (2011). MSC: 68T20 68T05 68T15 PDFBibTeX XMLCite \textit{A. Atserias} et al., J. Artif. Intell. Res. (JAIR) 40, 353--373 (2011; Zbl 1214.68340) Full Text: DOI
Ábrahám, Erika; Schubert, Tobias; Becker, Bernd; Fränzle, Martin; Herde, Christian Parallel SAT solving in bounded model checking. (English) Zbl 1213.68359 J. Log. Comput. 21, No. 1, 5-21 (2011). MSC: 68Q60 68T20 PDFBibTeX XMLCite \textit{E. Ábrahám} et al., J. Log. Comput. 21, No. 1, 5--21 (2011; Zbl 1213.68359) Full Text: DOI
Marić, Filip Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. (English) Zbl 1208.68205 Theor. Comput. Sci. 411, No. 50, 4333-4356 (2010). MSC: 68T20 68Q60 PDFBibTeX XMLCite \textit{F. Marić}, Theor. Comput. Sci. 411, No. 50, 4333--4356 (2010; Zbl 1208.68205) Full Text: DOI
Aloul, Fadi A.; Ramani, Arathi; Markov, Igor L.; Sakallah, Karem A. Dynamic symmetry-breaking for Boolean satisfiability. (English) Zbl 1205.68366 Ann. Math. Artif. Intell. 57, No. 1, 59-73 (2009). MSC: 68T20 90C05 PDFBibTeX XMLCite \textit{F. A. Aloul} et al., Ann. Math. Artif. Intell. 57, No. 1, 59--73 (2009; Zbl 1205.68366) Full Text: DOI
Sabharwal, Ashish SymChaff: Exploiting symmetry in a structure-aware satisfiability solver. (English) Zbl 1186.68442 Constraints 14, No. 4, 478-505 (2009). MSC: 68T20 PDFBibTeX XMLCite \textit{A. Sabharwal}, Constraints 14, No. 4, 478--505 (2009; Zbl 1186.68442) Full Text: DOI
Schubert, Tobias; Lewis, Matthew; Becker, Bernd PaMiraXT: parallel SAT solving with threads and message passing. (English) Zbl 1190.68057 J. Satisf. Boolean Model. Comput. 6, No. 4, 203-222 (2009). MSC: 68T20 68W10 PDFBibTeX XMLCite \textit{T. Schubert} et al., J. Satisf. Boolean Model. Comput. 6, No. 4, 203--222 (2009; Zbl 1190.68057)
Gershman, Roman; Strichman, Ofer HaifaSat: a SAT solver based on an abstraction/refinement model. (English) Zbl 1187.68541 J. Satisf. Boolean Model. Comput. 6, No. 1-3, 33-51 (2009). MSC: 68T20 PDFBibTeX XMLCite \textit{R. Gershman} and \textit{O. Strichman}, J. Satisf. Boolean Model. Comput. 6, No. 1--3, 33--51 (2009; Zbl 1187.68541)
Marić, Filip Formalization and implementation of modern SAT solvers. (English) Zbl 1187.68557 J. Autom. Reasoning 43, No. 1, 81-119 (2009). MSC: 68T20 68T15 68Q60 PDFBibTeX XMLCite \textit{F. Marić}, J. Autom. Reasoning 43, No. 1, 81--119 (2009; Zbl 1187.68557) Full Text: DOI
Järvisalo, Matti; Junttila, Tommi Limitations of restricted branching in clause learning. (English) Zbl 1192.68643 Constraints 14, No. 3, 325-356 (2009). MSC: 68T20 PDFBibTeX XMLCite \textit{M. Järvisalo} and \textit{T. Junttila}, Constraints 14, No. 3, 325--356 (2009; Zbl 1192.68643) Full Text: DOI
Goldberg, Eugene Boundary points and resolution. (English) Zbl 1247.68234 Kullmann, Oliver (ed.), Theory and applications of satisfiability testing – SAT 2009. 12th international conference, SAT 2009, Swansea, UK, June 30–July 3, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02776-5/pbk). Lecture Notes in Computer Science 5584, 147-160 (2009). MSC: 68T15 PDFBibTeX XMLCite \textit{E. Goldberg}, Lect. Notes Comput. Sci. 5584, 147--160 (2009; Zbl 1247.68234) Full Text: DOI
Atserias, Albert; Fichte, Johannes Klaus; Thurley, Marc Clause-learning algorithms with many restarts and bounded-width resolution. (English) Zbl 1247.68245 Kullmann, Oliver (ed.), Theory and applications of satisfiability testing – SAT 2009. 12th international conference, SAT 2009, Swansea, UK, June 30–July 3, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02776-5/pbk). Lecture Notes in Computer Science 5584, 114-127 (2009). MSC: 68T20 68T05 68T15 PDFBibTeX XMLCite \textit{A. Atserias} et al., Lect. Notes Comput. Sci. 5584, 114--127 (2009; Zbl 1247.68245) Full Text: DOI arXiv
Drechsler, R.; Eggersglüß, S.; Fey, G.; Tille, D. Test pattern generation using Boolean proof engines. (English) Zbl 1189.68029 Dordrecht: Springer (ISBN 978-90-481-2359-9/hbk; 978-90-481-2360-5/ebook). xii, 192 p. (2009). MSC: 68M99 68-02 68U07 68T20 PDFBibTeX XMLCite \textit{R. Drechsler} et al., Test pattern generation using Boolean proof engines. Dordrecht: Springer (2009; Zbl 1189.68029) Full Text: DOI
Goldberg, Eugene A resolution based SAT-solver operating on complete assignments. (English) Zbl 1172.68618 J. Satisf. Boolean Model. Comput. 5, No. 1-4, 217-242 (2009). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{E. Goldberg}, J. Satisf. Boolean Model. Comput. 5, No. 1--4, 217--242 (2009; Zbl 1172.68618)
Carvalho, Alda; Crato, Nuno; Gomes, Carla A generative power-law search tree model. (English) Zbl 1179.90173 Comput. Oper. Res. 36, No. 8, 2376-2386 (2009). MSC: 90B40 68T99 PDFBibTeX XMLCite \textit{A. Carvalho} et al., Comput. Oper. Res. 36, No. 8, 2376--2386 (2009; Zbl 1179.90173) Full Text: DOI
Baumgartner, Peter; Tinelli, Cesare The model evolution calculus as a first-order DPLL method. (English) Zbl 1182.03034 Artif. Intell. 172, No. 4-5, 591-632 (2008). MSC: 03B35 68T15 68T20 PDFBibTeX XMLCite \textit{P. Baumgartner} and \textit{C. Tinelli}, Artif. Intell. 172, No. 4--5, 591--632 (2008; Zbl 1182.03034) Full Text: DOI
Mouhoub, Malek Systematic versus local search and GA techniques for incremental SAT. (English) Zbl 1178.68543 Int. J. Comput. Intell. Appl. 7, No. 1, 77-96 (2008). MSC: 68T20 68Q17 68Q25 68W25 PDFBibTeX XMLCite \textit{M. Mouhoub}, Int. J. Comput. Intell. Appl. 7, No. 1, 77--96 (2008; Zbl 1178.68543) Full Text: DOI
Biere, Armin PicoSAT essentials. (English) Zbl 1159.68403 J. Satisf. Boolean Model. Comput. 4, No. 2-4, 75-97 (2008). MSC: 68P05 68T20 PDFBibTeX XMLCite \textit{A. Biere}, J. Satisf. Boolean Model. Comput. 4, No. 2--4, 75--97 (2008; Zbl 1159.68403)
Asín, Roberto; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric Efficient generation of unsatisfiability proofs and cores in SAT. (English) Zbl 1182.68215 Cervesato, Iliano (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 15th international conference, LPAR 2008, Doha, Qatar, November 22–27, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-89438-4/pbk). Lecture Notes in Computer Science 5330. Lecture Notes in Artificial Intelligence, 16-30 (2008). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{R. Asín} et al., Lect. Notes Comput. Sci. 5330, 16--30 (2008; Zbl 1182.68215) Full Text: DOI
Järvisalo, Matti; Niemelä, Ilkka The effect of structural branching on the efficiency of clause learning SAT solving: An experimental study. (English) Zbl 1162.68655 J. Algorithms 63, No. 1-3, 90-113 (2008). MSC: 68T20 PDFBibTeX XMLCite \textit{M. Järvisalo} and \textit{I. Niemelä}, J. Algorithms 63, No. 1--3, 90--113 (2008; Zbl 1162.68655) Full Text: DOI
Maratea, Marco; Ricca, Francesco; Faber, Wolfgang; Leone, Nicola Look-back techniques and heuristics in DLV: Implementation, evaluation, and comparison to QBF solvers. (English) Zbl 1162.68668 J. Algorithms 63, No. 1-3, 70-89 (2008). MSC: 68T30 PDFBibTeX XMLCite \textit{M. Maratea} et al., J. Algorithms 63, No. 1--3, 70--89 (2008; Zbl 1162.68668) Full Text: DOI
Bruni, Renato; Santori, Andrea New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability. (English) Zbl 1140.68492 Discrete Optim. 5, No. 3, 569-583 (2008). MSC: 68T20 PDFBibTeX XMLCite \textit{R. Bruni} and \textit{A. Santori}, Discrete Optim. 5, No. 3, 569--583 (2008; Zbl 1140.68492) Full Text: DOI
Letombe, Florian; Marques-Silva, Joao Improvements to hybrid incremental SAT algorithms. (English) Zbl 1138.68544 Kleine Büning, Hans (ed.) et al., Theory and applications of satisfiability testing – SAT 2008. 11th international conference, SAT 2008, Guangzhou, China, May 12–15, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-79718-0/pbk). Lecture Notes in Computer Science 4996, 168-181 (2008). MSC: 68T20 PDFBibTeX XMLCite \textit{F. Letombe} and \textit{J. Marques-Silva}, Lect. Notes Comput. Sci. 4996, 168--181 (2008; Zbl 1138.68544) Full Text: DOI Link
Goldberg, Eugene A decision-making procedure for resolution-based SAT-solvers. (English) Zbl 1138.68539 Kleine Büning, Hans (ed.) et al., Theory and applications of satisfiability testing – SAT 2008. 11th international conference, SAT 2008, Guangzhou, China, May 12–15, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-79718-0/pbk). Lecture Notes in Computer Science 4996, 119-132 (2008). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{E. Goldberg}, Lect. Notes Comput. Sci. 4996, 119--132 (2008; Zbl 1138.68539) Full Text: DOI
Marques-Silva, Joao; Lynce, Inês Towards robust CNF encodings of cardinality constraints. (English) Zbl 1145.68525 Bessière, Christian (ed.), Principles and practice of constraint programming – CP 2007. 13th international conference, CP 2007, Providence, RI, USA, September 23–27, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-74969-1/pbk). Lecture Notes in Computer Science 4741, 483-497 (2007). MSC: 68T20 PDFBibTeX XMLCite \textit{J. Marques-Silva} and \textit{I. Lynce}, Lect. Notes Comput. Sci. 4741, 483--497 (2007; Zbl 1145.68525) Full Text: DOI Link
Faber, Wolfgang; Leone, Nicola; Pfeifer, Gerald; Ricca, Francesco On look-ahead heuristics in disjunctive logic programming. (English) Zbl 1138.68018 Ann. Math. Artif. Intell. 51, No. 2-4, 229-266 (2007). MSC: 68N17 68T27 68T20 PDFBibTeX XMLCite \textit{W. Faber} et al., Ann. Math. Artif. Intell. 51, No. 2--4, 229--266 (2007; Zbl 1138.68018) Full Text: DOI
Jing, Minge; Zhou, Dian; Tang, Pushan; Zhou, Xiaofang; Zhang, Hua Solving SAT problem by heuristic polarity decision-making algorithm. (English) Zbl 1142.68514 Sci. China, Ser. F. 50, No. 6, 915-925 (2007). MSC: 68T20 68T35 PDFBibTeX XMLCite \textit{M. Jing} et al., Sci. China, Ser. F 50, No. 6, 915--925 (2007; Zbl 1142.68514) Full Text: DOI
Sinz, Carsten Visualizing SAT instances and runs of the DPLL algorithm. (English) Zbl 1129.68502 J. Autom. Reasoning 39, No. 2, 219-243 (2007). MSC: 68T15 68T20 PDFBibTeX XMLCite \textit{C. Sinz}, J. Autom. Reasoning 39, No. 2, 219--243 (2007; Zbl 1129.68502) Full Text: DOI
Faber, Wolfgang; Leone, Nicola; Maratea, Marco; Ricca, Francesco Experimenting with look-back heuristics for hard ASP programs. (English) Zbl 1149.68330 Baral, Chitta (ed.) et al., Logic programming and nonmonotonic reasoning. 9th international conference, LPNMR 2007, Tempe, AZ, USA, May 15–17, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72199-4/pbk). Lecture Notes in Computer Science 4483. Lecture Notes in Artificial Intelligence, 110-122 (2007). MSC: 68N17 68T15 68T20 PDFBibTeX XMLCite \textit{W. Faber} et al., Lect. Notes Comput. Sci. 4483, 110--122 (2007; Zbl 1149.68330) Full Text: DOI
Liu, Lengning; Truszczyński, Mirosław Satisfiability testing of Boolean combinations of pseudo-Boolean constraints using local-search techniques. (English) Zbl 1211.68386 Constraints 12, No. 3, 345-369 (2007). MSC: 68T20 03B70 PDFBibTeX XMLCite \textit{L. Liu} and \textit{M. Truszczyński}, Constraints 12, No. 3, 345--369 (2007; Zbl 1211.68386) Full Text: DOI
Condrat, Christopher; Kalla, Priyank A Gröbner basis approach to CNF-formulae preprocessing. (English) Zbl 1186.68576 Grumberg, Orna (ed.) et al., Tools and algorithms for the construction and analysis of systems. 13th international conference, TACAS 2007, held as part of the joint European conferences on theory and practice of software, ETAPS 2007, Braga, Portugal, March 24 – April 1, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-71208-4/pbk). Lecture Notes in Computer Science 4424, 618-631 (2007). MSC: 68W30 68T15 68T20 PDFBibTeX XMLCite \textit{C. Condrat} and \textit{P. Kalla}, Lect. Notes Comput. Sci. 4424, 618--631 (2007; Zbl 1186.68576) Full Text: DOI
Lynce, I.; Marques-Silva, J. Random backtracking in backtrack search algorithms for satisfiability. (English) Zbl 1121.68109 Discrete Appl. Math. 155, No. 12, 1604-1612 (2007). MSC: 68T20 68P10 68W20 PDFBibTeX XMLCite \textit{I. Lynce} and \textit{J. Marques-Silva}, Discrete Appl. Math. 155, No. 12, 1604--1612 (2007; Zbl 1121.68109) Full Text: DOI Link
Goldberg, Eugene; Novikov, Yakov BerkMin: A fast and robust SAT-solver. (English) Zbl 1121.68106 Discrete Appl. Math. 155, No. 12, 1549-1561 (2007). MSC: 68T20 PDFBibTeX XMLCite \textit{E. Goldberg} and \textit{Y. Novikov}, Discrete Appl. Math. 155, No. 12, 1549--1561 (2007; Zbl 1121.68106) Full Text: DOI
Ramani, A.; Markov, I. L.; Sakallah, K. A.; Aloul, F. A. Breaking instance-independent symmetries in exact graph coloring. (English) Zbl 1182.68152 J. Artif. Intell. Res. (JAIR) 26, 289-322 (2006). MSC: 68R10 68T20 PDFBibTeX XMLCite \textit{A. Ramani} et al., J. Artif. Intell. Res. (JAIR) 26, 289--322 (2006; Zbl 1182.68152) Full Text: arXiv
Paris, Lionel; Benhamou, Belaïd; Siegel, Pierre A Boolean encoding including SAT and \(n\)-ary CSPs. (English) Zbl 1158.68496 Euzenat, Jérôme (ed.) et al., Artificial intelligence: Methodology, systems, and applications. 12th international conference, AIMSA 2006, Varna, Bulgaria, September 12–15, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-40930-4/pbk). Lecture Notes in Computer Science 4183. Lecture Notes in Artificial Intelligence, 33-44 (2006). MSC: 68T20 68T27 68T30 PDFBibTeX XMLCite \textit{L. Paris} et al., Lect. Notes Comput. Sci. 4183, 33--44 (2006; Zbl 1158.68496) Full Text: DOI
Fränzle, Martin; Herde, Christian; Teige, Tino; Ratschan, Stefan; Schubert, Tobias Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. (English) Zbl 1144.68371 J. Satisf. Boolean Model. Comput. 1, No. 3-4, 209-236 (2006). MSC: 68T20 PDFBibTeX XMLCite \textit{M. Fränzle} et al., J. Satisf. Boolean Model. Comput. 1, No. 3--4, 209--236 (2006; Zbl 1144.68371)
Nguyen, Hung Son Approximate Boolean reasoning: Foundations and applications in data mining. (English) Zbl 1136.68497 Peters, James F. (ed.) et al., Transactions on Rough Sets V. Berlin: Springer (ISBN 978-3-540-39382-5/pbk). Lecture Notes in Computer Science 4100. Journal Subline, 334-506 (2006). MSC: 68T05 68T37 PDFBibTeX XMLCite \textit{H. S. Nguyen}, Lect. Notes Comput. Sci. 4100, 334--506 (2006; Zbl 1136.68497) Full Text: DOI
Aloul, Fadi A. Search techniques for SAT-based Boolean optimization. (English) Zbl 1177.90294 J. Franklin Inst. 343, No. 4-5, 436-447 (2006). MSC: 90C10 90C05 68T20 PDFBibTeX XMLCite \textit{F. A. Aloul}, J. Franklin Inst. 343, No. 4--5, 436--447 (2006; Zbl 1177.90294) Full Text: DOI
Goldberg, Eugene Determinization of resolution by an algorithm operating on complete assignments. (English) Zbl 1187.68543 Biere, Armin (ed.) et al., Theory and applications of satisfiability testing – SAT 2006. 9th international conference, Seattle, WA, USA, August 12–15, 2006. Proceedings. Berlin: Springer (ISBN 3-540-37206-7/pbk). Lecture Notes in Computer Science 4121, 90-95 (2006). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{E. Goldberg}, Lect. Notes Comput. Sci. 4121, 90--95 (2006; Zbl 1187.68543) Full Text: DOI
Dershowitz, Nachum; Hanna, Ziyad; Nadel, Alexander A scalable algorithm for minimal unsatisfiable core extraction. (English) Zbl 1187.68538 Biere, Armin (ed.) et al., Theory and applications of satisfiability testing – SAT 2006. 9th international conference, Seattle, WA, USA, August 12–15, 2006. Proceedings. Berlin: Springer (ISBN 3-540-37206-7/pbk). Lecture Notes in Computer Science 4121, 36-41 (2006). MSC: 68T20 68Q60 PDFBibTeX XMLCite \textit{N. Dershowitz} et al., Lect. Notes Comput. Sci. 4121, 36--41 (2006; Zbl 1187.68538) Full Text: DOI arXiv
Mironov, Ilya; Zhang, Lintao Applications of SAT solvers to cryptanalysis of hash functions. (English) Zbl 1187.94028 Biere, Armin (ed.) et al., Theory and applications of satisfiability testing – SAT 2006. 9th international conference, Seattle, WA, USA, August 12–15, 2006. Proceedings. Berlin: Springer (ISBN 3-540-37206-7/pbk). Lecture Notes in Computer Science 4121, 102-115 (2006). MSC: 94A60 68T20 PDFBibTeX XMLCite \textit{I. Mironov} and \textit{L. Zhang}, Lect. Notes Comput. Sci. 4121, 102--115 (2006; Zbl 1187.94028) Full Text: DOI
Cotton, Scott; Maler, Oded Fast and flexible difference constraint propagation for DPLL(T). (English) Zbl 1187.68537 Biere, Armin (ed.) et al., Theory and applications of satisfiability testing – SAT 2006. 9th international conference, Seattle, WA, USA, August 12–15, 2006. Proceedings. Berlin: Springer (ISBN 3-540-37206-7/pbk). Lecture Notes in Computer Science 4121, 170-183 (2006). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{S. Cotton} and \textit{O. Maler}, Lect. Notes Comput. Sci. 4121, 170--183 (2006; Zbl 1187.68537) Full Text: DOI
Jain, Himanshu; Bartzis, Constantinos; Clarke, Edmund Satisfiability checking of non-clausal formulas using general matings. (English) Zbl 1187.68549 Biere, Armin (ed.) et al., Theory and applications of satisfiability testing – SAT 2006. 9th international conference, Seattle, WA, USA, August 12–15, 2006. Proceedings. Berlin: Springer (ISBN 3-540-37206-7/pbk). Lecture Notes in Computer Science 4121, 75-89 (2006). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{H. Jain} et al., Lect. Notes Comput. Sci. 4121, 75--89 (2006; Zbl 1187.68549) Full Text: DOI
Jussila, Toni; Sinz, Carsten; Biere, Armin Extended resolution proofs for symbolic SAT solving with quantification. (English) Zbl 1187.68550 Biere, Armin (ed.) et al., Theory and applications of satisfiability testing – SAT 2006. 9th international conference, Seattle, WA, USA, August 12–15, 2006. Proceedings. Berlin: Springer (ISBN 3-540-37206-7/pbk). Lecture Notes in Computer Science 4121, 54-60 (2006). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{T. Jussila} et al., Lect. Notes Comput. Sci. 4121, 54--60 (2006; Zbl 1187.68550) Full Text: DOI
Fu, Zhaohui; Malik, Sharad On solving the partial MAX-SAT problem. (English) Zbl 1187.68540 Biere, Armin (ed.) et al., Theory and applications of satisfiability testing – SAT 2006. 9th international conference, Seattle, WA, USA, August 12–15, 2006. Proceedings. Berlin: Springer (ISBN 3-540-37206-7/pbk). Lecture Notes in Computer Science 4121, 252-265 (2006). MSC: 68T20 PDFBibTeX XMLCite \textit{Z. Fu} and \textit{S. Malik}, Lect. Notes Comput. Sci. 4121, 252--265 (2006; Zbl 1187.68540) Full Text: DOI
Bailleux, Olivier; Marquis, Pierre Some computational aspects of DISTANCE SAT. (English) Zbl 1113.68096 J. Autom. Reasoning 37, No. 4, 231-260 (2006). MSC: 68T20 68Q25 68T15 03B05 PDFBibTeX XMLCite \textit{O. Bailleux} and \textit{P. Marquis}, J. Autom. Reasoning 37, No. 4, 231--260 (2006; Zbl 1113.68096) Full Text: DOI
Sinz, Carsten; Biere, Armin Extended resolution proofs for conjoining BDDs. (English) Zbl 1185.68635 Grigoriev, Dima (ed.) et al., Computer science – theory and applications. First international computer science symposium in Russia, CSR 2006, St. Petersburg, Russia, June 8–12, 2006. Proceedings. Berlin: Springer (ISBN 3-540-34166-8/pbk). Lecture Notes in Computer Science 3967, 600-611 (2006). MSC: 68T15 PDFBibTeX XMLCite \textit{C. Sinz} and \textit{A. Biere}, Lect. Notes Comput. Sci. 3967, 600--611 (2006; Zbl 1185.68635) Full Text: DOI
Cimatti, Alessandro; Sebastiani, Roberto Building efficient decision procedures on top of SAT solvers. (English) Zbl 1182.68114 Bernardo, Marco (ed.) et al., Formal methods for hardware verification. 6th international school on formal methods for the design of computer, communication, and software systems, SFM 2006, Bertinoro, Italy, May 22–27, 2006. Advanced lectures. Berlin: Springer (ISBN 3-540-34304-0/pbk). Lecture Notes in Computer Science 3965, 144-175 (2006). MSC: 68Q60 68T15 PDFBibTeX XMLCite \textit{A. Cimatti} and \textit{R. Sebastiani}, Lect. Notes Comput. Sci. 3965, 144--175 (2006; Zbl 1182.68114) Full Text: DOI
Biere, Armin; Sinz, Carsten Decomposing SAT problems into connected components. (English) Zbl 1116.68079 J. Satisf. Boolean Model. Comput. 2, No. 1-4, 201-208 (2006). MSC: 68T20 PDFBibTeX XMLCite \textit{A. Biere} and \textit{C. Sinz}, J. Satisf. Boolean Model. Comput. 2, No. 1--4, 201--208 (2006; Zbl 1116.68079)
Gershman, Roman; Strichman, Ofer HaifaSat: A new robust SAT solver. (English) Zbl 1176.68120 Ur, Shmuel (ed.) et al., Hardware and software verification and testing. First international Haifa verification conference, Haifa, Israel, November 13–16, 2005. Revised selected papers. Berlin: Springer (ISBN 3-540-32604-9/pbk). Lecture Notes in Computer Science 3875, 76-89 (2006). MSC: 68Q60 68T20 PDFBibTeX XMLCite \textit{R. Gershman} and \textit{O. Strichman}, Lect. Notes Comput. Sci. 3875, 76--89 (2006; Zbl 1176.68120) Full Text: DOI
Chrabakh, Wahid; Wolski, Rich GridSAT: Design and implementation of a computational grid application. (English) Zbl 1099.68503 J. Grid Comput. 4, No. 2, 177-193 (2006). MSC: 68M10 68T20 PDFBibTeX XML Full Text: DOI
Mitchell, David G. A SAT solver primer. (English) Zbl 1169.68444 Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 85, 112-132 (2005). MSC: 68Q25 03B35 68T20 PDFBibTeX XMLCite \textit{D. G. Mitchell}, Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 85, 112--132 (2005; Zbl 1169.68444)
Li, Chu Min; Manyà, Felip; Planes, Jordi Exploiting unit propagation to compute lower bounds in branch and bound max-SAT solvers. (English) Zbl 1153.68470 van Beek, Peter (ed.), Principles and practice of constraint programming – CP 2005. 11th international conference, CP 2005, Sitges, Spain, October 1–5, 2005. Proceedings. Berlin: Springer (ISBN 978-3-540-29238-8/pbk). Lecture Notes in Computer Science 3709, 403-414 (2005). MSC: 68T20 PDFBibTeX XMLCite \textit{C. M. Li} et al., Lect. Notes Comput. Sci. 3709, 403--414 (2005; Zbl 1153.68470) Full Text: DOI
Shen, Haiou; Zhang, Hantao Another complete local search method for SAT. (English) Zbl 1143.68592 Sutcliffe, Geoff (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2–6, 2005. Proceedings. Berlin: Springer (ISBN 978-3-540-30553-8/pbk). Lecture Notes in Computer Science 3835, 595-605 (2005). MSC: 68T20 PDFBibTeX XMLCite \textit{H. Shen} and \textit{H. Zhang}, Lect. Notes Comput. Sci. 3835, 595--605 (2005; Zbl 1143.68592) Full Text: DOI
Van Gelder, Allen Pool resolution and its relation to regular resolution and DPLL with clause learning. (English) Zbl 1143.68582 Sutcliffe, Geoff (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2–6, 2005. Proceedings. Berlin: Springer (ISBN 978-3-540-30553-8/pbk). Lecture Notes in Computer Science 3835, 580-594 (2005). MSC: 68T15 PDFBibTeX XMLCite \textit{A. Van Gelder}, Lect. Notes Comput. Sci. 3835, 580--594 (2005; Zbl 1143.68582) Full Text: DOI
Wang, Chao; Ivančić, Franjo; Ganai, Malay; Gupta, Aarti Deciding separation logic formulae by SAT and incremental negative cycle elimination. (English) Zbl 1143.68583 Sutcliffe, Geoff (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2–6, 2005. Proceedings. Berlin: Springer (ISBN 978-3-540-30553-8/pbk). Lecture Notes in Computer Science 3835, 322-336 (2005). MSC: 68T15 03B35 03B70 68Q60 PDFBibTeX XMLCite \textit{C. Wang} et al., Lect. Notes Comput. Sci. 3835, 322--336 (2005; Zbl 1143.68583) Full Text: DOI
Nieuwenhuis, Robert; Oliveras, Albert Decision procedures for SAT, SAT modulo theories and beyond. The BarcelogicTools. (English) Zbl 1143.68579 Sutcliffe, Geoff (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2–6, 2005. Proceedings. Berlin: Springer (ISBN 978-3-540-30553-8/pbk). Lecture Notes in Computer Science 3835, 23-46 (2005). MSC: 68T15 68Q60 PDFBibTeX XMLCite \textit{R. Nieuwenhuis} and \textit{A. Oliveras}, Lect. Notes Comput. Sci. 3835, 23--46 (2005; Zbl 1143.68579) Full Text: DOI
Bhalla, Ateet; Lynce, Inês; de Sousa, José T.; Marques-Silva, João Heuristic-based backtracking relaxation for propositional satisfiability. (English) Zbl 1109.68099 J. Autom. Reasoning 35, No. 1-3, 3-24 (2005). MSC: 68T20 68P10 68W05 PDFBibTeX XMLCite \textit{A. Bhalla} et al., J. Autom. Reasoning 35, No. 1--3, 3--24 (2005; Zbl 1109.68099) Full Text: DOI Link
Cenzer, Douglas; Remmel, Jeffrey B.; Marek, Victor W. Logic programming with infinite sets. (English) Zbl 1086.68126 Ann. Math. Artif. Intell. 44, No. 4, 309-339 (2005). MSC: 68T27 03B70 68T30 PDFBibTeX XMLCite \textit{D. Cenzer} et al., Ann. Math. Artif. Intell. 44, No. 4, 309--339 (2005; Zbl 1086.68126) Full Text: DOI
Tang, Daijue; Yu, Yinlei; Ranjan, Darsh; Malik, Sharad Analysis of search based algorithms for satisfiability of propositional and quantified Boolean formulas arising from circuit state space diameter problems. (English) Zbl 1122.68619 Hoos, Holger H. (ed.) et al., Theory and applications of satisfiability testing. 7th international conference, SAT 2004, Vancouver, BC, Canada, May 10–13, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-27829-X/pbk). Lecture Notes in Computer Science 3542, 292-305 (2005). MSC: 68T20 PDFBibTeX XMLCite \textit{D. Tang} et al., Lect. Notes Comput. Sci. 3542, 292--305 (2005; Zbl 1122.68619) Full Text: DOI
Subbarayan, Sathiamoorthy; Pradhan, Dhiraj K. NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. (English) Zbl 1122.68618 Hoos, Holger H. (ed.) et al., Theory and applications of satisfiability testing. 7th international conference, SAT 2004, Vancouver, BC, Canada, May 10–13, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-27829-X/pbk). Lecture Notes in Computer Science 3542, 276-291 (2005). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{S. Subbarayan} and \textit{D. K. Pradhan}, Lect. Notes Comput. Sci. 3542, 276--291 (2005; Zbl 1122.68618) Full Text: DOI
Porschen, Stefan; Speckenmeyer, Ewald Worst case bounds for some NP-complete modified Horn-SAT problems. (English) Zbl 1122.68614 Hoos, Holger H. (ed.) et al., Theory and applications of satisfiability testing. 7th international conference, SAT 2004, Vancouver, BC, Canada, May 10–13, 2004. Revised selected papers. Berlin: Springer (ISBN 3-540-27829-X/pbk). Lecture Notes in Computer Science 3542, 251-262 (2005). MSC: 68T20 68Q17 PDFBibTeX XMLCite \textit{S. Porschen} and \textit{E. Speckenmeyer}, Lect. Notes Comput. Sci. 3542, 251--262 (2005; Zbl 1122.68614) Full Text: DOI
Dershowitz, Nachum; Hanna, Ziyad; Nadel, Alexander A clause-based heuristic for SAT solvers. (English) Zbl 1128.68461 Bacchus, Fahiem (ed.) et al., Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-26276-8/pbk). Lecture Notes in Computer Science 3569, 46-60 (2005). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{N. Dershowitz} et al., Lect. Notes Comput. Sci. 3569, 46--60 (2005; Zbl 1128.68461) Full Text: DOI
Lewis, Matthew D. T.; Schubert, Tobias; Becker, Bernd W. Speedup techniques utilized in modern SAT solvers – an analysis in the MIRA environment. (English) Zbl 1128.68471 Bacchus, Fahiem (ed.) et al., Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-26276-8/pbk). Lecture Notes in Computer Science 3569, 437-443 (2005). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{M. D. T. Lewis} et al., Lect. Notes Comput. Sci. 3569, 437--443 (2005; Zbl 1128.68471) Full Text: DOI
Gershman, Roman; Strichman, Ofer Cost-effective hyper-resolution for preprocessing CNF formulas. (English) Zbl 1128.68465 Bacchus, Fahiem (ed.) et al., Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-26276-8/pbk). Lecture Notes in Computer Science 3569, 423-429 (2005). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{R. Gershman} and \textit{O. Strichman}, Lect. Notes Comput. Sci. 3569, 423--429 (2005; Zbl 1128.68465) Full Text: DOI
Durairaj, Vijay; Kalla, Priyank Variable ordering for efficient SAT search by analyzing constraint-variable dependencies. (English) Zbl 1128.68462 Bacchus, Fahiem (ed.) et al., Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-26276-8/pbk). Lecture Notes in Computer Science 3569, 415-422 (2005). MSC: 68T20 PDFBibTeX XMLCite \textit{V. Durairaj} and \textit{P. Kalla}, Lect. Notes Comput. Sci. 3569, 415--422 (2005; Zbl 1128.68462) Full Text: DOI
Zarpas, Emmanuel Benchmarking SAT solvers for bounded model checking. (English) Zbl 1128.68368 Bacchus, Fahiem (ed.) et al., Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-26276-8/pbk). Lecture Notes in Computer Science 3569, 340-354 (2005). MSC: 68Q60 68T20 PDFBibTeX XMLCite \textit{E. Zarpas}, Lect. Notes Comput. Sci. 3569, 340--354 (2005; Zbl 1128.68368) Full Text: DOI
Sang, Tian; Beame, Paul; Kautz, Henry Heuristics for fast exact model counting. (English) Zbl 1128.68481 Bacchus, Fahiem (ed.) et al., Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-26276-8/pbk). Lecture Notes in Computer Science 3569, 226-240 (2005). MSC: 68T20 PDFBibTeX XMLCite \textit{T. Sang} et al., Lect. Notes Comput. Sci. 3569, 226--240 (2005; Zbl 1128.68481) Full Text: DOI
Prestwich, Steven Random walk with continuously smoothed variable weights. (English) Zbl 1128.68478 Bacchus, Fahiem (ed.) et al., Theory and applications of satisfiability testing. 8th international conference, SAT 2005, St Andrews, UK, June 19–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-26276-8/pbk). Lecture Notes in Computer Science 3569, 203-215 (2005). MSC: 68T20 PDFBibTeX XMLCite \textit{S. Prestwich}, Lect. Notes Comput. Sci. 3569, 203--215 (2005; Zbl 1128.68478) Full Text: DOI
Jin, HoonSang; Han, HyoJung; Somenzi, Fabio Efficient conflict analysis for finding all satisfying assignments of a Boolean circuit. (English) Zbl 1087.68631 Halbwachs, Nicolas (ed.) et al., Tools and algorithms for the construction and analysis of systems. 11th international conference, TACAS 2005, held as part of the joint European conference on theory and practice of software, ETAPS 2005, Edinburgh, UK, April 4–8, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25333-5/pbk). Lecture Notes in Computer Science 3440, 287-300 (2005). MSC: 68T15 68T20 94C10 PDFBibTeX XMLCite \textit{H. Jin} et al., Lect. Notes Comput. Sci. 3440, 287--300 (2005; Zbl 1087.68631) Full Text: DOI
Dahllöf, Vilhelm Applications of general exact satisfiability in propositional logic modelling. (English) Zbl 1108.68571 Baader, Franz (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14–18, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25236-3/pbk). Lecture Notes in Computer Science 3452. Lecture Notes in Artificial Intelligence, 95-109 (2005). MSC: 68T15 68Q25 PDFBibTeX XMLCite \textit{V. Dahllöf}, Lect. Notes Comput. Sci. 3452, 95--109 (2005; Zbl 1108.68571) Full Text: DOI
Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare Abstract DPLL and abstract DPLL modulo theories. (English) Zbl 1109.68097 Baader, Franz (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14–18, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25236-3/pbk). Lecture Notes in Computer Science 3452. Lecture Notes in Artificial Intelligence, 36-50 (2005). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{R. Nieuwenhuis} et al., Lect. Notes Comput. Sci. 3452, 36--50 (2005; Zbl 1109.68097) Full Text: DOI
Egly, Uwe; Pichler, Reinhard; Woltran, Stefan On deciding subsumption problems. (English) Zbl 1099.68095 Ann. Math. Artif. Intell. 43, No. 1-4, 255-294 (2005). MSC: 68T15 68T20 PDFBibTeX XMLCite \textit{U. Egly} et al., Ann. Math. Artif. Intell. 43, No. 1--4, 255--294 (2005; Zbl 1099.68095) Full Text: DOI
Prestwich, Steven; Bressan, Stéphane A SAT approach to query optimization in mediator systems. (English) Zbl 1099.68103 Ann. Math. Artif. Intell. 43, No. 1-4, 195-210 (2005). MSC: 68T20 68P15 PDFBibTeX XMLCite \textit{S. Prestwich} and \textit{S. Bressan}, Ann. Math. Artif. Intell. 43, No. 1--4, 195--210 (2005; Zbl 1099.68103) Full Text: DOI
Le Berre, Daniel; Simon, Laurent The essentials of the SAT 2003 competition. (English) Zbl 1204.68203 Giunchiglia, Enrico (ed.) et al., Theory and applications of satisfiability testing. 6th international conference, SAT 2003, Santa Margherita Ligure, Italy, May 5–8, 2003. Selected revised papers. Berlin: Springer (ISBN 3-540-20851-8/pbk). Lect. Notes Comput. Sci. 2919, 452-467 (2004). MSC: 68T20 PDFBibTeX XMLCite \textit{D. Le Berre} and \textit{L. Simon}, Lect. Notes Comput. Sci. 2919, 452--467 (2004; Zbl 1204.68203) Full Text: DOI
Franco, John; Kouril, Michal; Schlipf, John; Ward, Jeffrey; Weaver, Sean; Dransfield, Michael; Vanfleet, W. Mark SBSAT: a state-based, BDD-based satisfiability solver. (English) Zbl 1204.68193 Giunchiglia, Enrico (ed.) et al., Theory and applications of satisfiability testing. 6th international conference, SAT 2003, Santa Margherita Ligure, Italy, May 5–8, 2003. Selected revised papers. Berlin: Springer (ISBN 3-540-20851-8/pbk). Lect. Notes Comput. Sci. 2919, 398-410 (2004). MSC: 68T20 PDFBibTeX XMLCite \textit{J. Franco} et al., Lect. Notes Comput. Sci. 2919, 398--410 (2004; Zbl 1204.68193) Full Text: DOI
Zhang, Lintao; Malik, Sharad Cache performance of SAT solvers: a case study for efficient implementation of algorithms. (English) Zbl 1204.68213 Giunchiglia, Enrico (ed.) et al., Theory and applications of satisfiability testing. 6th international conference, SAT 2003, Santa Margherita Ligure, Italy, May 5–8, 2003. Selected revised papers. Berlin: Springer (ISBN 3-540-20851-8/pbk). Lect. Notes Comput. Sci. 2919, 287-298 (2004). MSC: 68T20 68P05 PDFBibTeX XMLCite \textit{L. Zhang} and \textit{S. Malik}, Lect. Notes Comput. Sci. 2919, 287--298 (2004; Zbl 1204.68213) Full Text: DOI
Khurshid, Sarfraz; Marinov, Darko; Shlyakhter, Ilya; Jackson, Daniel A case for efficient solution enumeration. (English) Zbl 1204.68180 Giunchiglia, Enrico (ed.) et al., Theory and applications of satisfiability testing. 6th international conference, SAT 2003, Santa Margherita Ligure, Italy, May 5–8, 2003. Selected revised papers. Berlin: Springer (ISBN 3-540-20851-8/pbk). Lect. Notes Comput. Sci. 2919, 272-286 (2004). MSC: 68T15 68Q25 68T20 PDFBibTeX XMLCite \textit{S. Khurshid} et al., Lect. Notes Comput. Sci. 2919, 272--286 (2004; Zbl 1204.68180) Full Text: DOI
Armando, Alessandro; Compagna, Luca Abstraction-driven SAT-based analysis of security protocols. (English) Zbl 1204.68031 Giunchiglia, Enrico (ed.) et al., Theory and applications of satisfiability testing. 6th international conference, SAT 2003, Santa Margherita Ligure, Italy, May 5–8, 2003. Selected revised papers. Berlin: Springer (ISBN 3-540-20851-8/pbk). Lect. Notes Comput. Sci. 2919, 257-271 (2004). MSC: 68M12 68Q60 68T20 PDFBibTeX XMLCite \textit{A. Armando} and \textit{L. Compagna}, Lect. Notes Comput. Sci. 2919, 257--271 (2004; Zbl 1204.68031) Full Text: DOI
Goldberg, Eugene; Novikov, Yakov How good can a resolution based SAT-solver be? (English) Zbl 1204.68196 Giunchiglia, Enrico (ed.) et al., Theory and applications of satisfiability testing. 6th international conference, SAT 2003, Santa Margherita Ligure, Italy, May 5–8, 2003. Selected revised papers. Berlin: Springer (ISBN 3-540-20851-8/pbk). Lect. Notes Comput. Sci. 2919, 37-52 (2004). MSC: 68T20 68T15 PDFBibTeX XMLCite \textit{E. Goldberg} and \textit{Y. Novikov}, Lect. Notes Comput. Sci. 2919, 37--52 (2004; Zbl 1204.68196) Full Text: DOI
Dransfield, Michael R.; Marek, Victor W.; Truszczyński, Mirosław Satisfiability and computing van der Waerden numbers. (English) Zbl 1204.05097 Giunchiglia, Enrico (ed.) et al., Theory and applications of satisfiability testing. 6th international conference, SAT 2003, Santa Margherita Ligure, Italy, May 5–8, 2003. Selected revised papers. Berlin: Springer (ISBN 3-540-20851-8/pbk). Lect. Notes Comput. Sci. 2919, 1-13 (2004). MSC: 05D10 03B35 68Q25 68T15 PDFBibTeX XMLCite \textit{M. R. Dransfield} et al., Lect. Notes Comput. Sci. 2919, 1--13 (2004; Zbl 1204.05097) Full Text: DOI
Giunchiglia, Enrico; Narizzano, Massimo; Tacchella, Armando Monotone literals and learning in QBF reasoning. (English) Zbl 1152.68554 Wallace, Mark (ed.), Principles and practice of constraint programming – CP 2004. 10th international conference, CP 2004, Toronto, Canada, September 27–October 1, 2004. Proceedings. Berlin: Springer (ISBN 978-3-540-23241-4/pbk). Lecture Notes in Computer Science 3258, 260-273 (2004). MSC: 68T20 68T05 PDFBibTeX XMLCite \textit{E. Giunchiglia} et al., Lect. Notes Comput. Sci. 3258, 260--273 (2004; Zbl 1152.68554) Full Text: DOI