Tomi Janhunen, Guohua Liu, and Ilkka Niemelä. Tight Integration of Non-Ground Answer Set Programming and Satisfiability Modulo Theories. To be Presented at the 1st Workshop on Grounding and Transformations for Theories with Variables, Vancouver, British Columbia, Canada, May 2011.
Guohua Liu, Randy Goebel, Tomi Janhunen, Ilkka Niemelä, and Jia-Huai You. Strong Equivalence of Logic Programs with Abstract Constraint Atoms. In J. Degrande and W. Faber, editors, the Proceedings of the 11th International Conference on Logic Programming and Nonmonotonic Reasoning, 161—173. Vancouver, British Columbia, Canada, May 2011. Springer-Verlag. Lecture Notes in Computer Science, vol. 6645. [Link]
Tomi Janhunen, Ilkka Niemelä, Johannes Oetsch, Jörg Pührer, and Hans Tompits. Random vs. Structure-Based Testing of Answer-Set Programs: An Experimental Comparison. In J. Degrande and W. Faber, editors, the Proceedings of the 11th International Conference on Logic Programming and Nonmonotonic Reasoning, 242—247. Vancouver, British Columbia, Canada, May 2011. Springer-Verlag. Lecture Notes in Computer Science, vol. 6645. [Link]
Tomi Janhunen and Ilkka Niemelä. Compact Translations of Non-Disjunctive Answer Set Programs to Propositional Clauses. In M. Balduccini and T. C. Son, editors, in the Proceedings of Symposium on Constructive Mathematics in Computer Science, Organized in Honour of Michael Gelfond's 65th Anniversary, 111—130, Lexington, Kentucky, October 2010. Springer-Verlag. Lecture Notes in Computer Science, vol. 6565. [Link]
Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Partitioning sat instances for distributed solving. In Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2010, volume 6397 of Lecture Notes in Computer Science, pages 372–386, 2010.
Vesa Luukkala and Ilkka Niemelä. Enhancing a smart space with answer set programming. In Proceedings of the 4th International Web Rule Symposium, RuleML 2010, Lecture Notes in Computer Science, 2010. To appear.
Tomi Janhunen, and Ilkka Niemelä (Eds). Logics in Artificial Intelligence - 12th European Conference, JELIA 2010, Helsinki, Finland, September 13-15, 2010. Proceedings Springer 2010. [Link]
Tero Laitinen, Tommi Junttila, and Ilkka Niemelä. Extending clause learning DPLL with parity reasoning. In Proceedings of the 19th European Conference on Artificial Intelligence, ECAI 2010, volume 215 of Frontiers in Artificial Intelligence and Applications, pages 21–26. IOS Press, 2010.
Tomi Janhunen, Ilkka Niemelä, Johannes Oetsch, Jörg Pührer, and Hans Tompits. On testing answer-set programs. In Proceedings of the 19th European Conference on Artificial Intelligence, ECAI 2010, volume 215 of Frontiers in Artificial Intelligence and Applications, pages 951–956. IOS Press, 2010.
Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Partitioning search spaces of a randomized search. In Proceedings of the 11th Conference of the Italian Association for Artificial Intelligence, AI*IA 2009: 243-252. LNCS 5883 [Link] [Extended report version including proofs]
Kari Kähkönen, Jani Lampinen, Keijo Heljanko, Ilkka Niemelä: The LIME Interface Specification Language and Runtime Monitoring Tool. RV 2009: 93-100. LNCS 5779 [Link]
Tomi Janhunen, Ilkka Niemelä, Mark Sevalnev: Computing Stable Models via Reductions to Difference Logic. LPNMR 2009: 142-154. LNCS 5753 [Link]
Matti Järvisalo, Emilia Oikarinen, Tomi Janhunen, Ilkka Niemelä: A Module-Based Framework for Multi-language Constraint Modeling. LPNMR 2009: 155-168. LNCS 5753 [Link]
Ilkka Niemelä: Integrating Answer Set Programming and Satisfiability Modulo Theories. LPNMR 2009: 3. LNCS 5753 [Link]
Antti Hyvärinen, Tommi Junttila, and Ilkka
Niemelä.
Incorporating Clause Learning in Grid-Based Randomized SAT Solving.
Journal on Satisfiability, Boolean Modeling and Computation
6 (2009), 223-244
[Link] to the journal web page
Kim Björkmann, Juho Frits, Janne Valkonen, Keijo Heljanko, and Ilkka Niemelä. Model-Based Analysis of a Stepwise Shutdown Logic. VTT Working Papers 115, VTT Technical Research Centre of Finland, Espoo, 2009. [Link]
Janne Valkonen, Matti Koskimies, Kim Björkman, Keijo Heljanko, Ilkka Niemelä, and Jari J. Hämäläinen. Formal Verification of Safety Automation Logic Designs. Automaatio XVIII 2009 Seminaari. [Link]
Rolf Drechsler, Tommi Junttila, and Ilkka Niemelä. Non-Clausal SAT and ATPG. In Armin Biere, , Marijn J. H. Heule, Hans van Maaren,and Toby Walsh, Editors, Handbook of Satisfiability, Chapter 21, pages 655-693, Frontiers in Artificial Intelligence and Applications, IOS Press, 2009. [Homepage of the Handbook]
Gerhard Brewka, Ilkka Niemelä, and Miroslaw Truszczyski. Nonmonotonic Reasoning. In Frank van Harmelen, Vladimir Lifschitz, and Bruce Porter, editors, Handbook of Knowledge Representation, chapter 6, pages 239-284. Elsevier Science, Amsterdam, 2008. [Link]
Matti Järvisalo and Ilkka Niemelä.
The Effect of Structural Branching on the Efficiency of Clause Learning
SAT Solving: An Experimental Study.
Journal of Algorithms,
63 (2008) 90-113.
[doi:10.1016/j.jalgor.2008.02.005]
Preliminary version:
[ps]
[pdf]
[bibtex]
Janne Valkonen, Ville Pettersson, Kim Björkman, Jan-Erik Holmberg, Matti Koskimies, Keijo Heljanko, and Ilkka Niemelä. Model-based analysis of an arc protection and an emergency cooling system. VTT Working Papers 93, VTT Technical Research Centre of Finland, Espoo, 2008. [Link]
Janne Valkonen, Ilkka Karanta, Matti Koskimies, Keijo Heljanko, Ilkka Niemelä, Dan Sheridan, and Robing E. Bloomfield. NPP safety automation systems analysis: State of the art. VTT Working Papers 94, VTT Technical Research Centre of Finland, Espoo, 2008. [Link]
Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä.
Strategies for solving SAT in Grids by randomized search.
In Proceedings of the
9th International Conference on
Artificial Intelligence and Symbolic Computation (AISC 2008),
LNCS 5144, pages 125-140, Springer-Verlag, 2008.
[ps]
[pdf]
[bibtex]
[Link to the
published paper]
Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. Justification-Based Non-Clausal Local Search for SAT. In Proceedings of the 18th European Conference on Artificial Intelligence (ECAI 2008), IOS Press, 2008. [ps] [pdf] [bibtex] [Link to the published paper]
Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä.
Incorporating Learning in Grid-Based Randomized SAT Solving.
In Proceedings of the
13th International Conference on Artificial Intelligence: Methodology,
Systems, Applications (AIMSA 2008), Springer (to appear).
[ps]
[pdf]
[bibtex]
[Link to the
published paper]
Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. Justification-Based Local Search with Adaptive Noise Strategies. 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] [ps] [pdf] [abstract/bibtex]
Ilkka Niemelä. Answer Set Programming without Unstratified Negation. Proceedings of the 24th International Conference on Logic Programming (ICLP 2008), volume 5366 of Lecture Notes in Computer Science, pages 88-92. Springer, 2008. [pdf] [doi:10.1007/978-3-540-89982-2_15]
J. Rintanen, K. Heljanko, and I, Niemelä. Planning as Satisfiability: Parallel Plans and Algorithms for Plan Search (pdf). Artificial Intelligence, Artificial Intelligence, September 2006, 170 (2006) 12-13, 1031-1080. [Link]
Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. A Distribution Method for Solving SAT in Grids. In: SAT 2006, volume 4121 of Lecture Notes in Computer Science, pages 430-435, Springer, 2006.
Tomi Janhunen, Ilkka Niemelä, Dietmar Seipel, Patrik Simons, Jia-Huai You. Unfolding Partiality and Disjunctions in Stable Model Semantics. ACM Transactions on Computational Logic January, 7(1), 1-37, 2006. [Link]
Harri Haanpää, Matti Järvisalo, Petteri Kaski, and Ilkka Niemelä. Hard Satisfiable Clause Sets for Benchmarking Equivalence Reasoning Techniques. Journal on Satisfiability, Boolean Modeling and Computation. Volume 2 (2006), 27-46.
G. Brewka, I. Niemelä, and M. Truszczynski. Prioritized Component Systems, Proceedings of the Twentieth National Conference on Artificial Intelligence, 2005, accepted for publication. [pdf]
J. Rintanen, K. Heljanko, and I. Niemelä. Planning as Satisfiability: Parallel Plans and Algorithms for Plan Search. Technical report 216, Institute of Computer Science at Freiburg University, 2005, 56p. [Link].
M. Keinänen and I. Niemelä. Solving Alternating boolean Equation Systems in Answer Set Programming. Applications of Declarative Programming and Knowledge Management. Pages 134-148. Lecture Notes in Computer Science 3392. Springer-Verlag, 2005. [Springerlink]
M. Järvisalo,
T. Junttila, and I. Niemelä.
Unrestricted vs Restricted Cut in a Tableau Method for Boolean
Circuits.
Annals of Mathematics and Artificial Intelligence, 44(4), 373-399,
2005.
[Springerlink]
Preliminary version:
[ps]
[pdf]
[abstract/bibtex]
T. Jussila, K. Heljanko, and I. Niemelä.
BMC via On-the-Fly Determinization.
International Journal on Software Tools for Technology
Transfer, 7(2), 89-101, 2005.
[ps]
[pdf].
[Link to the article in the journal]
M. Järvisalo and I. Niemelä. A Compact Reformulation of Propositional Satisfiability as Binary Constraint Satisfaction. In Proceedings of the Third International Workshop on Modelling and Reformulating Constraint Satisfaction Problems: Towards Systemisation and Automation, Toronto, Canada, September 2004. [abstract/bibtex/ps/pdf]
J. Rintanen, K. Heljanko, and I. Niemelä. Parallel Encodings of Classical Planning as Satisfiability. In Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA'04), Lecture Notes in Computer Science 3229, Lisbon, Portugal, September 2004. © Springer. To appear. [ps.gz] [pdf]. [Springerlink]
G. Brewka, I. Niemelä, and T. Syrjänen. Logic Programs with Ordered Disjunction. To appear in Computational Intelligence, 20(2), 333-357, 2004. [ps]
M. Keinänen and I. Niemelä. Solving alternating Boolean equation systems in answer set programming. Presented at the 15th International Conference on Applications of Declarative Programming and Knowledge Management (INAP 2004). Potsdam, Germany, March 2004. [ps] [pdf]
M. Järvisalo, T. Junttila, and I. Niemelä. Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits. The 8th International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida, USA, January 4-6, 2004. [ps] [pdf]
V. Marek, I. Niemelä, M. Truszczynski.
Logic
Programming with Monotone Cardinality Atoms,
To appear in the Seventh International Conference on Logic Programming
and Nonmonotonic Reasoning (LPNMR-7), Fort Lauderdale, Florida, Jan 6-8,
2004. [ps]
©
Springer-Verlag.
Lecture Notes in Artificial Intelligence, vol. 2923.
[Springerlink]
T. Janhunen and I. Niemelä.
GNT
- A Solver for Disjunctive Logic Programs.
In Proceedings
of the Seventh International Conference on Logic Programming and
Nonmonotonic Reasoning, pages 331-335, Fort Lauderdale, Florida,
January 2004. ©
Springer-Verlag.
Lecture Notes in Artificial Intelligence, vol. 2923.
[Springerlink]
G. Brewka, I. Niemelä, and M. Truszczynski. Answer Set Optimization. To appear in Proceedings of IJCAI-03. [ps]
T. Janhunen, I. Niemelä, D. Seipel, P. Simons, and J. You. Unfolding Partiality and Disjunctions in Stable Model Semantics. This is an extended version of a paper presented at KR'2002. (CoRR: arXiv:cs.AI/0303009). Accepted for publication in ACM Transactions on Computational Logic [ps]
See, GnT for the resulting implementation of disjunctive semantics.K. Heljanko and I. Niemelä. Bounded LTL Model Checking with Stable Models. Accepted for publication in Theory and Practice of Logic Programming (TPLP), 3 (4&5): 519-550, 2003. (CoRR: arXiv:cs.LO/0305040). (See also experiments).
G. Brewka, I. Niemelä and T. Syrjänen.
Implementing Ordered Disjunction Using Answer Set Solvers for
Normal Programs.
Proceedings of the
8th European Conference on Logics in Artificial Intelligence
(JELIA'02),
Cosenza, Italy, September 23-26, 2002.
[ps] [pdf]
©Springer-Verlag.
[Springerlink]
P. Simons, I. Niemelä, and T. Soininen.
Extending and Implementing the Stable Model Semantics.
[ps.gz]
To appear in Artificial Intelligence, 138(1-2): 181-234, 2002.
K. Heljanko and I. Niemelä.
Bounded LTL Model Checking with Stable Models.
Proceedings of the 6th International Conference on Logic Programming and
Nonmonotonic Reasoning, Vienna, Austria, September 17-19, 2001.
Volume 2173 of Lecture Notes in Artificial Intelligence,
Springer, Berlin.
[ps.gz] [pdf]
[Springerlink]
T. Syrjänen and I. Niemelä.
The Smodels System. Proceedings of the 6th International Conference
on Logic Programming and Nonmonotonic Reasoning LPNMR 2001, Vienna,
Austria, September 17-19, 2001.
Volume 2173 of Lecture Notes in Artificial Intelligence,
Springer, Berlin.
[ps.gz]
©
K. Heljanko and I. Niemelä.
Answer Set Programming and Bounded Model Checking.
Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming:
Towards Efficient and Scalable Knowledge.
Stanford, USA, March 2001.
[ps.gz]
T. Soininen, I. Niemelä, J. Tiihonen, and R. Sulonen.
Representing Configuration Knowledge With Weight Constraint Rules.
Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming:
Towards Efficient and Scalable Knowledge.
Stanford, USA, March 2001.
[ps.gz]
S. Brass and J. Dix and I. Niemelä and T.C. Przymusinski.
On the Equivalence of the Static and
Disjunctive Well-Founded Semantics and its Computation.
Theoretical Computer Science. To appear.
[ps.gz]
Ilkka Niemelä and Patrik Simons.
Extending the Smodels System with Cardinality and Weight Constraints.
This is an introduction to the extended
rule language of Smodels 2.x. To appear in
Jack Minker, editor, Logic-Based Artificial Intelligence,
pages 491-521. Kluwer Academic Publishers, 2000.
Hietalahti, M., Massacci, F., and Niemelä, I.
DES: a challenge problem for nonmonotonic reasoning systems.
In Proceedings of the 8th International Workshop on
Non-Monotonic Reasoning, Breckenridge, Colorado, USA.
(CoRR: arXiv:cs.AI/0003039)
(Test
cases)
I. Niemelä, P. Simons, and T. Syrjänen.
Smodels: a system for answer set programming.
In Proceedings of the 8th International Workshop on
Non-Monotonic Reasoning (cs.AI/0003073), Breckenridge, Colorado, USA, April
2000.
(CoRR: arXiv:cs.AI/0003033)
Tomi Janhunen, Ilkka Niemelä, Patrik Simons, and Jia-Huai You.
Unfolding partiality and disjunctions in stable model semantics. In
A.G. Cohn, F. Guinchiglia, and B. Selman, editors, Proceedings of the
Seventh International Conference on Principles of Knowledge
Representation and Reasoning, pages 411-419, Breckenridge, Colorado,
USA, April 2000. Morgan Kaufmann Publishers.
T. Soininen, I. Niemelä, J. Tiihonen, and R. Sulonen.
Unified configuration knowledge representation using weight
constraint rules.
In Workshop Notes of the ECAI'2000 Configuration Workshop,
pages 79--84, Berlin, Germany, August 2000.
[ps.gz]
K. Heljanko and I. Niemelä.
Petri net analysis and nonmonotonic reasoning.
In Leksa Notes in Computer Science, Festschrift in Honour of Professor Leo
Ojala, pages 7-19. Helsinki University of Technology, Laboratory for
Theoretical Computer Science, 2000.
[ps.gz]
Timo Soininen and Ilkka Niemelä.
Developing a declarative rule language for applications in product
configuration,
in Proceedings of the First International Workshop on Practical
Aspects of Declarative Languages, San Antonio, Texas, May 1999.
Springer-Verlag.
See LNCS Series Homepage
Timo Soininen, Esther Gelle, and Ilkka Niemelä.
A Fixpoint Definition of Dynamic Constraint Satisfaction,
in the Proceedings of the
Fifth International Conference on Principles and
Practice of Constraint Programming, Alexandria, Virginia, USA,
October 12-16, 1999.
Springer-Verlag.
See LNCS Series
Homepage
Ilkka Niemelä, Patrik Simons, and Timo Soininen.
Stable Model Semantics of Weight Constraint Rules,
in the Proceedings of the
Fifth International Conference on Logic Programming and Nonmonotonic
Reasoning, El Paso, Texas, USA, December 2-4, 1999.
Springer-Verlag.
See LNCS Series
Homepage
H. Beaver and I. Niemelä.
Finding MAPs for Belief Networks using Rule-based Constraint
Programming.
Arpakannus 1/99 - Special Issue on Networks'99.
[ps.gz]
C. Aravindan and J. Dix and I. Niemelä.
DisLoP: A Research Project on Disjunctive Logic Programming.
AI Communications, 10 (1997) 3/4, 151-165.
[ps.gz]
Ilkka Niemelä,
A tableau calculus for minimal model reasoning,
Research Report 5-96, Universität Koblenz-Landau, 1996.
(Abstract,
Report)
Ilkka Niemelä,
Implementing Circumscription Using a Tableau Method,
Research Report 6-96, Universität Koblenz-Landau, 1996.
(Abstract,
Report)
Ilkka Niemelä,
A tableau calculus for minimal model reasoning,
in Proceedings of the Fifth Workshop on Theorem Proving with
Analytic Tableaux and Related Methods, pages 278-294, Terrasini, Italy,
May 15-17, 1996, Springer-Verlag, 1996.
Ilkka Niemelä,
Autoepistemic Logic as a Basis for Automating Nonmonotonic Reasoning,
in Partiality, Modality and Non-monotonicity, Patrick Doherty (Ed.),
CSLI Publications, 1996, pages 251-289.
[Springerlink]
2000
Tommi Junttila and Ilkka Niemelä.
Towards an efficient tableau method for boolean circuit
satisfiability checking.
In Proceedings of the First International Conference on
Computational Logic, Automated Deduction: Putting Theory into Practice,
pages 553-567, London, U.K., July 2000.
Volume 1861 of
Lecture Notes in Artificial Intelligence,
Springer, Berlin.
[Gzipped PostScript]
(116 Kb).
[PDF]
© Springer-Verlag.
[Springerlink]
For an implementation of the method, see BCSat solver
1999
I. Niemelä,
Logic Programs with Stable Model Semantics as a Constraint
Programming Paradigm.
(Test
cases)
This is an extended version of the paper presented at
the Workshop on Computational Aspects of
Nonmonotonic Reasoning, Trento, Italy, May 30-June 1, 1998 and
accepted for publication in Annals of Mathematics and
Artificial Intelligence 25(3,4):241-273, 1999.
[Link]
1998
Stefan Brass, Jürgen Dix, Ilkka Niemelä, and Teodor C. Przymusinski.
A comparison of the static and the disjunctive well-founded semantics
and its implementation,
in Proceedings of Sixth International Conference on Principles
of Knowledge Representation and Reasoning, pages 74-85, Trento, Italy, June
1998. Morgan Kaufmann Publishers.
1997
Ilkka Niemelä and Patrik Simons,
Smodels - an implementation of the stable model and well-founded
semantics for normal logic programs,
in Proceedings of the 4th International Conference on Logic Programming
and Non-Monotonic Reasoning,
Dagstuhl, Germany, July 28-31, 1997, Springer-Verlag.
[ps.gz]
[Springerlink]
1996
Stefan Brass, Jürgen Dix, Ilkka Niemelä and Teodor C. Przymusinski,
A Comparison of STATIC semantics with D-WFS,
Research Report 2-96, Universität Koblenz-Landau, 1996.
(Abstract,
Report)
Ilkka Niemelä and Patrik Simons, Evaluating an Algorithm for Default Reasoning, in Working Notes of the IJCAI'95 Workshop on Applications and Implementations of Nonmonotonic Reasoning Systems, Montreal, August 21, 1995, Montré al, Canada, pages 66-72.
Ilkka Niemelä, Autoepistemic Logic as a Unified Basis for Nonmonotonic Reasoning , Doctoral Dissertation, Research report A24, Helsinki University of Technology, Digital Systems Laboratory, Espoo, Finland, 1993, 162 p. (Abstract)