Arrow Research search

Author name cluster

António Morgado 0001

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.

12 papers
1 author row

Possible papers

12

SAT Conference 2020 Conference Paper

SAT-Based Encodings for Optimal Decision Trees with Explicit Paths

  • Mikolás Janota
  • António Morgado 0001

Abstract Decision trees play an important role both in Machine Learning and Knowledge Representation. They are attractive due to their immediate interpretability. In the spirit of Occam’s razor, and interpretability, it is desirable to calculate the smallest tree. This, however, has proven to be a challenging task and greedy approaches are typically used to learn trees in practice. Nevertheless, recent work showed that by the use of SAT solvers one may calculate the optimal size tree for real-world benchmarks. This paper proposes a novel SAT-based encoding that explicitly models paths in the tree, which enables us to control the tree’s depth as well as size. At the level of individual SAT calls, we investigate splitting the search space into tree topologies. Our tool outperforms the existing implementation. But also, the experimental results show that minimizing the depth first and then minimizing the number of nodes enables solving a larger set of instances.

Details

SAT Conference 2019 Conference Paper

DRMaxSAT with MaxHS: First Contact

  • António Morgado 0001
  • Alexey Ignatiev
  • Maria Luisa Bonet
  • João Marques-Silva 0001
  • Sam Buss

Abstract The proof system of Dual-Rail MaxSAT (DRMaxSAT) was recently shown to be capable of efficiently refuting families of formulas that are well-known to be hard for resolution, concretely when the MaxSAT solving approach is either MaxSAT resolution or core-guided algorithms. Moreover, DRMaxSAT based on MaxSAT resolution was shown to be stronger than general resolution. Nevertheless, existing experimental evidence indicates that the use of MaxSAT algorithms based on the computation of minimum hitting sets (MHSes), i. e. MaxHS-like algorithms, are as effective, and often more effective, than core-guided algorithms and algorithms based on MaxSAT resolution. This paper investigates the use of MaxHS-like algorithms in the DRMaxSAT proof system. Concretely, the paper proves that the propositional encoding of the pigenonhole and doubled pigenonhole principles have polynomial time refutations when the DRMaxSAT proof system uses a MaxHS-like algorithm.

Details

SAT Conference 2018 Conference Paper

PySAT: A Python Toolkit for Prototyping with SAT Oracles

  • Alexey Ignatiev
  • António Morgado 0001
  • João Marques-Silva 0001

Abstract Boolean satisfiability (SAT) solvers are at the core of efficient approaches for solving a vast multitude of practical problems. Moreover, albeit targeting an NP-complete problem, SAT solvers are increasingly used for tackling problems beyond NP. Despite the success of SAT in practice, modeling with SAT and more importantly implementing SAT-based problem solving solutions is often a difficult and error-prone task. This paper proposes the PySAT toolkit, which enables fast Python-based prototyping using SAT oracles and SAT-related technology. PySAT provides a simple API for working with a few state-of-the-art SAT oracles and also integrates a number of cardinality constraint encodings, all aiming at simplifying the prototyping process. Experimental results presented in the paper show that PySAT-based implementations can be as efficient as those written in a low-level language.

Details

SAT Conference 2017 Conference Paper

On Tackling the Limits of Resolution in SAT Solving

  • Alexey Ignatiev
  • António Morgado 0001
  • João Marques-Silva 0001

Abstract The practical success of Boolean Satisfiability (SAT) solvers stems from the CDCL (Conflict-Driven Clause Learning) approach to SAT solving. However, from a propositional proof complexity perspective, CDCL is no more powerful than the resolution proof system, for which many hard examples exist. This paper proposes a new problem transformation, which enables reducing the decision problem for formulas in conjunctive normal form (CNF) to the problem of solving maximum satisfiability over Horn formulas. Given the new transformation, the paper proves a polynomial bound on the number of MaxSAT resolution steps for pigeonhole formulas. This result is in clear contrast with earlier results on the length of proofs of MaxSAT resolution for pigeonhole formulas. The paper also establishes the same polynomial bound in the case of modern core-guided MaxSAT solvers. Experimental results, obtained on CNF formulas known to be hard for CDCL SAT solvers, show that these can be efficiently solved with modern MaxSAT solvers.

Details

ECAI Conference 2016 Conference Paper

Propositional Abduction with Implicit Hitting Sets

  • Alexey Ignatiev
  • António Morgado 0001
  • João Marques-Silva 0001

Logic-based abduction finds important applications in artificial intelligence and related areas. One application example is in finding explanations for observed phenomena. Propositional abduction is a restriction of abduction to the propositional domain, and complexity-wise is in the second level of the polynomial hierarchy. Recent work has shown that exploiting implicit hitting sets and propositional satisfiability (SAT) solvers provides an efficient approach for propositional abduction. This paper investigates this earlier work and proposes a number of algorithmic improvements. These improvements are shown to yield exponential reductions in the number of SAT solver calls. More importantly, the experimental results show significant performance improvements compared to the the best approaches for propositional abduction.

Details

ECAI Conference 2014 Conference Paper

Efficient Autarkies

  • João Marques-Silva 0001
  • Alexey Ignatiev
  • António Morgado 0001
  • Vasco Manquinho
  • Inês Lynce

Autarkies are partial truth assignments that satisfy all clauses having literals in the assigned variables. Autarkies provide important information in the analysis of unsatisfiable formulas. Indeed, clauses satisfied by autarkies cannot be included in minimal explanations or in minimal corrections of unsatisfiability. Computing the maximum autarky allows identifying all such clauses. In recent years, a number of alternative approaches have been proposed for computing a maximum autarky. This paper develops new models for representing autarkies, and proposes new algorithms for computing the maximum autarky. Experimental results, obtained on a large number of problem instances, show orders of magnitude performance improvements over existing approaches, and solving instances that could not otherwise be solved.

Details

SAT Conference 2014 Conference Paper

On Reducing Maximum Independent Set to Minimum Satisfiability

  • Alexey Ignatiev
  • António Morgado 0001
  • João Marques-Silva 0001

Abstract Maximum Independent Set (MIS) is a well-known NP-hard graph problem, tightly related with other well known NP-hard graph problems, namely Minimum Vertex Cover (MVC) and Maximum Clique (MaxClq). This paper introduces a novel reduction of MIS into Minimum Satisfiability (MinSAT), thus, providing an alternative approach for solving MIS. The reduction naturally maps the vertices of a graph into clauses, without requiring the inclusion of hard clauses. Moreover, it is shown that the proposed reduction uses fewer variables and clauses than the existing alternative of mapping MIS into Maximum Satisfiability (MaxSAT). The paper develops a number of optimizations to the basic reduction, which significantly reduce the total number of variables used. The experimental evaluation considered the reductions described in the paper as well as existing state-of-the-art approaches. The results show that the proposed approaches based on MinSAT are competitive with existing approaches.

Details

ECAI Conference 2014 Conference Paper

Progression in Maximum Satisfiability

  • Alexey Ignatiev
  • António Morgado 0001
  • Vasco Manquinho
  • Inês Lynce
  • João Marques-Silva 0001

Maximum Satisfiability (MaxSAT) is a well-known optimization version of Propositional Satisfiability (SAT), that finds a wide range of relevant practical applications. Despite the significant progress made in MaxSAT solving in recent years, many practically relevant problem instances require prohibitively large run times, and many cannot simply be solved with existing algorithms. One approach for solving MaxSAT is based on iterative SAT solving, which may optionally be guided by unsatisfiable cores. A difficulty with this class of algorithms is the possibly large number of times a SAT solver is called, e. g. for instances with very large clause weights. This paper proposes the use of geometric progressions to tackle this issue, thus allowing, for the vast majority of problem instances, to reduce the number of calls to the SAT solver. The new approach is also shown to be applicable to core-guided MaxSAT algorithms. Experimental results, obtained on a large number of problem instances, show gains when compared to state-of-the-art implementations of MaxSAT algorithms.

Details

LPAR Conference 2013 Conference Paper

Maximal Falsifiability - Definitions, Algorithms, and Applications

  • Alexey Ignatiev
  • António Morgado 0001
  • Jordi Planes
  • João Marques-Silva 0001

Abstract Similarly to Maximum Satisfiability (MaxSAT), Minimum Satisfiability (MinSAT) is an optimization extension of the Boolean Satisfiability (SAT) decision problem. In recent years, both problems have been studied in terms of exact and approximation algorithms. In addition, the MaxSAT problem has been characterized in terms ofMaximal Satisfiable Subsets (MSSes) andMinimal Correction Subsets (MCSes), as well as Minimal Unsatisfiable Subsets (MUSes) and minimal hitting set dualization. However, and in contrast with MaxSAT, no such characterizations exist for MinSAT. This paper addresses this issue by casting the MinSAT problem in a more general framework. The paper studies Maximal Falsifiability, the problem of computing a subset-maximal set of clauses that can be simultaneously falsified, and shows that MinSAT corresponds to the complement of a largest subset-maximal set of simultaneously falsifiable clauses, i. e. the solution of the Maximum Falsifiability (MaxFalse) problem. Additional contributions of the paper include novel algorithms for Maximum and Maximal Falsifiability, as well as minimal hitting set dualization results for the MaxFalse problem. Moreover, the proposed algorithms are validated on practical instances.

Details

LPAR Conference 2013 Conference Paper

SAT-Based Preprocessing for MaxSAT

  • Anton Belov
  • António Morgado 0001
  • João Marques-Silva 0001

Abstract State-of-the-art algorithms for industrial instances of MaxSAT problem rely on iterative calls to a SAT solver. Preprocessing is crucial for the acceleration of SAT solving, and the key preprocessing techniques rely on the application of resolution and subsumption elimination. Additionally, satisfiability-preserving clause elimination procedures are often used. Since MaxSAT computation typically involves a large number of SAT calls, we are interested in whether an input instance to a MaxSAT problem can be preprocessed up-front, i. e. prior to running the MaxSAT solver, rather than (or, in addition to) during each iterative SAT solver call. The key requirement in this setting is that the preprocessing has to be sound, i. e. so that the solution can be reconstructed correctly and efficiently after the execution of a MaxSAT algorithm on the preprocessed instance. While, as we demonstrate in this paper, certain clause elimination procedures are sound for MaxSAT, it is well-known that this is not the case for resolution and subsumption elimination. In this paper we show how to adapt these preprocessing techniques to MaxSAT. To achieve this we recast the MaxSAT problem in a recently introduced labelled-CNF framework, and show that within the framework the preprocessing techniques can be applied soundly. Furthermore, we show that MaxSAT algorithms restated in the framework have a natural implementation on top of an incremental SAT solver. We evaluate the prototype implementation of a MaxSAT algorithm WMSU1 in this setting, demonstrate the effectiveness of preprocessing, and show overall improvement with respect to non-incremental versions of the algorithm on some classes of problems.

Details

SAT Conference 2012 Conference Paper

Improvements to Core-Guided Binary Search for MaxSAT

  • António Morgado 0001
  • Federico Heras
  • João Marques-Silva 0001

Abstract Maximum Satisfiability (MaxSAT ) and its weighted variants are well-known optimization formulations of Boolean Satisfiability ( SAT ). Motivated by practical applications, recent years have seen the development of core-guided algorithms for MaxSAT. Among these, core-guided binary search with disjoint cores ( BCD ) represents a recent robust solution. This paper identifies a number of inefficiencies in the original BCD algorithm, related with the computation of lower and upper bounds during the execution of the algorithm, and develops solutions for them. In addition, the paper proposes two additional novel techniques, which can be implemented on top of core-guided MaxSAT algorithms that maintain both lower and upper bounds. Experimental results, obtained on representative problem instances, indicate that the proposed optimizations yield significant performance gains, and allow solving more problem instances.

Details

SAT Conference 2006 Conference Paper

Counting Models in Integer Domains

  • António Morgado 0001
  • Paulo J. Matos
  • Vasco Manquinho
  • João Marques-Silva 0001

Abstract This paper addresses the problem of counting models in integer linear programming (ILP) using Boolean Satisfiability (SAT) techniques, and proposes two approaches to solve this problem. The first approach consists of encoding ILP instances into pseudo-Boolean (PB) instances. Moreover, the paper introduces a model counter for PB constraints, which can be used for counting models in PB as well as in ILP. A second alternative approach consists of encoding instances of ILP into instances of SAT. A two-step procedure is proposed, consisting of first mapping the ILP instance into PB constraints and then encoding the PB constraints into SAT. One key observation is that not all existing PB to SAT encodings can be used for counting models. The paper provides conditions for PB to SAT encodings that can be safely used for model counting, and proves that some of the existing encodings are safe for model counting while others are not. Finally, the paper provides experimental results, comparing the PB and SAT approaches, as well as existing alternative solutions.

Details