Minimal sets on propositional formulae. Problems and reductions
From MaRDI portal
Publication:1677431
DOI10.1016/j.artint.2017.07.005zbMath1419.68098arXiv1402.3011OpenAlexW2740761706MaRDI QIDQ1677431
Mikoláš Janota, Carlos Mencía, João P. Marques-Silva
Publication date: 21 November 2017
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1402.3011
Boolean satisfiabilitymonotone predicatesindependent supportminimal unsatisfiabilityautarkiesbackbone literalsformula entailmentirredundant subformulaemaximal falsifiabilitymaximal satisfiabilityMCSesMESesMFSesminimal and maximal modelsminimal satisfiabilityMUSesprime implicates and implicantsvariable independence
Related Items
Extracting unsatisfiable cores for LTL via temporal resolution, On Tackling Explanation Redundancy in Decision Trees, A primal-dual approximation algorithm for \textsc{minsat}, ASP and subset minimality: enumeration, cautious reasoning and MUSes, On computing probabilistic abductive explanations, A memetic algorithm for restoring feasibility in scheduling with limited makespan, Enumeration of minimal models and MUSes in WASP, A logic-algebraic tool for reasoning with knowledge-based systems, Unnamed Item, Timed automata relaxation for reachability, On the query complexity of selecting minimal sets for monotone predicates
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On the query complexity of selecting minimal sets for monotone predicates
- On computing minimal independent support and its applications to sampling and counting
- Fast, flexible MUS enumeration
- Generating all maximal models of a Boolean expression
- Computer aided verification. 25th international conference, CAV 2013, Saint Petersburg, Russia, July 13--19, 2013. Proceedings
- SAT-based MaxSAT algorithms
- Algorithms for computing minimal equivalent subformulas
- Solving satisfiability problems with preferences
- Opportunistic algorithms for eliminating supersets
- Property-directed incremental invariant generation
- Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems
- Saturation, nonmonotonic reasoning and the closed-world assumption
- Solving satisfiability in less than \(2^ n\) steps
- A structure-preserving clause form translation
- A theory of diagnosis from first principles
- The complexity of optimization problems
- Reasoning with minimal models: efficient algorithms and applications
- An almost optimal algorithm for unbounded searching
- On approximation algorithms for the minimum satisfiability problem
- On computing minimal models
- Learning to ask relevant questions
- Optimizing with minimum satisfiability
- Approximating MIN 2-SAT and MIN 3-SAT
- Autarky pruning in propositional model elimination reduces failure redundancy
- Investigations on autark assignments
- The complexity of selecting maximal solutions
- Complexity analysis of propositional resolution with autarky pruning
- Iterative and core-guided maxsat solving: a survey and assessment
- Propositional circumscription and extended closed-world reasoning are \(\Pi_ 2^ P\)-complete
- Redundancy in logic. II: 2CNF and Horn propositional formulae
- Redundancy in logic. III: Non-monotonic reasoning
- Redundancy in logic. I: CNF propositional formulae
- Algorithms for computing minimal unsatisfiable subsets of constraints
- MCS Extraction with Sublinear Oracle Queries
- On Efficient Computation of Variable MUSes
- Advanced SAT Techniques for Abstract Argumentation
- Maximal Falsifiability
- Constraint Satisfaction Problems in Clausal Form I: Autarkies and Deficiency
- Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form
- On Computing Backbones of Propositional Theories
- Identifying Necessary Reactions in Metabolic Pathways by Minimal Model Generation
- Minimally Unsatisfiable Boolean Circuits
- On Improving MUS Extraction Algorithms
- Towards efficient MUS extraction
- On Reducing Maximum Independent Set to Minimum Satisfiability
- A Way to Simplify Truth Functions
- Computing Maximal Autarkies with Few and Simple Oracle Queries
- SAT-Based Formula Simplification
- A New Approach to Partial MUS Enumeration
- On Anti-subsumptive Knowledge Enforcement
- Searching for Autarkies to Trim Unsatisfiable Clause Sets
- Locating Minimal Infeasible Constraint Sets in Linear Programs
- The Minimum Satisfiability Problem
- The complexity of logic-based abduction
- Consistent subsets of inconsistent systems: structure and behaviour
- Algorithms for computing backbones of propositional formulae
- MaxSAT-based encodings for Group MaxSAT
- A tableau calculus for minimal model reasoning
- Enumerating Infeasibility: Finding Multiple MUSes Quickly
- Identifying the Class of Maxi-Consistent Operators in Argumentation
- Tools and Algorithms for the Construction and Analysis of Systems
- Theory and Applications of Satisfiability Testing
- A Dynamic Programming Approach to Sequential Pattern Recognition
- Verification, Model Checking, and Abstract Interpretation
- Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel
