Algorithms for computing minimal equivalent subformulas
DOI10.1016/J.ARTINT.2014.07.011zbMATH Open1405.68340OpenAlexW2091072454MaRDI QIDQ460638FDOQ460638
Authors: Anton Belov, Mikoláš Janota, Inês Lynce, Joao Marques-Silva 
Publication date: 13 October 2014
Published in: Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.artint.2014.07.011
Recommendations
- Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems
- Computing minimally unsatisfiable subformulas: state of the art and future directions
- Minimally unsatisfiable Boolean circuits
- scientific article; zbMATH DE number 2080337
- Algorithms for computing backbones of propositional formulae
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Logic in artificial intelligence (68T27)
Cites Work
- Theory and Applications of Satisfiability Testing
- Title not available (Why is that?)
- Blocked clause elimination for QBF
- A structure-preserving clause form translation
- Algorithms for computing minimal unsatisfiable subsets of constraints
- Failed literal detection for QBF
- Title not available (Why is that?)
- Redundancy in logic. I: CNF propositional formulae
- A Way to Simplify Truth Functions
- Locating Minimal Infeasible Constraint Sets in Linear Programs
- Removing propagation redundant constraints in redundant modeling
- The Problem of Simplifying Truth Functions
- Towards efficient MUS extraction
- Efficient combination of decision procedures for MUS computation
- Logical and algorithmic properties of stable conditional independence
- Title not available (Why is that?)
- Inprocessing rules
- Minimal Representation of Directed Hypergraphs
- Principles and practice of constraint programming. 18th international conference, CP 2012, Québec City, QC, Canada, October 8--12, 2012. Proceedings
- Optimal compression of propositional Horn knowledge bases: Complexity and approximation
- The complexity of Boolean formula minimization
- Temporal induction by incremental SAT solving
- On the power of clause-learning SAT solvers as resolution engines
- MUST: Provide a Finer-Grained Explanation of Unsatisfiability
- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
- A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
- 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
- The scaling window of the 2-SAT transition
- On improving MUS extraction algorithms
- Finding Guaranteed MUSes Fast
- Eliminating Redundant Clauses in SAT Instances
- Two-level logic minimization: an overview
- Determining computational complexity from characteristic ``phase transitions
- Title not available (Why is that?)
Cited In (4)
Uses Software
This page was built for publication: Algorithms for computing minimal equivalent subformulas
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q460638)
