Arrow Research search

Author name cluster

Marco Maratea

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

32 papers
2 author rows

Possible papers

32

AAAI Conference 2026 Conference Paper

A Domain-specific Heuristic for PDDL+-based Traffic Signal Optimisation

  • Francesco Doria
  • Francesco Percassi
  • Marco Maratea
  • Mauro Vallati

Optimising traffic signals is crucial for mitigating urban congestion, and automated planning, particularly with PDDL+, has shown promise for real-world deployment due to its flexibility and centralised perspective. While existing PDDL+ models guarantee deployability on current infrastructure, they face significant limitations: reliance on domain-independent heuristics restricts their applicability and scalability, leading to slow solution generation and unclear plan quality. To overcome these challenges and unlock the widespread adoption of planning-based traffic control, we introduce hCAFE, a domain-specific heuristic for PDDL+-based traffic signal optimisation. Unlike prior approaches, hCAFE is designed to work effectively across multiple problem encodings, addressing a key limitation of traditional domain-specific heuristics. We demonstrate its capabilities on real-world data from a region of the UK, showing significant improvements in solution generation time and search space exploration. Our evaluation also compares the strategies generated by hCAFE against historical data from existing traffic control systems and a non-deployable benchmark, confirming the high quality of the resulting plans.

PDF Details DOI

AAAI Conference 2026 Conference Paper

A Simple Proof-Theoretic Characterization of Stable Models: Reduction to Difference Logic and Experiments (Abstract Reprint)

  • Martin Gebser
  • Enrico Giunchiglia
  • Marco Maratea
  • Marco Mochi

Stable models of logic programs have been studied and characterized in relation with other formalisms by many researchers. As already argued in previous papers, such characterizations are interesting for diverse reasons, including theoretical investigations and the possibility of leading to new algorithms for computing stable models of logic programs. At the theoretical level, complexity and expressiveness comparisons have brought about fundamental insights. Beyond that, practical implementations of the developed reductions enable the use of existing solvers for other logical formalisms to compute stable models. In this paper, we first provide a simple characterization of stable models that can be viewed as a proof-theoretic counterpart of the standard model-theoretic definition. We further show how it can be naturally encoded in difference logic. Such an encoding, compared to the existing reductions to classical logics, does not require Boolean variables. Then, we implement our novel translation to a Satisfiability Modulo Theories (SMT) formula. We finally compare our approach, employing the SMT solver yices, to the translation-based ASP solver lp2diff and to clingo on domains from the “Basic Decision” track of the 2017 Answer Set Programming competition. The results show that our approach is competitive to and often better than lp2diff, and that it can also be faster than clingo on non-tight domains.

PDF Details DOI

AIJ Journal 2026 Journal Article

Symbolic pattern planning

  • Matteo Cardellini
  • Enrico Giunchiglia
  • Marco Maratea

In this paper, we propose a novel approach for solving automated planning problems, called Symbolic Pattern Planning. Given a deterministic planning problem Π, we propose to compute a plan by first fixing a pattern –defined as an arbitrary sequence of actions– and then define a formula encoding the state resulting from the sequential execution of the actions in the pattern, starting from an arbitrary initial state. By allowing each action in the pattern to be executed consecutively zero, one or possibly more times, and by imposing the conditions on the initial and goal states, we can check whether the pattern allows determining a valid plan or whether the pattern needs to be extended and the procedure iterated. We ground our proposal in the numeric planning setting, we prove the correctness and also the completeness of the procedure (provided at each iteration the pattern is extended with a complete sequence of actions), and we define procedures for the pattern selection and for computing quality plans. When exploiting the planning as satisfiability approach, we show that our encoding allows to determine a valid plan in a number of iterations which is never higher than the one needed by the state-of-the-art rolled-up or relaxed-relaxed-∃ symbolic encodings. On the experimental side, we run an extensive analysis which included the problems and systems involved in the numeric track of the 2023 International Planning Competition, showing that the results validate the theoretical findings and that our planner Patty has remarkably good comparative performances.

Details DOI

AAAI Conference 2026 System Paper

Traffic Signal Plans Explorer: A General Framework for Visualising Traffic Evolution

  • Francesco Doria
  • Francesco Percassi
  • Marco Maratea
  • Mauro Vallati

We present the Traffic Signal Plans Explorer, a framework for visualising and exploring traffic signal plans generated via PDDL+ planning. Designed to support both traffic experts and non-specialists, the tool offers a web-based interface for high-level network analysis and a SUMO-based adapter for detailed simulation. Users can inspect junction settings and link dynamics, and simulate plan execution step by step. The system bridges planning technology with practical traffic control, enhancing the transparency and usability of automatically generated solutions.

PDF Details DOI

IJCAI Conference 2025 Conference Paper

A General Framework for Representing Controlled Natural Language Sentences and Translation to KR Formalisms

  • Simone Caruso
  • Carmine Dodaro
  • Marco Maratea
  • Alice Tarzariol

Languages for Knowledge Representation and Reasoning, such as ASP, CP, and SMT, excel at solving some complex problems, but encoding them into a higher-level language may be more profitable, leaving these formalisms as targets for solving. Recent studies aim to convert controlled natural languages into formal representations, yet these solutions are often tailored to specific languages and require significant effort. This paper introduces a general framework that generates grammars for target representation languages, enabling the translation of problems stated in CNL into formal representations. The related system, CNLWizard, offers a flexible, high-level approach to defining desired grammars, significantly reducing the time and effort needed to create custom grammars. Finally, we demonstrate the system's effectiveness through an experimental analysis.

PDF Details DOI

AIJ Journal 2025 Journal Article

A simple proof-theoretic characterization of stable models: Reduction to difference logic and experiments

  • Martin Gebser
  • Enrico Giunchiglia
  • Marco Maratea
  • Marco Mochi

Stable models of logic programs have been studied and characterized in relation with other formalisms by many researchers. As already argued in previous papers, such characterizations are interesting for diverse reasons, including theoretical investigations and the possibility of leading to new algorithms for computing stable models of logic programs. At the theoretical level, complexity and expressiveness comparisons have brought about fundamental insights. Beyond that, practical implementations of the developed reductions enable the use of existing solvers for other logical formalisms to compute stable models. In this paper, we first provide a simple characterization of stable models that can be viewed as a proof-theoretic counterpart of the standard model-theoretic definition. We further show how it can be naturally encoded in difference logic. Such an encoding, compared to the existing reductions to classical logics, does not require Boolean variables. Then, we implement our novel translation to a Satisfiability Modulo Theories (SMT) formula. We finally compare our approach, employing the SMT solver yices, to the translation-based ASP solver lp2diff and to clingo on domains from the “Basic Decision” track of the 2017 Answer Set Programming competition. The results show that our approach is competitive to and often better than lp2diff, and that it can also be faster than clingo on non-tight domains.

Details DOI

IJCAI Conference 2024 Conference Paper

AMO-aware Aggregates in Answer Set Programming

  • Mario Alviano
  • Carmine Dodaro
  • Salvatore Fiorentino
  • Marco Maratea

Aggregates such as sum and count are among the most frequently used linguistic extensions of Answer Set Programming (ASP). At-most-one (AMO) constraints are a specific form of aggregates that excludes the simultaneous truth of multiple elements in a set. This article unleashes a powerful propagation strategy in case groups of elements in an aggregate are also involved in AMO constraints. In fact, the combined knowledge given by aggregates and AMO constraints significantly increases the effectiveness of search space pruning, resulting in sensible performance gains.

PDF Details DOI

EAAI Journal 2024 Journal Article

Digital workflow for printability checking and prefabrication in robotic construction 3D printing based on Artificial Intelligence planning

  • Erfan Shojaei Barjuei
  • Alessio Capitanelli
  • Riccardo Bertolucci
  • Eric Courteille
  • Fulvio Mastrogiovanni
  • Marco Maratea

This paper introduces an innovative digital workflow for printability checking and prefabrication in robotic construction 3D printing based on Artificial Intelligence (AI) planning techniques. The proposed method generates operational sequences for a robotic manipulator tasked with concrete 3D printing by utilizing Planning Domain Definition Language (PDDL) 2. 1-based AI planners. The planned sequences consider diverse geometry specifications, aligning with printability checks and prefabrication requisites. The sequences can then be executed in a robotic simulation environment, allowing operators to assess the 3D printing process in every aspect before real-world deployment, and potentially avoiding costly mistakes and the waste of resources. Compared to existing methods, the use of AI planning makes our approach more modular and easy to adapt across a variety of robotic platforms, diverse designs, materials, and printing conditions; and it is released as open-source software to the benefit of the community. The proposed method was tested by processing objects with multiple geometries and a varying number of printing layers, and by employing two different PDDL planners. Results prove the viability of the approach but also hint at possible scalability limitations for complex geometries that involve a large number of edges to be printed.

Details DOI

AAAI Conference 2024 Conference Paper

Symbolic Numeric Planning with Patterns

  • Matteo Cardellini
  • Enrico Giunchiglia
  • Marco Maratea

In this paper, we propose a novel approach for solving linear numeric planning problems, called Symbolic Pattern Planning. Given a planning problem Pi, a bound n and a pattern --defined as an arbitrary sequence of actions-- we encode the problem of finding a plan for Pi with bound n as a formula with fewer variables and/or clauses than the state-of-the-art rolled-up and relaxed-relaxed-exists encodings. More importantly, we prove that for any given bound, it is never the case that the latter two encodings allow finding a valid plan while ours does not. On the experimental side, we consider 6 other planning systems --including the ones which participated in this year's International Planning Competition (IPC)-- and we show that our planner Patty has remarkably good comparative performances on this year's IPC problems.

PDF Details DOI

ICAPS Conference 2024 Conference Paper

Taming Discretised PDDL+ through Multiple Discretisations

  • Matteo Cardellini
  • Marco Maratea
  • Francesco Percassi
  • Enrico Scala
  • Mauro Vallati

The PDDL+ formalism allows the use of planning techniques in applications that require the ability to perform hybrid discrete-continuous reasoning. PDDL+ problems are notoriously challenging to tackle, and to reason upon them a well-established approach is discretisation. Existing systems rely on a single discretisation delta or, at most, two: a simulation delta to model the dynamics of the environment, and a planning delta, that is used to specify when decisions can be taken. However, there exist cases where this rigid schema is not ideal, for instance when agents with very different speeds need to cooperate or interact in a shared environment, and a more flexible approach that can accommodate more deltas is necessary. To address the needs of this class of hybrid planning problems, in this paper we introduce a reformulation approach that allows the encapsulation of different levels of discretisation in PDDL+ models, hence allowing any domain-independent planning engine to reap the benefits. Further, we provide the community with a new set of benchmarks that highlights the limits of fixed discretisation.

Details

SoCS Conference 2024 Conference Paper

Taming Discretised PDDL+ through Multiple Discretisations (Extended Abstract)

  • Matteo Cardellini
  • Marco Maratea
  • Francesco Percassi
  • Enrico Scala
  • Mauro Vallati

The PDDL+ formalism allows the use of planning techniques in applications that require the ability to perform hybrid discrete-continuous reasoning. PDDL+ problems are notoriously challenging to tackle, and to reason upon them a well-established approach is discretisation. Existing systems rely on a single discretisation delta or, at most, two: a simulation delta to model the dynamics of the environment, and a planning delta, that is used to specify when decisions can be taken. However, there exist cases where this rigid schema is not ideal, for instance when agents with very different speeds need to cooperate or interact in a shared environment, and a more flexible approach that can accommodate more deltas is necessary. To address the needs of this class of hybrid planning problems, in this paper we introduce a reformulation approach that allows the encapsulation of different levels of discretisation in PDDL+ models, hence allowing any domain-independent planning engine to reap the benefits. Further, we provide the community with a new set of benchmarks that highlights the limits of fixed discretisation.

Details

JELIA Conference 2023 Conference Paper

Comparing Planning Domain Models Using Answer Set Programming

  • Lukás Chrpa
  • Carmine Dodaro
  • Marco Maratea
  • Marco Mochi
  • Mauro Vallati

Abstract Automated planning is a prominent area of Artificial Intelligence, and an important component for intelligent autonomous agents. A critical aspect of domain-independent planning is the domain model, that encodes a formal representation of domain knowledge needed to reason upon a given problem. Despite the crucial role of domain models in automated planning, there is lack of tools supporting knowledge engineering process by comparing different versions of the models, in particular, determining and highlighting differences the models have. In this paper, we build on the notion of strong equivalence of domain models and formalise a novel concept of similarity of domain models. To measure the similarity of two models, we introduce a directed graph representation of lifted domain models that allows to formulate the domain model similarity problem as a variant of the graph edit distance problem. We propose an Answer Set Programming approach to optimally solve the domain model similarity problem, that identifies the minimum number of modifications the models need to become strongly equivalent, and we demonstrate the capabilities of the approach on a range of benchmark models.

Details

AIJ Journal 2022 Journal Article

Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving

  • Thomas Linsbichler
  • Marco Maratea
  • Andreas Niskanen
  • Johannes P. Wallner
  • Stefan Woltran

dialectical frameworks (ADFs) constitute one of the most powerful formalisms in abstract argumentation. Their high computational complexity poses, however, certain challenges when designing efficient systems. In this paper, we tackle this issue by (i) analyzing the complexity of ADFs under structural restrictions, (ii) presenting novel algorithms which make use of these insights, and (iii) implementing these algorithms via (multiple) calls to SAT solvers. An empirical evaluation of the resulting implementation on ADF benchmarks generated from ICCMA competitions shows that our solver is able to outperform state-of-the-art ADF systems.

Details DOI

SoCS Conference 2021 Conference Paper

A Planning-based Approach for In-Station Train Dispatching

  • Matteo Cardellini
  • Marco Maratea
  • Mauro Vallati
  • Gianluca Boleto
  • Luca Oneto

In-station train dispatching is the problem of optimising the effective utilisation of available railway infrastructures for mitigating incidents and delays. In this paper, we describe an approach for dealing with the in-station dispatching problem by means of automated planning techniques.

Details

ICAPS Conference 2021 Conference Paper

In-Station Train Dispatching: A PDDL+ Planning Approach

  • Matteo Cardellini
  • Marco Maratea
  • Mauro Vallati
  • Gianluca Boleto
  • Luca Oneto

In railway networks, stations are probably the most critical points for interconnecting trains' routes: in a restricted geographical area, a potentially large number of trains have to stop according to an official timetable, with the concrete risk of accumulating delays that can then have a knockout effect on the rest of the network. In this context, in-station train dispatching plays a central role in maximising the effective utilisation of available railway infrastructures and in mitigating the impact of incidents and delays. Unfortunately, in-station train dispatching is still largely handled manually by human operators in charge of a group of stations. In this paper we make a step towards supporting the operator with some automatic tool, by describing an approach for performing in-station dispatching by means of automated planning techniques. Given the mixed discrete-continuous nature of the problem, we employ PDDL+ for the specification of the problem, and the ENHSP planning engine enhanced by domain-specific solving techniques. Results on a range of scenarios, using real-data of a station of the North West of Italy, show the potential of our approach.

Details

IJCAI Conference 2020 Conference Paper

A Formal Approach for Cautious Reasoning in Answer Set Programming (Extended Abstract)

  • Giovanni Amendola
  • Carmine Dodaro
  • Marco Maratea

The issue of describing in a formal way solving algorithms in various fields such as Propositional Satisfiability (SAT), Quantified SAT, Satisfiability Modulo Theories, Answer Set Programming (ASP), and Constraint ASP, has been relatively recently solved employing abstract solvers. In this paper we deal with cautious reasoning tasks in ASP, and design, implement and test novel abstract solutions, borrowed from backbone computation in SAT. By employing abstract solvers, we also formally show that the algorithms for solving cautious reasoning tasks in ASP are strongly related to those for computing backbones of Boolean formulas. Some of the new solutions have been implemented in the ASP solver WASP, and tested.

PDF Details DOI

AIJ Journal 2020 Journal Article

Design and results of the Second International Competition on Computational Models of Argumentation

  • Sarah A. Gaggl
  • Thomas Linsbichler
  • Marco Maratea
  • Stefan Woltran

Argumentation is a major topic in the study of Artificial Intelligence. Since the first edition in 2015, advancements in solving (abstract) argumentation frameworks are assessed in competition events, similar to other closely related problem solving technologies. In this paper, we report about the design and results of the Second International Competition on Computational Models of Argumentation, which has been jointly organized by TU Dresden (Germany), TU Wien (Austria), and the University of Genova (Italy), in affiliation with the 2017 International Workshop on Theory and Applications of Formal Argumentation. This second edition maintains some of the design choices made in the first event, e. g. the I/O formats, the basic reasoning problems, and the organization into tasks and tracks. At the same time, it introduces significant novelties, e. g. three additional prominent semantics, and an instance selection stage for classifying instances according to their empirical hardness.

Details DOI

IJCAI Conference 2018 Conference Paper

Evaluation Techniques and Systems for Answer Set Programming: a Survey

  • Martin Gebser
  • Nicola Leone
  • Marco Maratea
  • Simona Perri
  • Francesco Ricca
  • Torsten Schaub

Answer set programming (ASP) is a prominent knowledge representation and reasoning paradigm that found both industrial and scientific applications. The success of ASP is due to the combination of two factors: a rich modeling language and the availability of efficient ASP implementations. In this paper we trace the history of ASP systems, describing the key evaluation techniques and their implementation in actual tools.

PDF Details

IJCAI Conference 2018 Conference Paper

Novel Algorithms for Abstract Dialectical Frameworks based on Complexity Analysis of Subclasses and SAT Solving

  • Thomas Linsbichler
  • Marco Maratea
  • Andreas Niskanen
  • Johannes P. Wallner
  • Stefan Woltran

Abstract dialectical frameworks (ADFs) constitute one of the most powerful formalisms in abstract argumentation. Their high computational complexity poses, however, certain challenges when designing efficient systems. In this paper, we tackle this issue by (i) analyzing the complexity of ADFs under structural restrictions, (ii) presenting novel algorithms which make use of these insights, and (iii) empirically evaluating a resulting implementation which relies on calls to SAT solvers.

PDF Details

JAIR Journal 2017 Journal Article

The Sixth Answer Set Programming Competition

  • Martin Gebser
  • Marco Maratea
  • Francesco Ricca

Answer Set Programming (ASP) is a well-known paradigm of declarative programming with roots in logic programming and non-monotonic reasoning. Similar to other closely related problem-solving technologies, such as SAT/SMT, QBF, Planning and Scheduling, advancements in ASP solving are assessed in competition events. In this paper, we report about the design and results of the Sixth ASP Competition, which was jointly organized by the University of Calabria (Italy), Aalto University (Finland), and the University of Genoa (Italy), in affiliation with the 13th International Conference on Logic Programming and Non-Monotonic Reasoning. This edition maintained some of the design decisions introduced in 2014, e.g., the conception of sub-tracks, the scoring scheme, and the adherence to a fixed modeling language in order to push the adoption of the ASP-Core-2 standard. On the other hand, it featured also some novelties, like a benchmark selection stage classifying instances according to their empirical hardness, and a "Marathon" track where the top-performing systems are given more time for solving hard benchmarks.

PDF Details DOI

AIJ Journal 2016 Journal Article

Design and results of the Fifth Answer Set Programming Competition

  • Francesco Calimeri
  • Martin Gebser
  • Marco Maratea
  • Francesco Ricca

Answer Set Programming (ASP) is a well-established paradigm of declarative programming that has been developed in the field of logic programming and non-monotonic reasoning. Advances in ASP solving technology are customarily assessed in competition events, as it happens for other closely related problem solving areas such as Boolean Satisfiability, Satisfiability Modulo Theories, Quantified Boolean Formulas, Planning, etc. This paper reports about the fifth edition of the ASP Competition by covering all aspects of the event, ranging from the new design of the competition to an in-depth analysis of the results. The paper comprises also additional analyses that were conceived for measuring the progress of the state of the art, as well as for studying aspects orthogonal to solving technology, such as the effects of modeling. A detailed picture of the progress of the state of the art in ASP solving is drawn, and the ASP Competition is located in the spectrum of related events.

Details DOI

AAAI Conference 2016 Conference Paper

What’s Hot in the Answer Set Programming Competition

  • Martin Gebser
  • Marco Maratea
  • Francesco Ricca

Answer Set Programming (ASP) is a declarative programming paradigm with roots in logic programming, knowledge representation, and non-monotonic reasoning. The ASP competition series aims at assessing and promoting the evolution of ASP systems and applications. Its growing range of challenging application-oriented benchmarks inspires and showcases continuous advancements of the state of the art in ASP.

PDF Details

ECAI Conference 2014 Conference Paper

Abstract Disjunctive Answer Set Solvers

  • Rémi Brochenin
  • Yuliya Lierler
  • Marco Maratea

A fundamental task in answer set programming is to compute answer sets of logic programs. Answer set solvers are the programs that perform this task. The problem of deciding whether a disjunctive program has an answer set is Σ P2

Details

ICAPS Conference 2013 Conference Paper

Modeling and Reasoning about Business Processes under Authorization Constraints: A Planning-Based Approach

  • Alessandro Armando
  • Enrico Giunchiglia
  • Marco Maratea
  • Serena Elisa Ponta

Business processes under authorization control are sets of coordinated activities subject to a security policy stating which agent can access which resource. Their behavior is difficult to predict due to the complex and unexpected interleaving of different execution flows within the process. Therefore, serious flaws may go undetected and manifest themselves only after deployment. This problem may be tackled by applying formal methods to reason about business process models. In this paper we outline the main contributions in this application domain of (Armando et al. 2012), that uses the action-based planning language C and the Causal Calculator tool CCalc. C is used to specify a business process from the banking domain that is representative of an important class of business processes of practical relevance, and proved to be a rich and natural formal specification language in this domain. CCalc is then used to automatically solve three reasoning tasks that arise in this context. We also compare C with the SMV specification language used in model-checking: the comparison highlights some key advantages of C in the business process domain.

Details

JELIA Conference 2012 Conference Paper

The Multi-Engine ASP Solver me-asp

  • Marco Maratea
  • Luca Pulina
  • Francesco Ricca

Abstract In this paper we describe the new system me-asp, which applies machine learning techniques for inductively choosing, among a set of available ones, the “best” ASP solver on a per-instance basis. Moreover, we report the results of some experiments, carried out on benchmarks from the “System Track” of the 3rd ASP Competition, showing the state-of-the-art performance of our solver.

Details

JELIA Conference 2010 Conference Paper

DLV MC: Enhanced Model Checking in DLV

  • Marco Maratea
  • Francesco Ricca
  • Pierfrancesco Veltri

Abstract Stable Model Checking (MC) in Answer Set Programming systems is, in general, a co-NP task for disjunctive programs. Thus, implementing an efficient strategy is very important for the performance of ASP systems. In DLV, MC is carried out by exploiting the SAT solver SATZ, and the result of this operation also returns (in case the check fails) an ”unfounded set”, as by-product, which is also used for pruning the search space during answer set computation. In this paper we report on the integration of a “modern” SAT solver, MiniSAT, in DLV. The integration poses not only technological issues, but also challenges w. r. t. the ”quality” of the returned unfounded set and w. r. t. the interplay with the existing DLV techniques.

Details

ECAI Conference 2008 Conference Paper

A new Approach for Solving Satisfiability Problems with Qualitative Preferences

  • Emanuele Di Rosa
  • Enrico Giunchiglia
  • Marco Maratea

The problem of expressing and solving satisfiability problems (SAT) with qualitative preferences is central in many areas of Computer Science and Artificial Intelligence. In previous papers, it has been shown that qualitative preferences on literals allow for capturing qualitative/quantitative preferences on literals/formulas; and that an optimal model for a satisfiability problems with qualitative preferences on literals can be computed via a simple modification of the Davis-Logemann-Loveland procedure (DLL): Given a SAT formula, an optimal solution is computed by simply imposing that DLL branches according to the partial order on the preferences. Unfortunately, it is well known that introducing an ordering on the branching heuristic of DLL may cause an exponential degradation in its performances. The experimental analysis reported in these papers hightlights that such degradation can indeed show up in the presence of a significant number of preferences.

Details

JELIA Conference 2006 Conference Paper

optsat: A Tool for Solving SAT Related Optimization Problems

  • Enrico Giunchiglia
  • Marco Maratea

Abstract Propositional satisfiability (SAT) is one of the most important and central problems in Artificial Intelligence and Computer Science. Basically, most SAT solvers are based on the well-known Davis-Logemann-Loveland (DLL) procedure. DLL is a decision procedure: given a SAT formula φ, it can decide if φ is satisfiable (and it can return a satisfying assignment μ ), or not. Often, this is not suffi- cient, in that we would like μ to be also “optimal”, i. e. , that has also to minimize/ maximize a given objective function. max-sat, min-one, distance-sat and their weighted versions are popular optimization problems. (In the following, φ is the input formula expressed as a set of clauses). Almost all the systems that can deal with these problems follow a classical branch&bound schema: whenever a satisfying assignment μ for φ with a cost c μ is found, the search goes on looking for another satisfying assignment with a lower (or higher, depending on the problem) cost.

Details

ECAI Conference 2006 Conference Paper

Solving Optimization Problems with DLL

  • Enrico Giunchiglia
  • Marco Maratea

Propositional satisfiability (SAT) is a success story in Computer Science and Artificial Intelligence: SAT solvers are currently used to solve problems in many different application domains, including planning and formal verification. The main reason for this success is that modern SAT solvers can successfully deal with problems having millions of variables. All these solvers are based on the Davis-Logemann-Loveland procedure (DLL). DLL is a decision procedure: Given a formula φ , it returns whether φ is satisfiable or not. Further, DLL can be easily modified in order to return an assignment satisfying φ , assuming one exists. However, in many cases it is not enough to compute a satisfying assignment: Indeed, the returned assignment has also to be “optimal” in some sense, e. g. , it has to minimize/maximize a given objective function. In this paper we show that DLL can be very easily adapted in order to solve optimization problems like MAX-SAT and MIN-ONE. In particular these problems are solved by simply imposing an ordering on a set of literals, to be followed while branching. Other popular problems, like DISTANCE-SAT and WEIGHTED-MAX-SAT, can be solved in a similar way. We implemented these ideas in ZCHAFF and the experimental analysis show that the resulting system is competitive with respect to other state-of-the-art systems.

Details

SAT Conference 2004 Conference Paper

A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints

  • Alessandro Armando
  • Claudio Castellini
  • Enrico Giunchiglia
  • Marco Maratea

The problem of solving boolean combinations of difference constraints is at the core of many important techniques such as planning, scheduling, and model-checking of real-time systems. Efficient decision procedures for this class of formulas are, therefore, strongly needed. In this paper we present TSAT++, a SAT-based open reasoning platform able to decide boolean combinations of difference constraints. Experimental results indicate that TSAT++ outperforms its competitors both on randomly-generated, hand-made and real world problems.

Details

NMR Workshop 2004 Conference Paper

A SAT-based polynomial space algorithm for answer set programming

  • Enrico Giunchiglia
  • Yuliya Lierler
  • Marco Maratea

The relation between answer set programming (ASP) and propositional satisfiability (SAT) is at the center of many research papers, partly because of the tremendous performance boost of SAT solvers during last years. Various translations from ASP to SAT are known but the resulting SAT formula either includes many new variables or may have an unpractical size. There are also well known results showing a one-to-one correspondence between the answer sets of a logic program and the models of its completion. Unfortunately, these results only work for specific classes of problems. In this paper we present a SAT-Based decision procedure for answer set programming that (i) deals with any (non disjunctive) logic program, (ii) works on a SAT formula without additional variables, and (iii) is guaranteed to work in polynomial space. Further, our procedure can be extended to compute all the answer sets still working in polynomial space. The experimental results of a prototypical implementation show that the approach can pay off sometimes by orders of magnitude when computing one solution, and it is competitive when computing all solutions.

Details

JELIA Conference 2002 Conference Paper

Dependent and Independent Variables in Propositional Satisfiability

  • Enrico Giunchiglia
  • Marco Maratea
  • Armando Tacchella

Abstract Propositional reasoning (SAT) is central in many applications of Computer Science. Several decision procedures for SAT have been proposed, along with optimizations and heuristics to speed them up. Currently, the most effective implementations are based on the Davis, Logemann, Loveland method. In this method, the input formula is represented as a set of clauses, and the space of truth assignments is searched by iteratively assigning a literal until all the clauses are satisfied, or a clause is violated and backtracking occurs. Once a new literal is assigned, pruning techniques (e. g. , unit propagation) are used to cut the search space by inferring truth values for other variables. In this paper, we investigate the “independent variable selection (IVS) heuristic”, i. e. , given a formula on the set of variables N, the selection is restricted to a - possibly small - subset S which is suficient to determine a truth value for all the variables in N. During the search phase, scoring and selection of the literal to assign next are restricted to S, and the truth values for the remaining variables are determined by the pruning techniques of the solver. We discuss the possible advantages and disadvantages of the IVS heuristic. Our experimental analysis shows that obtaining either positive or negative results strictly depends on the type of problems considered, on the underlying scoring and selection technique, and also on the backtracking scheme.

Details
v2026.09.13