Algorithms for computing minimal equivalent subformulas
From MaRDI portal
Publication:460638
DOI10.1016/j.artint.2014.07.011zbMath1405.68340OpenAlexW2091072454MaRDI QIDQ460638
Anton Belov, Mikoláš Janota, Inês Lynce, João P. 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
Logic in artificial intelligence (68T27) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
Quantified maximum satisfiability ⋮ SAT-Based Horn Least Upper Bounds ⋮ Minimal sets on propositional formulae. Problems and reductions ⋮ On redundant topological constraints
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On the power of clause-learning SAT solvers as resolution engines
- The complexity of Boolean formula minimization
- Principles and practice of constraint programming. 18th international conference, CP 2012, Québec City, QC, Canada, October 8--12, 2012. Proceedings
- Logical and algorithmic properties of stable conditional independence
- Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems
- A structure-preserving clause form translation
- Optimal compression of propositional Horn knowledge bases: Complexity and approximation
- 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
- The scaling window of the 2-SAT transition
- Constraint Satisfaction Problems in Clausal Form I: Autarkies and Deficiency
- Inprocessing Rules
- On Improving MUS Extraction Algorithms
- Failed Literal Detection for QBF
- Towards efficient MUS extraction
- A Way to Simplify Truth Functions
- Finding Guaranteed MUSes Fast
- MUST: Provide a Finer-Grained Explanation of Unsatisfiability
- Eliminating Redundant Clauses in SAT Instances
- Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
- Efficient Combination of Decision Procedures for MUS Computation
- Minimal Representation of Directed Hypergraphs
- Locating Minimal Infeasible Constraint Sets in Linear Programs
- Two-level logic minimization: an overview
- Blocked Clause Elimination for QBF
- Removing propagation redundant constraints in redundant modeling
- Theory and Applications of Satisfiability Testing
- Determining computational complexity from characteristic ‘phase transitions’
- A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
- The Problem of Simplifying Truth Functions
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
