NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances
From MaRDI portal
Recommendations
- Effective preprocessing in SAT through variable and clause elimination
- Elimination of Infrequent Variables Improves Average Case Performance of Satisfiability Algorithms
- Eliminating Redundant Clauses in SAT Instances
- Theory and Applications of Satisfiability Testing
- A Preprocessor for Max-SAT Solvers
Cited in
(22)- Automatically improving constraint models in Savile Row
- NiVER
- Definability for model counting
- On preprocessing techniques and their impact on propositional model counting
- What we can learn from conflicts in propositional satisfiability
- SATenstein: automatically building local search SAT solvers from components
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- SAT modulo graphs: acyclicity
- An expressive model for instance decomposition based parallel SAT solvers
- PBLib -- a library for encoding pseudo-Boolean constraints into CNF
- Simulating circuit-level simplifications on CNF
- Learning from conflicts in propositional satisfiability
- Incremental preprocessing methods for use in BMC
- On quantifying literals in Boolean logic and its applications to explainable AI
- Effective preprocessing in SAT through variable and clause elimination
- SAT-Inspired Eliminations for Superposition
- Mining definitions in Kissat with Kittens
- SAT-Inspired Higher-Order Eliminations
- The ghosts of forgotten things: a study on size after forgetting
- Common equivalence and size of forgetting from Horn formulae
- Enhancing query efficiency for D-DNNF representations through preprocessing
- Certified MaxSAT preprocessing
This page was built for publication: NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5714759)
