Minimal sets on propositional formulae. Problems and reductions

DOI10.1016/J.ARTINT.2017.07.005zbMATH Open1419.68098arXiv1402.3011OpenAlexW2740761706MaRDI QIDQ1677431FDOQ1677431

Mikoláš Janota, Carlos Mencía, Joao Marques-Silva

Publication date: 21 November 2017

Published in: Artificial Intelligence (Search for Journal in Brave)

Abstract: Boolean Satisfiability (SAT) is arguably the archetypical NP-complete decision problem. Progress in SAT solving algorithms has motivated an ever increasing number of practical applications in recent years. However, many practical uses of SAT involve solving function as opposed to decision problems. Concrete examples include computing minimal unsatisfiable subsets, minimal correction subsets, prime implicates and implicants, minimal models, backbone literals, and autarkies, among several others. In most cases, solving a function problem requires a number of adaptive or non-adaptive calls to a SAT solver. Given the computational complexity of SAT, it is therefore important to develop algorithms that either require the smallest possible number of calls to the SAT solver, or that involve simpler instances. This paper addresses a number of representative function problems defined on Boolean formulas, and shows that all these function problems can be reduced to a generic problem of computing a minimal set subject to a monotone predicate. This problem is referred to as the Minimal Set over Monotone Predicate (MSMP) problem. This exercise provides new ways for solving well-known function problems, including prime implicates, minimal correction subsets, backbone literals, independent variables and autarkies, among several others. Moreover, this exercise motivates the development of more efficient algorithms for the MSMP problem. Finally the paper outlines a number of areas of future research related with extensions of the MSMP problem.

Full work available at URL: https://arxiv.org/abs/1402.3011

zbMATH Keywords

monotone predicatesindependent supportBoolean satisfiabilityminimal unsatisfiabilityautarkiesbackbone literalsformula entailmentirredundant subformulaemaximal falsifiabilitymaximal satisfiabilityMCSesMESesMFSesminimal and maximal modelsminimal satisfiabilityMUSesprime implicates and implicantsvariable independence

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cites Work

• Theory and Applications of Satisfiability Testing
• A structure-preserving clause form translation
• The complexity of optimization problems
• The complexity of selecting maximal solutions
• Algorithms for computing minimal unsatisfiable subsets of constraints
• On the query complexity of selecting minimal sets for monotone predicates
• Consequence finding algorithms
• Consistent subsets of inconsistent systems: structure and behaviour
• Algorithms for computing backbones of propositional formulae
• Solving satisfiability problems with preferences
• Property-directed incremental invariant generation
• Redundancy in logic. I: CNF propositional formulae
• On computing minimal independent support and its applications to sampling and counting
• Minimally Unsatisfiable Boolean Circuits
• A Way to Simplify Truth Functions
• Locating Minimal Infeasible Constraint Sets in Linear Programs
• A theory of diagnosis from first principles
• Iterative and core-guided maxsat solving: a survey and assessment
• Fast, flexible MUS enumeration
• On Efficient Computation of Variable MUSes
• Constraint satisfaction problems in clausal form. II: Minimal unsatisfiability and conflict structure
• Generating all maximal models of a Boolean expression
• Towards efficient MUS extraction
• A New Approach to Partial MUS Enumeration
• SAT-based MaxSAT algorithms
• Algorithms for computing minimal equivalent subformulas
• Enumerating Infeasibility: Finding Multiple MUSes Quickly
• Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel
• Reasoning with minimal models: efficient algorithms and applications
• On approximation algorithms for the minimum satisfiability problem
• The Minimum Satisfiability Problem
• Opportunistic algorithms for eliminating supersets
• Solving satisfiability in less than \(2^ n\) steps
• An almost optimal algorithm for unbounded searching
• On computing minimal models
• Saturation, nonmonotonic reasoning and the closed-world assumption
• Computer aided verification. 25th international conference, CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings
• Propositional circumscription and extended closed-world reasoning are \(\Pi_ 2^ P\)-complete
• Tools and Algorithms for the Construction and Analysis of Systems
• Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems
• Redundancy in logic. II: 2CNF and Horn propositional formulae
• Redundancy in logic. III: Non-monotonic reasoning
• On Improving MUS Extraction Algorithms
• Autarky pruning in propositional model elimination reduces failure redundancy
• Investigations on autark assignments
• The complexity of logic-based abduction
• Optimizing with minimum satisfiability
• On Reducing Maximum Independent Set to Minimum Satisfiability
• Approximating MIN 2-SAT and MIN 3-SAT
• Computing Maximal Autarkies with Few and Simple Oracle Queries
• A tableau calculus for minimal model reasoning
• On Computing Backbones of Propositional Theories
• On the use of autarkies for satisfiability decision
• Learning to ask relevant questions
• Complexity analysis of propositional resolution with autarky pruning
• MCS Extraction with Sublinear Oracle Queries
• Advanced SAT Techniques for Abstract Argumentation
• Maximal Falsifiability
• Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form
• Identifying Necessary Reactions in Metabolic Pathways by Minimal Model Generation
• SAT-Based Formula Simplification
• On Anti-subsumptive Knowledge Enforcement
• Searching for Autarkies to Trim Unsatisfiable Clause Sets
• MaxSAT-based encodings for Group MaxSAT
• Identifying the Class of Maxi-Consistent Operators in Argumentation
• A Dynamic Programming Approach to Sequential Pattern Recognition
• Verification, Model Checking, and Abstract Interpretation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (13)

• On the query complexity of selecting minimal sets for monotone predicates
• On computing probabilistic abductive explanations
• Extracting unsatisfiable cores for LTL via temporal resolution
• A primal-dual approximation algorithm for \textsc{minsat}
• A logic-algebraic tool for reasoning with knowledge-based systems
• ASP and subset minimality: enumeration, cautious reasoning and MUSes
• On Tackling Explanation Redundancy in Decision Trees
• Timed automata relaxation for reachability
• Extension and equivalence problems for clause minimal formulae
• A memetic algorithm for restoring feasibility in scheduling with limited makespan
• Enumeration of minimal models and MUSes in WASP
• Certified logic-based explainable AI -- the case of monotonic classifiers
• Title not available (Why is that?)

Uses Software

• MiniSat
• JBool
• PicoSAT
• QUICKXPLAIN

This page was built for publication: Minimal sets on propositional formulae. Problems and reductions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1677431)