Algorithms for computing minimal equivalent subformulas

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
Constraint satisfaction problems in clausal form. II: Minimal unsatisfiability and conflict structure
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)

Quantified maximum satisfiability
Minimal sets on propositional formulae. Problems and reductions
On redundant topological constraints
SAT-Based Horn Least Upper Bounds

Uses Software

MiniSat
PicoSAT
Bloqqer
QUICKXPLAIN

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)