Selected Publications
- 2007
- 2006
- E.
Giunchiglia, M. Maratea - Solving
Optimization
Problems with DLL. In Proc. 17th
European Conference on
Artificial Intelligence, Riva del Garda,August 28th - September 1st
2006. ECAI.
- E.
Giunchiglia, M. Narizzano, A. Tacchella - Quantifier
structure in search based procedures
for QBFs.In Proc. Design, Automation and Test in Europe
(DATE 2006). 6-10
March, 2006, ICM, Messe Munich. Germany.
- E.
Giunchiglia, M. Narizzano, A. Tacchella - Clause/Term
Resolution and Learning in the Evaluation of Quantified Boolean Formulas.
Journal of
Artificial Intelligence Research (JAIR), Vol. 26, pp. 371-417, May
2006..
- E.
Giunchiglia, Y. Lierler, M. Maratea - Answer
Set Programming based on Propositional
Satisfiability. Journal
of Automated Reasoning (JAR),
Vol. 36(4), pgg. 345-377 (2006).
- 2005
- E.
Giunchiglia, M. Maratea - On
the relation
between Answer Set and SAT procedures (or, between smodels and cmodels)
In Proc. 21th International Conference on Logic Programming (ICLP
2005). October 2 - 5, 2005,
Sitges (Barcelona) Spain.
To appear LNCS.
- E.
Giunchiglia, M. Maratea - Evaluating
Search
Strategies and Heuristics for Efficient Answer Set Programming.
Accepted to AI*IA
2005 9th Congress of the Italian
Association for Artificial Intelligence. September 21-23, 2005, Milan, Italy, EU. To appear LNAI.
- A.
Nareyek, R. Fourer, E.C. Freuder, E. Giunchiglia,
R.P. Goldman, H. Kautz,
J. Rintanen, A. Tate. Constraints
and AI Planning.
IEEE Intelligent Systems, 20(2), 62-72.
- A.
Armando, C. Castellini, E. Giunchiglia,
M. Maratea - The
SAT-based
Approach to Separation Logic. Journal of
Automated Reasoning, Volume 35, Numbers 1-3, pp. 237-263,
October 2005 (JAR).
- 2004
- Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella. QuBE++:
an
Efficient QBF Solver. In
Proc. 5th International Conference on Formal Methods in Computer-Aided
Design (FMCAD'04). November 14-17, 2004, Austin, Texas, USA.
- Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella. Monotone
Literals
and Learning in QBF reasoning. In Proc. 10th
International Conference on Principles and Practice of Constraint
Programming (CP'04). September 27 - October 1, 2004, Toronto
Marriott Downtown Eaton Centre, Toronto, Canada.
- E. Giunchiglia, Yuliya Lierler,
M. Maratea. SAT-Based
Answer Set Programming. In
Proc. 19th National Conference on Artificial Intelligence (AAAI). July
25-29, San Jose, California. AAAI.
- A. Armando, C. Castellini, E.
Giunchiglia, M. Idini, and M. Maratea. TSAT++:
an Open Platform for Satisfiability
Modulo Theories. In the
Proceedings of the 2nd Workshop on Pragmatics of Decision Procedures in
Automated Reasoning (PDPAR'04), July 05, 2004, Cork,
Ireland.
- Alessandro
Armando, Claudio
Castellini, Enrico Giunchiglia,
Marco Maratea. A
SAT-based Decision Procedure for the Boolean
Combination of Difference Constraints. In
Proc. of the 7th
International Conference on Theory and Applications of Satisfiability
Testing (SAT'04). May 10-13 2004, Vancouver, BC, Canada.
- Enrico
Giunchiglia, Massimo
Narizzano, Armando Tacchella. QBF
reasoning on real-world instances. In
Proc. the 7th
International Conference on Theory and Applications of Satisfiability
Testing (SAT'04). May 10-13 2004, Vancouver, BC, Canada.
- Salem Benferhat, Enrico Giunchiglia. Editorial
to the
"Artificial Intelligence" special issue on Nonmonotonic Reasoning.
In Artificial
Intelligence,
Volume 157, Issues 1-2, August 2004, Pages 1-3.
- E.
Giunchiglia, J. Lee, V. Lifschitz, N. McCain and H. Turner. Nonmonotonic
causal
theories . In Artificial
Intelligence 153(1-2): 49-104 (2004).
- 2003
- I. Gent, E. Giunchiglia, M.
Narizzano, A. Rowley and A. Tacchella. Watched
Data Structures for QBF Solvers. In
LNCS Vol. 2919 - Theory and Applications of Satisfiability
Testing, Selected Papers.
- E.
Giunchiglia, M. Maratea, A. Tacchella - (In)Effectiveness
of Look-ahead Techniques in
a Modern
SAT Solver. In LNCS Vol. 2833 - Proceedings of the
Ninth
International Conference on Principles and Practice of Constraint
Programming . Short version.
- E.
Giunchiglia, M. Maratea, A. Tacchella -
Look-Ahead vs. Look-Back techniques in a
modern SAT solver. In SAT2003: Sixth
International Conference on Theory and
Applications of Satisfiability Testing. May 5-8 2003. Portofino,
Italy (EU).
- C. Castellini, E. Giunchiglia, A. Tacchella. SAT-Based
planning in complex domains: Concurrency, Constraints and
Nondeterminism . In Artificial
Intelligence, 147(1-2): 85-117 (2003).
- E. Giunchiglia, M. Narizzano and
A. Tacchella. Backjumping
for
Quantified Boolean Logic Satisfiability . In Artificial Intelligence
145(1-2): 99-120 (2003)
- 2002
- Alessandro
Armando, Claudio
Castellini, Enrico Giunchiglia, Fausto
Giunchiglia, Armando Tacchella. SAT-Based
Decision Procedures for Automated Reasoning: a Unifying Perspective.
In Festschrift in
Honor of Jörg H. Siekmann. To appear in Springer Verlag.
- E. Giunchiglia, M. Maratea, A.
Tacchella. Dependent
and Independent Variables for Propositional Satisfiability. In
LNCS Vol. 2424 - Proceedings of the 8th
European Conference on Logics in Artificial Intelligence (JELIA),
September 23-26, 2002, Cosenza - Italy.
- A. Cimatti, E. M. Clarke, E.
Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A.
Tacchella. NuSMV
2: An OpenSource Tool for Symbolic Model Checking . In
Proc. CAV-2002
Conference on Computer-Aided Verification. Copenhagen, Denmark, July
27-31, 2002.
- E. Giunchiglia, M. Narizzano and
A. Tacchella. Learning
for Quantified Boolean Logic Satisfiability . In
Proc. 18th National Conference on Artificial Intelligence (AAAI). July
28 - August 1, 2002 Edmonton, Alberta, Canada. AAAI
- Alessandro
Cimatti, Enrico
Giunchiglia, Marco Pistore,
Marco Roveri, Roberto Sebastiani,
Armando Tacchella. Integrating
BDD-based and SAT-based Symbolic
Model
Checking . In Proc.
Frontiers of Combining Systems (FROCOS). Santa Margherita, Italy,
2002. LNAI, N.2309. Springer Verlag.
- Enrico
Giunchiglia, Fausto
Giunchiglia, Armando Tacchella. SAT-Based
Decision Procedures for Classical Modal Logics. In
Journal of
Automated Reasoning, Vol. 28, no. 2 (February 2002), pagg. 143-171 .
- 2001
- Luigia
Carlucci Aiello, Amedeo
Cesta, Enrico
Giunchiglia, Marco Pistore,
Paolo Traverso. Planning
and verification techniques for the
high level programming and monitoring of autonomous robotic devices.
In ESA
Workshop on "On-Board Autonomy". 17-19 October 2001, ESTEC, Noordwijk,
The Netherlands.
- C. Castellini, E. Giunchiglia, A.
Tacchella. Improvements
to SAT-based conformant planning . In Proc. 6th
European Conference on Planning, Toledo, Spain,
September, 12-14 2001.
- E. Giunchiglia, M. Narizzano, A.
Tacchella. An
analysis of backjumping and trivial truth in quantified boolean
formulas satisfiability . In Proc. 7 Congresso
dell'Associazione
Italiana per l'Intelligenza Artificiale, Bari, September, 25-28 2001.
LNAI 2175.
- E. Giunchiglia, M. Narizzano, A.
Tacchella, M. Vardi. Towards
an Efficient Library for SAT: a
Manifesto . LICS
2001 Workshop on Theory and Applications of Satisfiability Testing (SAT
2001), Boston (Massachusetts, USA),
June 14-15, 2001. Vol. 9,
Electronics Notes in Discrete Mathematics. Elsevier Science.
- E.
Giunchiglia, A. Tacchella. A
Subset-matching Size-bounded Cache for Testing
Satisfiability in Modal Logics . Extended
version of the paper in Proc. Tableaux 2000. In Annals
of Mathematics and Artificial Intelligence, 33:39-67, 2001.
- E. Giunchiglia, M. Narizzano and
A. Tacchella. Backjumping
for Quantified Boolean Logic
Satisfiability . In
Proc. 17th International Joint Conference on Artificial Intelligence
(IJCAI). Seattle, Washington, USA, August 4-10, 2001.
- E. Giunchiglia, M. Maratea, A.
Tacchella and D. Zambonin. Evaluating
search heuristics and optimization
techniques in propositional satisfiability. In
Proc. International Joint Conference on Automated Reasoning (IJCAR),
Siena, June,
18-23 2001. LNAI 2083.
- E. Giunchiglia, M. Narizzano and
A. Tacchella. QUBE:
A system for deciding Quantified Boolean
Formulas
Satisfiability. In Proc. International Joint
Conference on
Automated Reasoning (IJCAR), Siena,
June, 18-23 2001. LNAI 2083.
- F. Copty, L. Fix, E. Giunchiglia,
G. Kamhi, A. Tacchella and M. Vardi. Benefits
of Bounded Model Checking at an
Industrial Setting. In Proc. 13th Conference on
Computer Aided
Verification (CAV'01). July 18-23, 2001. Paris, France.
- E.
Giunchiglia, F. Giunchiglia. Ideal
and Real Belief about Belief . Journal
of Logic and Computation, Vol. 11, No 1. pp. 157-192, 2001.
- Luigia
Carlucci Aiello, Amedeo
Cesta, Enrico
Giunchiglia, Paolo Traverso. Merging
Planning and Verification Techniques for "Safe Planning" in Space
Robotics. In 6th International Symposium on
Artificial
Intelligence, Robotics and Automation in Space: A New Space Odyssey.
Montreal,
Canada, June 18 - 22, 2001
- 2000
- E.
Giunchiglia, A. Tacchella. *SAT:
a System for the Development of Modal
Decision Procedures . In Proc. CADE 2000.
- E.
Giunchiglia, A. Tacchella. A
Subset-matching Size-bounded Cache for
Satisfiability in Modal Logics . In Proc.
Tableaux 2000.
- E. Giunchiglia, F. Giunchiglia,
R. Sebastiani, A. Tacchella. SAT
vs. Translation Based decision procedures
for modal logics: a comparative evaluation. Journal
of Applied Non Classical Logics, vol. 10, number 2, pp. 145-172, 2000.
- E. Giunchiglia, F. Giunchiglia,
A. Tacchella. SAT-Based
Decision Procedures for Classical Modal Logics. In
SAT2000. Highlights of Satisfiability Research in the Year 2000.
Ian Gent and Hans Van Maaren
and Toby Walsh
editors. IOS Press. 2000. To appear also in Journal of Automated
Reasoning.
- P.
Ferraris, E. Giunchiglia. Planning
as Satisfiability in Nondeterministic
Domains . In AAAI'00, July 30-August 3, 2000,
Austin, Texas. AAAI
- E.
Giunchiglia. Planning
as Satisfiability with Expressive
Action
Languages: Concurrency, Constraints and Nondeterminism. In
Seventh International Conference on Principles of Knowledge
Representation and Reasoning (KR'00). Breckenridge, Colorado,
USA 12-15 April 2000.
- A. Cesta, E. Giunchiglia, P.
Traverso. Interactive Autonomy
for Space Applications. In Proc. 2nd Intl. Workshop on
Planning and
Scheduling for Space. Marzo 16-18, 2000, San Francisco, California.
NASA Conference Proceedings number NASA/CP--2000-209590 issued by the
NASA Ames Research Center, Moffett Field, California.
- 1999
- E. Giunchiglia, R. Sebastiani. Applying
the
Davis-Putnam procedure to non-clausal formulas . In
AI*IA'99.
- A. Armando, C. Castellini, E.
Giunchiglia. SAT-based
procedures for temporal reasoning. In Proceeding
of the 5th European Conference on Planning (ECP-99). Durham
(UK), September 8-10, 1999.
- E.
Giunchiglia, V. Lifschitz. Action
Languages, Temporal Action Logics and the
Situation Calculus. In NRAC'99.
- A.
Cesta, M. Daniele, E. Giunchiglia, M. Piaggio, P. Riccucci, M. Schaerf,
P. Traverso. JERRY: A System for
the Automatic Generation and Execution of Plans for Robotic Devices -
The Case Study of the SPIDER Arm. In Proc. 5th
International Symposium on Artificial Intelligence, Robotics and
Automation in Space (iSAIRAS 99)}, pag. 687--692, ESTEC, Noordwijk,
Olanda, Giugno 1-3, 1999.
- M. Benerecetti, E. Giunchiglia,
L. Serafini, A. Villafiorita. Formal
specification of beliefs in multi-agent
systems . In International Journal of Intelligent
Systems, 14:1021--1040, October 1999.
- 1998
- E.
Giunchiglia, V. Lifschitz. An
Action Language Based on Causal Explanation:
Preliminary Report. In AAAI'98. AAAI
- E. Giunchiglia, A. Massarotto, R.
Sebastiani. Act,
and the Rest Will Follow: Exploiting Determinism in Planning as
Satisfiability. In AAAI'98. AAAI
- E. Giunchiglia, F. Giunchiglia,
R. Sebastiani, A. Tacchella. More
evaluation of decision procedures for modal
logics. In
Sixth International Conference on Principles of Knowledge
Representation and Reasoning (KR'98). Trento, Italy, June 2--5
1998. Morgan Kauffmann Publishers.
- M. Di Manzo, E. Giunchiglia, S.
Ruffino. Planning
via Model Checking in Determistic Domains: Preliminary Report.
In
AIMSA'98.
- 1997
- E. Giunchiglia, G. N. Kartha, V.
Lifschitz. Representing
Action: Indeterminacy and Ramifications.. In Artificial
Intelligence vol. 95, no. 2, pp.
409-438.
- A. Cimatti, E. Giunchiglia, F.
Giunchiglia, and P. Traverso. Planning
via Model Checking: A Decision
Procedure for AR . May 1997. In Proc. of
the Fourth European
Conference on Planning -- ECP '97, Toulouse, France,
24/25/26 September 1997.
- < 1997
- E.
Giunchiglia. Determining
Ramifications in the Situation
Calculus. In
Fifth International Conference on Principles of Knowledge
Representation and Reasoning (KR'96). Cambridge, Massachusetts,
November 5--8 1996. Morgan Kauffmann Publishers.
- E.
Giunchiglia, V. Lifschitz. Dependent
fluents. In
Proc. of the 14th International Joint Conference on Artificial
Intelligence (IJCAI'95), pag 1964--1969, Montreal, Canada,
August 20-25 1995. Morgan Kauffmann Publishers.
- E. Giunchiglia, G. N. Kartha, V.
Lifschitz. Actions
with indirect effects. In
Symposium on Extending Theories of Action: Formal Theory and Practical
Applications, 1995. AAAI Spring Symposium Series, pag. 80--85,
Stanford, U.S.A.,
March 27-29 1995.
- A. Armando, E. Giunchiglia, P.
Pecchiari. Structured
Proof Procedures. In the Annals
of Mathematics and Artificial Intelligence, vol. 15, n. 1, 1995.
- E.
Giunchiglia, P. Traverso. A
Multi-context Architecture for Formalizing
Complex Reasoning . In International Journal of
Intelligent
Systems, 10:501--539, May 1995.
- F. Giunchiglia, L. Serafini, E.
Giunchiglia, M. Frixione. Non-Omniscient
Belief as Context-Based Reasoning . In
Proc. of the 13th International Joint Conference on Artificial
Intelligence (IJCAI'93). pag. 548--554, Chambery, France.
Morgan Kauffmann Publishers
- A.
Armando, E. Giunchiglia. Embedding
complex decision procedures inside an
interactive theorem prover. In the Annals
of Mathematics and Artificial Intelligence, vol. 8, n. 3-4, 1993.
- F.
Giunchiglia, E. Giunchiglia. Building
Complex Derived Inference Rules: a
Decider for the Class of Prenex Universal-Existential Formulas.
In
Proceedings 7th European Conference of Artificial Intelligence
(ECAI-88), pp. 607-609. Pitman Publishing, 1988.