Publications by Matti Järvisalo

[2013] [2012] [2011] [2010] [2009] [2008] [2007] [2006] [2005] [2004] [2001]

This list is also available sorted by type.

2013

• Theory and Applications of Satisfiability Testing - SAT 2013.
  Matti Järvisalo and Allen Van Gelder (editors).
  volume 7962 of Lecture Notes in Computer Science, Springer 2013 (forthcoming).
  [Book at Springer.com]
  
  
• Discovering Cyclic Causal Models with Latent Variables: A General SAT-Based Procedure.
  Antti Hyttinen, Patrik Hoyer, Frederick Eberhardt, and Matti Järvisalo.
  In ???, editors, Proceedings of the 29th Conference on Uncertainty in Artificial Intelligence (UAI 2013), pages ???-???, 2013 (to appear).
  [pdf] [abstract/bibtex]
  
  
• Formula Preprocessing in MUS Extraction.
  Anton Belov, Matti Järvisalo, and Joao Marques-Silva.
  In Nir Piterman and Scott Smolka, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), volume 7795 of Lecture Notes in Computer Science, pages 110-125. Springer, 2013.
  [doi:10.1007/978-3-642-36742-7_8] Preliminary version: [pdf] [abstract/bibtex]
  
  
• Revisiting Hyper Binary Resolution.
  Marijn Heule, Matti Järvisalo, and Armin Biere.
  In Carla Gomes and Meinolf Sellmann, editors, Proceedings of the 10th International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR 2013), volume 7874 of Lecture Notes in Computer Science, pages 77-93. Springer, 2013.
  [doi:10.1007/978-3-642-38171-3_6] Preliminary version: [pdf] [abstract/bibtex]
  
  
• Harnessing Constraint Programming for Poetry Composition.
  Jukka M. Toivanen, Matti Järvisalo, and Hannu Toivonen.
  In Mary Lou Maher, Tony Veale, Rob Saunders, and Oliver Bown, editors, Proceedings of the 4th International Conference on Computational Creativity (ICCC 2013), pages 160-167. The University of Sydney, 2013.
  [pdf] [abstract/bibtex]
  
  
• Covered Clause Elimination.
  Marijn Heule, Matti Järvisalo, and Armin Biere.
  In Andrei Voronkov, Geoff Sutcliffe, Matthias Baaz, and Christian Fermüller, editors, Short Paper Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-17 / 2010), volume 13 of EasyChair Proceedings in Computing, pages 41-46, 2013.
  Preliminary version: [arXiv:cs.LO/1011.5202] [pdf] [abstract/bibtex]
  
  
• Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions.
  Adrian Balint, Anton Belov, Marijn J.H. Heule, and Matti Järvisalo (editors),
  volume B-2013-1 of Department of Computer Science Series of Publications B, University of Helsinki, 2013. ISBN 978-952-10-8991-6. (forthcoming)
  

2012

• Simulating Circuit-Level Simplifications on CNF.
  Matti Järvisalo, Armin Biere, and Marijn Heule.
  Journal of Automated Reasoning 49(4):583-619, 2012.
  [doi:10.1007/s10817-011-9239-9] Preliminary version: [pdf] [abstract/bibtex]
  
  
• The International SAT Solver Competitions.
  Matti Järvisalo, Daniel Le Berre, Olivier Roussel, and Laurent Simon.
  AI Magazine 33(1):89-92, 2012.
  [Publisher's copy] Preliminary version: [pdf] [abstract/bibtex]
  
  
• Relating Proof Complexity Measures and Practical Hardness of SAT.
  Matti Järvisalo, Arie Matsliah, Jakob Nordström, and Stanislav Živný.
  In Michela Milano, editor, Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming (CP 2012), volume 7514 of Lecture Notes in Computer Science (LNCS), pages 316-331. Springer, 2012.
  [doi:10.1007/978-3-642-33558-7_25] Preliminary version: [pdf] [abstract/bibtex]
  
  
• Inprocessing Rules.
  Matti Järvisalo, Marijn Heule, and Armin Biere.
  In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR 2012), volume 7364 of Lecture Notes in Computer Science (LNCS/LNAI), pages 355-370. Springer, 2012.
  [doi:10.1007/978-3-642-31365-3_28] Preliminary version: [pdf] [abstract/bibtex]
  
  
• Complexity-Sensitive Decision Procedures for Abstract Argumentation.
  Wolfgang Dvořák, Matti Järvisalo, Johannes Peter Wallner, and Stefan Woltran.
  In Thomas Eiter and Sheila McIlraith, editors, Proceedings of the 13th International Conference on Principles of Knowledge Representation and Reasoning (KR 2012), pages 54-64. AAAI Press, 2012.
  [KR 2012 Distinguished Student Paper Prize]
  [Publisher's version] Local copy: [pdf] [abstract/bibtex]
  
  
• Finding Efficient Circuits for Ensemble Computation.
  Matti Järvisalo, Petteri Kaski, Mikko Koivisto, and Janne H. Korhonen.
  In Alessandro Cimatti and Roberto Sebastiani, editors, Proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing (SAT 2012), volume 7317 of Lecture Notes in Computer Science, pages 369-382. Springer, 2012.
  [doi:10.1007/978-3-642-31612-8_28] Preliminary version: [pdf] [abstract/bibtex]
  
  
• Weak Models of Distributed Computing, with Connections to Modal Logic.
  Lauri Hella, Matti Järvisalo, Antti Kuusisto, Juhana Laurinharju, Tuomo Lempiäinen, Kerkko Luosto, Jukka Suomela, and Jonni Virtema.
  In Darek Kowalski and Alessandro Panconesi, editors, Proceedings of the 31st Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC 2012), pages 185-194. ACM Press, 2012.
  [doi:10.1145/2332432.2332466] Preliminary version: [pdf] [abstract/bibtex] Preliminary extended version: [arXiv:cs.DC/1205.2051]
  
  
• Proceedings of SAT Challenge 2012: Solver and Benchmark Descriptions.
  Adrian Balint, Anton Belov, Daniel Diepold, Simon Gerber, Matti Järvisalo, and Carsten Sinz (editors),
  volume B-2012-2 of Department of Computer Science Series of Publications B, University of Helsinki, 2012. ISBN 978-952-10-8106-4.
  [handle:10138/34218] [bibtex]
  
  
• CEGARTIX: A SAT-Based Argumentation System.
  Wolfgang Dvořák, Matti Järvisalo, Johannes Peter Wallner, and Stefan Woltran.
  In 3rd Workshop on Pragmatics of SAT (PoS 2012), 2012.


• Finding Circuits for Ensemble Computation via Boolean Satisfiability.
  Matti Järvisalo, Petteri Kaski, Mikko Koivisto, and Janne H. Korhonen.
  In Adrian Balint, Anton Belov, Daniel Diepold, Simon Gerber, Matti Järvisalo, and Carsten Sinz, editors, Proceedings of SAT Challenge 2012, volume B-2012-2 of Department of Computer Science Series of Publications B, pages 79-81. University of Helsinki, 2012.
  [handle:10138/34218]


• Application and Hard Combinatorial Benchmarks in SAT Challenge 2012.
  Adrian Balint, Anton Belov, Matti Järvisalo, and Carsten Sinz.
  In Adrian Balint, Anton Belov, Daniel Diepold, Simon Gerber, Matti Järvisalo, and Carsten Sinz, editors, Proceedings of SAT Challenge 2012, volume B-2012-2 of Department of Computer Science Series of Publications B, pages 69-71. University of Helsinki, 2012.
  [handle:10138/34218]


• SAT Challenge 2012 Random SAT Track: Description of Benchmark Generation.
  Adrian Balint, Anton Belov, Matti Järvisalo, and Carsten Sinz.
  In Adrian Balint, Anton Belov, Daniel Diepold, Simon Gerber, Matti Järvisalo, and Carsten Sinz, editors, Proceedings of SAT Challenge 2012, volume B-2012-2 of Department of Computer Science Series of Publications B, pages 72-73. University of Helsinki, 2012.
  [handle:10138/34218]

2011

• On the Relative Efficiency of DPLL and OBDDs with Axiom and Join.
  Matti Järvisalo.
  In Jimmy Lee, editor, Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming (CP 2011), volume 6876 of Lecture Notes in Computer Science, pages 429-437. Springer, 2011.
  [doi:10.1007/978-3-642-23786-7_33] Preliminary version: [pdf] [abstract/bibtex]
  
  
• Depth-Driven Circuit-Level Stochastic Local Search for SAT.
  Anton Belov, Matti Järvisalo, and Zbigniew Stachniak.
  In Toby Walsh, editor, Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI 2011), pages 504-509. AAAI Press, 2011.
  [Publisher's copy] Preliminary version: [pdf] [abstract/bibtex]
  
  
• Efficient CNF Simplification based on Binary Implication Graphs.
  Marijn Heule, Matti Järvisalo, and Armin Biere.
  In Karem Sakallah and Laurent Simon, editors, Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing (SAT 2011), volume 6695 of Lecture Notes in Computer Science, pages 201-215. Springer, 2011.
  [doi:10.1007/978-3-642-21581-0_17] Preliminary version: [pdf] [abstract/bibtex]
  
  
• Itemset Mining as a Challenge Application for Answer Set Enumeration.
  Matti Järvisalo.
  In James Delgrande and Wolfgang Faber, editors, Proceedings of the 11th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2011), volume 6645 of Lecture Notes in Computer Science, pages 304-310. Springer, 2011.
  [doi:10.1007/978-3-642-20895-9_35] Preliminary version: [pdf] [abstract/bibtex]
  
  
• Structure-Based Local Search Heuristics for Circuit-Level Boolean Satisfiability.
  Anton Belov and Matti Järvisalo.
  In Laurent Michel and Steve Prestwich, editors, Proceedings of the 8th International Workshop on Local Search Techniques in Constraint Satisfaction (LSCS 2011), pages 3--17, 2011.
  Online version: [pdf] Local copy: [pdf] [abstract/bibtex]
  
  

2010

• Testing and Debugging Techniques for Answer Set Solver Development.
  Robert Brummayer and Matti Järvisalo.
  Theory and Practice of Logic Programming, 10(4-6):741-758, 2010.
  [doi:10.1017/S1471068410000396] Preliminary version: [arXiv:cs.AI/1007.3223] [pdf] [abstract/bibtex]
  
  
• Blocked Clause Elimination.
  Matti Järvisalo, Armin Biere, and Marijn Heule.
  In Javier Esparza and Rupak Majumdar, editors, Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2010), volume 6015 of Lecture Notes in Computer Science (LNCS), pages 129-144. Springer, 2010.
  [doi:10.1007/978-3-642-12002-2_10] Preliminary version: [pdf] [abstract/bibtex]
  
  
• Clause Elimination Procedures for CNF Formulas.
  Marijn Heule, Matti Järvisalo, and Armin Biere.
  In Christian Fermüller and Andrei Voronkov, editors, Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-17), volume 6397 of Lecture Notes in Computer Science (LNCS/ARCoSS), pages 357-371. Springer, 2010.
  [doi:10.1007/978-3-642-16242-8_26] Preliminary version: [pdf] [abstract/bibtex]
  
  
• Reconstructing Solutions after Blocked Clause Elimination.
  Matti Järvisalo and Armin Biere.
  In Ofer Strichman and Stefan Szeider, editors, Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010), volume 6175 of Lecture Notes in Computer Science (LNCS), pages 340-345. Springer, 2010.
  [doi:10.1007/978-3-642-14186-7_30] Preliminary version: [pdf] [abstract/bibtex]
  
  
• Depth-Based Local Search Heuristics for Boolean Circuit Satisfiability.
  Anton Belov and Matti Järvisalo.
  HIIT Technical Reports 2010-2, Helsinki Institute for Information Technology HIIT, Helsinki, Finland, 2010. ISBN 978-952-60-3415-7.
  [pdf] [abstract/bibtex]
  
  
• Blocked Clause Elimination and its Extentions.
  Marijn J.H. Heule, Matti Järvisalo, and Armin Biere.
  Extended abstract presented at Guangzhou Symposium on Satisfiability In Logic-Based Modeling, 2010.
  [pdf]
  

2009

• Limitations of Restricted Branching in Clause Learning.
  Matti Järvisalo and Tommi Junttila.
  Constraints, 14(3):325-356, 2009.
  [doi:10.1007/s10601-008-9062-z] [pdf] [abstract/bibtex]
  
  
• Structure-Based Satisfiability Checking: Analyzing and Harnessing the Potential.
  Matti Järvisalo.
  AI Communications, 22(2):117-119, 2009.
  [doi:10.3233/AIC-2009-0445] [pdf] [abstract/bibtex]
  
  
• Max-ASP: Maximum Satisfiability of Answer Set Programs.
  Emilia Oikarinen and Matti Järvisalo.
  In Esra Erdem, Fangzhen Lin, and Torsten Schaub, editors, Proceedings of the 10th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2009), volume 5753 of Lecture Notes in Computer Science (LNCS/LNAI), pages 236-249. Springer, 2009.
  [10.1007/978-3-642-04238-6_21] [pdf] [abstract/bibtex]
  
  
• A Module-Based Framework for Multi-Language Constraint Modeling.
  Matti Järvisalo, Emilia Oikarinen, Tomi Janhunen, and Ilkka Niemelä.
  In Esra Erdem, Fangzhen Lin, and Torsten Schaub, editors, Proceedings of the 10th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2009), volume 5753 of Lecture Notes in Computer Science (LNCS/LNAI), pages 155-168. Springer, 2009.
  [doi:10.1007/978-3-642-04238-6_15] [pdf] [abstract/bibtex]
  
  
• A Module-Based Framework for Multi-Language Constraint Modeling.
  Matti Järvisalo, Emilia Oikarinen, Tomi Janhunen, and Ilkka Niemelä.
  In 2nd Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2009), 2009.
  

2008

• Structure-Based Satisfiability Checking: Analyzing and Harnessing the Potential
  Matti Järvisalo.
  Doctoral dissertation.
  Volume TKK-ICS-D10 of TKK Dissertations in Information and Computer Science.
  Helsinki University of Technology, Faculty of Information and Natural Sciences, Department of Information and Computer Science, Espoo, Finland, 2008.
  ISBN 978-951-22-9641-5 (print) / 978-951-22-9642-2 (online).
  [abstract/bibtex] [Online version]
  
  
• The Effect of Structural Branching on the Efficiency of Clause Learning SAT Solving: An Experimental Study.
  Matti Järvisalo and Ilkka Niemelä.
  Journal of Algorithms, 63(1-3):90-113, 2008.
  [doi:10.1016/j.jalgor.2008.02.005] [pdf] [abstract/bibtex]
  
  
• Extended ASP Tableaux and Rule Redundancy in Normal Logic Programs.
  Matti Järvisalo and Emilia Oikarinen.
  Theory and Practice of Logic Programming, 8(5-6):691-716, 2008.
  [doi:10.1017/S1471068408003578] Preliminary version: [arXiv:cs.AI/0809.3204] [pdf] [abstract/bibtex]
  
  
• Justification-Based Local Search with Adaptive Noise Strategies.
  Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä.
  In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2008), volume 5330 of Lecture Notes in Computer Science, pages 31-46. Springer, 2008.
  [doi:10.1007/978-3-540-89439-1_3] [pdf] [abstract/bibtex]
  
  
• Justification-Based Non-Clausal Local Search for SAT.
  Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä.
  In Malik Ghallab, Constantine D. Spyropoulos, Nikos Fanotakis, and Nikos Avoukis, editors, Proceedings of the 18th European Conference on Artificial Intelligence (ECAI 2008), volume 178 of Frontiers in Artificial Intelligence and Applications, pages 535-539. IOS Press, 2008.
  [doi:10.3233/978-1-58603-891-5-535] [pdf] [abstract/bibtex]
  
  
• On the Power of Top-Down Branching Heuristics.
  Matti Järvisalo and Tommi Junttila.
  In Dieter Fox and Carla P. Gomes, editors, Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI 2008), pages 304-309. AAAI Press, 2008.
  [Publisher's copy] [pdf] [abstract/bibtex]
  
  
• Justification-Based Local Search with Adaptive Noise Strategies.
  Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä.
  In Proceedings of the 2nd International Workshop on Logic and Search: Computation of structures from declarative descriptions (LaSh 2008), pages 111-125. KU Leuven, 2008.
  [See the LPAR'08 version] [abstract/bibtex]
  

2007

• Limitations of Restricted Branching in Clause Learning.
  Matti Järvisalo and Tommi Junttila.
  In Christian Bessiere, editor, Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming (CP 2007), volume 4741 of Lecture Notes in Computer Science (LNCS), pages 348-363. Springer, 2007.
  [Runner-up for the CP'07 Best Paper Award]
  [doi:10.1007/978-3-540-74970-7_26] [pdf] [abstract/bibtex]
  
  
• Extended ASP Tableaux and Rule Redundancy in Normal Logic Programs.
  Matti Järvisalo and Emilia Oikarinen.
  In Verónica Dahl and Ilkka Niemelä, editors, Proceedings of the 23rd International Conference on Logic Programming (ICLP 2007), volume 4670 of Lecture Notes in Computer Science (LNCS), pages 134-148. Springer 2007.
  [ICLP'07 Best Student Paper Award]
  [doi:10.1007/978-3-540-74610-2_10] [pdf] [bibtex]
  
  
• The Effect of Structural Branching on the Efficiency of Clause Learning SAT Solving.
  Matti Järvisalo.
  In 14th RCRA Workshop: Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, 2007.
  [pdf] [abstract/bibtex]
  
  
• Restricted Branching in Clause Learning DPLL.
  Matti Järvisalo.
  In Brahim Hnich and Kostas Stergiou, editors, Proceedings of the CP 2007 Doctoral Programme, 2007.
  [bibtex]
  
  
• Impact of Restricted Branching on Clause Learning SAT Solving
  Matti Järvisalo.
  Research Report A107, Helsinki University of Technology, Laboratory for Theoretical Computer Science, 2007. ISBN 978-951-22-8907-3.
  [pdf] [abstract/bibtex]
  
  
• Equivalence Checking Hardware Multiplier Designs.
  Matti Järvisalo.
  SAT Competition 2007 benchmark description.
  Benchmarks available here.
  [pdf] [bibtex]
  
  
• Industrial-Strength SAT Solving and Restricted Branching.
  Matti Järvisalo.
  In Veli Mäkinen, Greger Lindén, and Hannu Toivonen, editors, Summer School on Algorithmic Data Analysis (SADA 2007) and Annual Hecse Poster Session. Poster Abstracts, Series of Publications B, Report B-2007-4, page 39. Helsinki University Printing House, 2007. [bibtex]
  
  
• Impact of Restricted Branching on Clause Learning SAT Solving.
  Matti Järvisalo.
  Licentiate's thesis.
  Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science, Espoo, Finland, 2007.
  [bibtex]
  

2006

• Hard Satisfiable Clause Sets for Benchmarking Equivalence Reasoning Techniques.
  Harri Haanpää, Matti Järvisalo, Petteri Kaski, and Ilkka Niemelä.
  Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):27-46, 2006.
  [Publisher's copy] [pdf] [abstract/bibtex]
  
  
• Further Investigations into Regular XORSAT.
  Matti Järvisalo.
  In Proceedings of the 21st National Conference on Artificial Intelligence (AAAI 2006), pages 1873-1874. AAAI Press, 2006.
  [Publisher's copy] [pdf] [bibtex]
  
  
• Opinions, Hopes, and Expectations of CS&E Students, A Case Study in Academic Skills and Hidden Curriculum.
  Matti Järvisalo.
  In Tapio Salakoski, Tomi Mäntylä, and Mikko Laakso, editors, Koli Calling 2005 - Proceedings of the Fifth Koli Calling Conference on Computer Science Education, volume 41 of TUCS General Publications. Turku Centre for Computer Science, 2006. ISBN 951-29-3006-4.
  [abstract/bibtex]
  
  
• drgen - regular d-XORSAT generator.
  Matti Järvisalo.
  February 2006.
  [download] [bibtex]
  

2005

• Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits.
  Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä.
  Annals of Mathematics and Artificial Intelligence, 44(4):373-399, 2005.
  [doi:10.1007/s10472-005-7034-1] [pdf] [abstract/bibtex]
  
  
• SAT Benchmarks based on 3-Regular Graphs.
  Harri Haanpää, Matti Järvisalo, Petteri Kaski, and Ilkka Niemelä.
  May 2005. SAT Competition 2005 benchmark description. Benchmark set available here and SAT Competition 2005 results through this link.
  [pdf] [Please cite our J.SAT 2006 article instead of this description!]
  
  
• rgen - a SAT benchmark generator.
  Matti Järvisalo.
  September 2005.
  [download] [bibtex]
  

2004

• Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits.
  Matti Järvisalo, Tommi A. Junttila, and Ilkka Niemelä.
  In Proceedings of the 8th International Symposium on Artificial Intelligence and Mathematics (ISAIM 2004), pages 129-136, 2004.
  Journal version: [Springerlink] [abstract/bibtex]
  
  
• Teaching Smullyan's Analytic Tableaux in a Scalable Learning Environment.
  Tomi Janhunen, Toni Jussila, Matti Järvisalo, and Emilia Oikarinen.
  In Ari Korhonen and Lauri Malmi, editors, Kolin Kolistelut - Koli Calling 2004, Proceedings of the Fourth Finnish/Baltic Sea Conference on Computer Science Education, volume TKO-42/04 of Research Report Series of Laboratory of Information Processing Science, Helsinki University of Technology, pages 85-94. Otamedia, 2004.
  [abstract/bibtex]
  
  
• A Compact Reformulation of Propositional Satisfiability as Binary Constraint Satisfaction.
  Matti Järvisalo and Ilkka Niemelä.
  In Alan M. Frisch and Ian Miguel, editors, Proceedings of the 3rd International Workshop on Modelling and Reformulating Constraint Satisfaction Problems: Towards Systemisation and Automation (ModRef 2004), pages 111-124, 2004.
  [pdf] [abstract/bibtex]
  
  
• Proof Complexity of Cut-Based Tableaux for Boolean Circuit Satisfiability Checking.
  Matti Järvisalo.
  Research Report A90, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, 2004. ISBN 951-22-7020-X.
  [pdf] [abstract/bibtex]
  
  
• Lauselogiikan toteutuvuustarkastus: käytännönläheistä teoriaa.
  Matti Järvisalo.
  Tietojenkäsittelytiede 22:47-63, 2004. In Finnish.
  [pdf] [abstract/bibtex]
  
  
• Todistuskompleksisuudesta Boolen piirien toteutuvuustarkastuksessa.
  Matti Järvisalo.
  In Pasi Fränti and Esko Marjomaa, editors, Tietojenkäsittelytieteen päivät 2004, volume 5 of International Proceedings Series of Department of Computer Science, University of Joensuu, pages 49-53. Joensuun yliopisto, 2004. In Finnish.
  [pdf] [bibtex]
  
  
• Proof Complexity of Cut-Based Tableaux for Boolean Circuit Satisfiability Checking.
  Matti Järvisalo.
  Master's thesis.
  Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science, Espoo, Finland, 2004.
  [abstract/bibtex]
  

2001

• Altistuminen ilman epäpuhtauksille - mallinnustyökalun kehittäminen.
  Hannu Koskela, Raimo Niemelä, Matti Järvisalo, and Petri Kauhaniemi.
  In Valtteri Hongisto and Riikka Helenius, editors, Työhygienian päivät 2001, volume 16 of Report Series of Turku Regional Institute for Occupational Health, pages 105-112, 2001. In Finnish.