Matti Järvisalo

Postdoctoral Researcher

Contact Information

Matti.Jarvisalo[at]cs.helsinki.fi
http://cs.helsinki.fi/matti.jarvisalo/
A312
(09) 191 51377

Principal Investigator of

Teaching

2013 spring
Seminar: Constraint Solving Meets Machine Learning and Data Mining
Seminar: Constraint Solving Meets Machine Learning and Data Mining
Seminar: Constraint Solving Meets Machine Learning and Data Mining

  • In charge

2012 spring
Discrete Optimization Project
Övningsarbete i diskret optimering
Diskreetin optimoinnin harjoitustyö

  • Lecturer , in charge

2011 autumn
Discrete Optimization
Diskret optimering
Diskreetti optimointi

  • Lecturer , in charge

2010 autumn
Seminar on Boolean Constraint Reasoning
Seminar on Boolean Constraint Reasoning
Seminar on Boolean Constraint Reasoning

  • In charge

Publications

Publications gathered from the TUHAT database profile.

2013

Formula Preprocessing in MUS Extraction

Belov, A. , Järvisalo, M. & Marques-Silva, J. 2013 p. 110-125.

Publication: Conference contribution › A4 Article in conference publication (refereed)

Revisiting Hyper Binary Resolution

Heule, M. , Järvisalo, M. & Biere, A. 2013

Publication: Conference contribution › A4 Article in conference publication (refereed)

2012

CEGARTIX: A SAT-Based Argumentation System

Dvorak, W. , Järvisalo, M. , Wallner, J. & Woltran, S. 2012

Publication: Conference contribution › A4 Article in conference publication (refereed)

Complexity-Sensitive Decision Procedures for Abstract Argumentation

Dvorak, W. , Järvisalo, M. , Wallner, J. & Woltran, S. 2012 11 p.

Publication: Conference contribution › A4 Article in conference publication (refereed)

Finding Efficient Circuits for Ensemble Computation

Järvisalo, M. , Kaski, P. , Koivisto, M. & Korhonen, J. H. 2012 p. 369-382. 14 p.

Publication: Conference contribution › A4 Article in conference publication (refereed)

Inprocessing Rules

Järvisalo, M. , Heule, M. & Biere, A. 2012 p. 355-370. 16 p.

Publication: Conference contribution › A4 Article in conference publication (refereed)

Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions

Balint, A. (ed.), Belov, A. (ed.), Diepold, D. (ed.), Gerber, S. (ed.), Järvisalo, M. (ed.) & Sinz, C. (ed.) 2012 Helsinki: University of Helsinki. 92 p. (Department of Computer Science Series of Publications B).

Publication: Book/anthology › C2 Edited book, compilation, conference proceeding or special issue of journal

Relating Proof Complexity Measures and Practical Hardness of SAT

Järvisalo, M. , Matsliah, A. , Nordström, J. & Zivny, S. 2012 p. 316-331. 16 p.

Publication: Conference contribution › A4 Article in conference publication (refereed)

Simulating Circuit-Level Simplifications on CNF

Järvisalo, M. , Biere, A. & Heule, M. 2012 In : Journal of Automated Reasoning. 49, 4, p. 583-619.

Publication: Contribution to journal › A1 Refereed journal article

The International SAT Solver Competitions

Järvisalo, M. , Le Berre, D. , Roussel, O. & Simon, L. 2012 In : AI Magazine. 33, 1, p. 89-92. 4 p.

Publication: Contribution to journal › B1 Unrefereed journal article

Weak Models of Distributed Computing, with Connections to Modal Logic

Hella, L. , Järvisalo, M. , Kuusisto, A. , Laurinharju, J. , Lempiäinen, T. , Luosto, K. , Suomela, J. & Virtema, J. 2012 p. 185–194. 10 p.

Publication: Conference contribution › A4 Article in conference publication (refereed)

2011

Depth-Driven Circuit-Level Stochastic Local Search for SAT

Belov, A. , Järvisalo, M. & Stachniak, Z. 2011 p. 504-509. 6 p.

Publication: Conference contribution › A4 Article in conference publication (refereed)

Efficient CNF Simplification based on Binary Implication Graphs

Heule, M. J. H. , Järvisalo, M. & Biere, A. 2011 p. 201-215. 15 p.

Publication: Conference contribution › A4 Article in conference publication (refereed)

Itemset Mining as a Challenge Application for Answer Set Enumeration

Järvisalo, M. 2011 p. 304-310. 7 p.

Publication: Conference contribution › A4 Article in conference publication (refereed)

On the Relative Efficiency of DPLL and OBDDs with Axiom and Join

Järvisalo, M. 2011 p. 429-437. 9 p.

Publication: Conference contribution › A4 Article in conference publication (refereed)

Structure-Based Local Search Heuristics for Circuit-Level Boolean Satisfiability

Belov, A. & Järvisalo, M. 2011 p. 3-17. 15 p.

Publication: Conference contribution › A4 Article in conference publication (refereed)

2010

Blocked Clause Elimination

Järvisalo, M. , Biere, A. & Heule, M. 2010 p. 129-144. 15 p.

Publication: Conference contribution › A4 Article in conference publication (refereed)

Clause Elimination Procedures for CNF Formulas

Heule, M. , Järvisalo, M. & Biere, A. 2010 p. 357-371. 15 p.

Publication: Conference contribution › A4 Article in conference publication (refereed)

Covered Clause Elimination

Heule, M. , Järvisalo, M. & Biere, A. 2010

Publication: Conference contribution › A4 Article in conference publication (refereed)

Depth-Based Local Search Heuristics for Boolean Circuit Satisfiability

Belov, A. & Järvisalo, M. 2010 Helsinki, Finland: Helsinki Institute for Information Technology HIIT. 20 p. (HIIT Technical Reports).

Publication: Book/anthology › D4 Published development or research report

Reconstructing Solutions after Blocked Clause Elimination

Järvisalo, M. & Biere, A. 2010 p. 340-345. 6 p.

Publication: Conference contribution › A4 Article in conference publication (refereed)

Testing and Debugging Techniques for Answer Set Solver Development

Brummayer, R. & Järvisalo, M. 2010 In : Theory and Practice of Logic Programming. 10, 4-6, p. 741-758. 18 p.

Publication: Contribution to journal › A1 Refereed journal article