Search results

  • 2024

    SAT-Based Techniques for Lexicographically Smallest Finite Models

    Janota, M., Chow, C., Araújo, J., Codish, M. & Vojtěchovský, P., 25 Mar 2024, In: Proceedings of the AAAI Conference on Artificial Intelligence. 38, 8, p. 8048-8056 9 p.

    Research output: Contribution to journalConference articlepeer-review

    Open Access
    1 Scopus citations
  • 2023

    Breaking Symmetries with High Dimensional Graph Invariants and Their Combination

    Itzhakov, A. & Codish, M., 1 Jan 2023, Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 20th International Conference, CPAIOR 2023, Proceedings. Cire, A. A. (ed.). Springer Science and Business Media Deutschland GmbH, p. 133-149 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13884 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    3 Scopus citations
  • 2022

    Complete symmetry breaking constraints for the class of uniquely Hamiltonian graphs

    Itzhakov, A. & Codish, M., 1 Apr 2022, In: Constraints. 27, 1-2, p. 8-28 21 p.

    Research output: Contribution to journalArticlepeer-review

  • 2020

    Incremental symmetry breaking constraints for graph search problems

    Itzhakov, A. & Codish, M., 1 Jan 2020, AAAI 2020 - 34th AAAI Conference on Artificial Intelligence. AAAI press, p. 1536-1543 8 p. (AAAI 2020 - 34th AAAI Conference on Artificial Intelligence).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    4 Scopus citations
  • 2019

    Constraints for symmetry breaking in graph representation

    Codish, M., Miller, A., Prosser, P. & Stuckey, P. J., 15 Jan 2019, In: Constraints. 24, 1, p. 1-24 24 p.

    Research output: Contribution to journalArticlepeer-review

    Open Access
    24 Scopus citations
  • Sorting networks: To the end and back again

    Codish, M., Cruz-Filipe, L., Ehlers, T., Müller, M. & Schneider-Kamp, P., 1 Sep 2019, In: Journal of Computer and System Sciences. 104, p. 184-201 18 p.

    Research output: Contribution to journalArticlepeer-review

    Open Access
    13 Scopus citations
  • 2018

    A SAT Encoding for the n-Fractions Problem

    Codish, M., 2 Jul 2018.

    Research output: Working paper/PreprintPreprint

    40 Downloads (Pure)
  • Breaking symmetries with lex implications

    Codish, M., Ehlers, T., Gange, G., Itzhakov, A. & Stuckey, P. J., 1 Jan 2018, Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Proceedings. Gallagher, J. P., Sulzmann, M. & Gallagher, J. P. (eds.). Springer Verlag, p. 182-197 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10818 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    2 Scopus citations
  • Logic programming with max-clique and its application to graph coloring (tool description)

    Codish, M., Frank, M., Metodi, A. & Muslimany, M., 1 Feb 2018, Technical Communications of the 33rd International Conference on Logic Programming, ICLP 2017. Son, T. C., Mears, C., Rocha, R. & Saeedloei, N. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 5. (OpenAccess Series in Informatics; vol. 58).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    1 Scopus citations
  • SAT-based big-step local search

    Muslimany, M. & Codish, M., 1 Sep 2018, Proceedings - 2018 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2018. Institute of Electrical and Electronics Engineers, p. 109-116 8 p. 8750736. (Proceedings - 2018 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2018).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • 2017

    Optimal-depth sorting networks

    Bundala, D., Codish, M., Cruz-Filipe, L., Schneider-Kamp, P. & Závodný, J., 1 Mar 2017, In: Journal of Computer and System Sciences. 84, p. 185-204 20 p.

    Research output: Contribution to journalArticlepeer-review

    Open Access
    11 Scopus citations
  • Optimizing sorting algorithms by using sorting networks

    Codish, M., Cruz-Filipe, L., Nebel, M. & Schneider-Kamp, P., 1 May 2017, In: Formal Aspects of Computing. 29, 3, p. 559-579 21 p.

    Research output: Contribution to journalArticlepeer-review

    5 Scopus citations
  • The DNA word design problem: A new constraint model and new results

    Codish, M., Frank, M. & Lagoon, V., 1 Jan 2017, 26th International Joint Conference on Artificial Intelligence, IJCAI 2017. Sierra, C. (ed.). International Joint Conferences on Artificial Intelligence, p. 585-591 7 p. (IJCAI International Joint Conference on Artificial Intelligence; vol. 0).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    4 Scopus citations
  • 2016

    Breaking Symmetries in Graph Coloring Problems with Degree Matrices: the Ramsey Number R(4,3,3)=30?

    Codish, M., Frank, M., Itzhakov, A. & Miller, A., 14 Aug 2016.

    Research output: Working paper/PreprintWorking paper

  • Breaking symmetries in graphs: The nauty way

    Codish, M., Gange, G., Itzhakov, A. & Stuckey, P. J., 1 Jan 2016, Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Proceedings. Rueher, M. (ed.). Springer Verlag, p. 157-172 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9892 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    10 Scopus citations
  • Breaking symmetries in graph search with canonizing sets

    Itzhakov, A. & Codish, M., 1 Jul 2016, In: Constraints. 21, 3, p. 357-374 18 p.

    Research output: Contribution to journalArticlepeer-review

    11 Scopus citations
  • Computing the Ramsey number R(4,3,3) using abstraction and symmetry breaking

    Codish, M., Frank, M., Itzhakov, A. & Miller, A., 1 Jul 2016, In: Constraints. 21, 3, p. 375-393 19 p.

    Research output: Contribution to journalArticlepeer-review

    15 Scopus citations
  • Logic Programming with Graph Automorphism: Integrating nauty with Prolog (Tool Description)

    Frank, M. & Codish, M., 1 Sep 2016, In: Theory and Practice of Logic Programming. 16, 5-6, p. 688-702 15 p.

    Research output: Contribution to journalArticlepeer-review

    4 Scopus citations
  • Preface for special section from FLOPS 2014.

    Codish, M. & Sumii, E., 22 Jul 2016, Journal of Functional Programming, 26, 14, p. e14 1 p.

    Research output: Contribution to specialist publicationEditorial

  • Sorting nine inputs requires twenty-five comparisons

    Codish, M., Cruz-Filipe, L., Frank, M. & Schneider-Kamp, P., 1 Jan 2016, In: Journal of Computer and System Sciences. 82, 3, p. 551-563 13 p.

    Research output: Contribution to journalArticlepeer-review

    Open Access
    15 Scopus citations
  • 2015

    Applying sorting networks to synthesize optimized sorting libraries

    Codish, M., Cruz-Filipe, L., Nebel, M. & Schneider-Kamp, P., 1 Jan 2015, Logic-Based Program Synthesis and Transformation - 25th International Symposium, LOPSTR 2015, Revised Selected Papers. Falaschi, M. (ed.). Springer Verlag, p. 127-142 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9527).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    5 Scopus citations
  • Sorting networks: The end game

    Codish, M., Cruz-Filipe, L. & Schneider-Kamp, P., 1 Jan 2015, Language and Automata Theory and Applications - 9th International Conference, LATA 2015, Proceedings. Dediu, A.-H., Martín-Vide, C., Formenti, E. & Truthe, B. (eds.). Springer Verlag, p. 664-675 12 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8977).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    7 Scopus citations
  • The quest for optimal sorting networks: Efficient generation of two-layer prefixes

    Codish, M., Cruz-Filipe, L. & Schneider-Kamp, P., 5 Feb 2015, Proceedings - 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2014. Winkler, F., Negru, V., Ida, T., Jebelean, T., Petcu, D., Watt, S. M. & Zaharie, D. (eds.). Institute of Electrical and Electronics Engineers, p. 359-366 8 p. 7034705. (Proceedings - 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2014).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    11 Scopus citations
  • 2014

    A novel SAT-based approach to model based diagnosis

    Metodi, A., Stern, R., Kalech, M. & Codish, M., 14 Oct 2014, In: Journal Of Artificial Intelligence Research. 51, p. 377-411 35 p.

    Research output: Contribution to journalArticlepeer-review

    Open Access
    67 Scopus citations
  • Functional and Logic Programming: 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014. Proceedings

    Codish, M. (Editor) & Sumii, E. (Editor), Apr 2014, Springer Cham. 353 p. (Lecture Notes in Computer Science)

    Research output: Book/ReportBookpeer-review

  • Simplifying pseudo-boolean constraints in residual number systems

    Fekete, Y. & Codish, M., 1 Jan 2014, Theory and Applications of Satisfiability Testing, SAT 2014 - 17th International Conference, Held as Part of theVienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, p. 351-366 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8561 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    4 Scopus citations
  • Twenty-Five Comparators Is Optimal When Sorting Nine Inputs (and Twenty-Nine for Ten)

    Codish, M., Cruz-Filipe, L., Frank, M. & Schneider-Kamp, P., 12 Dec 2014, Proceedings - 2014 IEEE 26th International Conference on Tools with Artificial Intelligence, ICTAI 2014. Institute of Electrical and Electronics Engineers, p. 186-193 8 p. 6984472. (Proceedings - International Conference on Tools with Artificial Intelligence, ICTAI; vol. 2014-December).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    31 Scopus citations
  • 2013

    Backbones for equality

    Codish, M., Fekete, Y. & Metodi, A., 1 Jan 2013, Hardware and Software: Verification and Testing - 9th International Haifa Verification Conference, HVC 2013, Proceedings. Springer Verlag, p. 1-14 14 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8244 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    7 Scopus citations
  • Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems

    Metodi, A., Codish, M. & Stuckey, P. J., 1 Jan 2013, In: Journal Of Artificial Intelligence Research. 46, p. 303-341 39 p.

    Research output: Contribution to journalArticlepeer-review

    Open Access
    33 Scopus citations
  • Breaking symmetries in graph representation

    Codish, M., Miller, A., Prosser, P. & Stuckey, P. J., 1 Dec 2013, IJCAI 2013 - Proceedings of the 23rd International Joint Conference on Artificial Intelligence. p. 510-516 7 p. (IJCAI International Joint Conference on Artificial Intelligence).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    20 Scopus citations
  • Compiling finite domain constraints to SAT with BEE: The director's cut

    Codish, M., Fekete, Y. & Metodi, A., 1 Jan 2013.

    Research output: Contribution to conferencePaperpeer-review

  • 2012

    Compiling finite domain constraints to SAT with BEE*

    Metodi, A. & Codish, M., 1 Jul 2012, In: Theory and Practice of Logic Programming. 12, 4-5, p. 465-483 19 p.

    Research output: Contribution to journalArticlepeer-review

    Open Access
    38 Scopus citations
  • Compiling model-based diagnosis to Boolean satisfaction

    Metodi, A., Stern, R., Kalech, M. & Codish, M., 7 Nov 2012, AAAI-12 / IAAI-12 - Proceedings of the 26th AAAI Conference on Artificial Intelligence and the 24th Innovative Applications of Artificial Intelligence Conference. p. 793-799 7 p. (Proceedings of the National Conference on Artificial Intelligence; vol. 1).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    24 Scopus citations
  • Compiling Model-Based Diagnosis to Boolean Satisfaction

    Metodi, A., Stern, R., Kalech, M. & Codish, M., 1 Jan 2012, p. 793-799. 7 p.

    Research output: Contribution to conferencePaperpeer-review

    9 Scopus citations
  • Exotic Semi-Ring Constraints

    Codish, M., Fekete, Y., Fuhs, C., Giesl, J. & Waldmann, J., Dec 2012, p. 88-97. 10 p.

    Research output: Contribution to conferencePaperpeer-review

    Open Access
  • Programming with Boolean Satisfaction

    Codish, M., May 2012, Functional and Logic Programming : 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012, Proceedings. Springer Berlin Heidelberg, p. 1 1 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • SAT solving for termination proofs with recursive path orders and dependency pairs

    Codish, M., Giesl, J., Schneider-Kamp, P. & Thiemann, R., 1 Jun 2012, In: Journal of Automated Reasoning. 49, 1, p. 53-93 41 p.

    Research output: Contribution to journalArticlepeer-review

    Open Access
    17 Scopus citations
  • 2011

    Boolean equi-propagation for optimized SAT encoding

    Metodi, A., Codish, M., Lagoon, V. & Stuckey, P. J., 26 Sep 2011, Principles and Practice of Constraint Programming, CP 2011 - 17th International Conference, Proceedings. p. 621-636 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6876 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    16 Scopus citations
  • Optimal base encodings for Pseudo-Boolean constraints

    Codish, M., Fekete, Y., Fuhs, C. & Schneider-Kamp, P., 4 Apr 2011, Tools and Algorithms for the Construction and Analysis of Systems - 17th Int. Conf., TACAS 2011, Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2011, Proceedings. p. 189-204 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6605 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    11 Scopus citations
  • SAT-based termination analysis using monotonicity constraints over the integers

    Codish, M., Gonopolskiy, I., Ben-Amram, A. M., Fuhs, C. & Giesl, J., 1 Jul 2011, In: Theory and Practice of Logic Programming. 11, 4-5, p. 503-520 18 p.

    Research output: Contribution to journalArticlepeer-review

    Open Access
    7 Scopus citations
  • 2010

    Lazy abstraction for size-change termination

    Codish, M., Fuhs, C., Giesl, J. & Schneider-Kamp, P., 1 Jan 2010, Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings. Springer Verlag, p. 217-232 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6397 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    6 Scopus citations
  • Pairwise cardinality networks

    Codish, M. & Zazon-Ivry, M., 1 Dec 2010, Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Revised Selected Papers. p. 154-172 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6355 LNAI).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    38 Scopus citations
  • 2009

    A declarative encoding of telecommunications feature subscription in SAT

    Codish, M., Genaim, S. & Stuckey, P. J., 30 Nov 2009, PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming. p. 255-265 11 p. (PPDP'09 - Proceedings of the 11th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    6 Scopus citations
  • Propagation via lazy clause generation

    Ohrimenko, O., Stuckey, P. J. & Codish, M., 1 Sep 2009, In: Constraints. 14, 3, p. 357-391 35 p.

    Research output: Contribution to journalArticlepeer-review

    204 Scopus citations
  • 2008

    A SAT-based approach to size change termination with global ranking functions

    Ben-Amram, A. M. & Codish, M., 21 Jul 2008, Tools and Algorithms for the Construction and Analysis of Systems - 14th Int. Conf., TACAS 2008 - Held as Part of the Joint European Conf. Theory and Practice of Software, ETAPS 2008 Proceedings. p. 218-232 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4963 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    15 Scopus citations
  • Logic programming with satisfiability

    Codish, M., Lagoon, V. & Stuckey, P. J., 1 Jan 2008, In: Theory and Practice of Logic Programming. 8, 1, p. 121-128 8 p.

    Research output: Contribution to journalArticlepeer-review

    Open Access
    30 Scopus citations
  • Proving termination with (Boolean) satisfaction

    Codish, M., 1 Dec 2008, Logic-Based Program Synthesis and Transformation - 17th International Symposium, LOPSTR 2007, Revised Selected Papers. p. 1-7 7 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4915 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    3 Scopus citations
  • Telecommunications feature subscription as a partial order constraint problem

    Codish, M., Lagoon, V. & Stuckey, P. J., 1 Dec 2008, Logic Programming - 24th International Conference, ICLP 2008, Proceedings. p. 749-753 5 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5366 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    5 Scopus citations
  • Termination analysis of Java Bytecode

    Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G. & Zanardini, D., 4 Jul 2008, Formal Methods for Open Object-Based Distributed Systems - 10th IFIP WG 6.1 International Conference, FMOODS 2008, Proceedings. p. 2-18 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5051 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    41 Scopus citations
  • 2007

    Implementing RPO and POLO using SAT

    Fuhs, C., Schneider-Kamp, P., Thiemann, R., Giesl, J., Annov, E., Codish, M., Middeldorp, A. & Zankl, H., 1 Jan 2007, In: Dagstuhl Seminar Proceedings. 7401

    Research output: Contribution to journalConference articlepeer-review