Effective preprocessing in SAT through variable and clause elimination
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- Efficiently checking propositional refutations in HOL theorem provers
- Lower bound on average-case complexity of inversion of Goldreich's function by drunken backtracking algorithms
- Automatically improving constraint models in Savile Row
- What is answer set programming to propositional satisfiability
- Auto-tabling for subproblem presolving in MiniZinc
- Conflict-driven answer set solving: from theory to practice
- The complexity of inverting explicit Goldreich's function by DPLL algorithms
- Exploiting partial variable assignment in interpolation-based model checking
- Flexible proof production in an industrial-strength SMT solver
- Preprocessing of propagation redundant clauses
- Hash-based preprocessing and inprocessing techniques in SAT solvers
- On the hierarchical community structure of practical Boolean formulas
- XOR local search for Boolean Brent equations
- Leveraging GPUs for effective clause sharing in parallel SAT solving
- Incremental column-wise verification of arithmetic circuits using computer algebra
- Clause vivification by unit propagation in CDCL SAT solvers
- How we designed winning algorithms for abstract argumentation and which insight we attained
- Definability for model counting
- Computing properties of stable configurations of thermodynamic binding networks
- Compiling CP subproblems to MDDs and d-DNNFs
- On the hardness of solving edge matching puzzles as SAT or CSP problems
- On preprocessing techniques and their impact on propositional model counting
- Visualizing SAT instances and runs of the DPLL algorithm
- Broken triangles: from value merging to a tractable class of general-arity constraint satisfaction problems
- Set constraint model and automated encoding into SAT: application to the social golfer problem
- What we can learn from conflicts in propositional satisfiability
- SATenstein: automatically building local search SAT solvers from components
- Craig interpolation with clausal first-order tableaux
- Extended formulation and valid inequalities for the multi-item inventory lot-sizing problem with supplier selection
- Tighter bounds on directed Ramsey number \(R(7)\)
- On the hardness of SAT with community structure
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Synthesis of domain specific CNF encoders for bit-vector solvers
- Finding Finite Models in Multi-sorted First-Order Logic
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- LMHS: a SAT-IP hybrid MaxSat solver
- On the one-way function candidate proposed by Goldreich
- DRAT proofs for XOR reasoning
- Preprocessing in incremental SAT
- SAT-based preprocessing for MaxSAT
- Algorithms for Solving Satisfiability Problems with Qualitative Preferences
- Inprocessing rules
- An expressive model for instance decomposition based parallel SAT solvers
- On freezing and reactivating learnt clauses
- Efficient CNF simplification based on binary implication graphs
- SAT-Based Model Checking without Unrolling
- Propositional SAT solving
- Truth assignments as conditional autarkies
- Decomposing SAT Instances with Pseudo Backbones
- Advances in WASP
- PBLib -- a library for encoding pseudo-Boolean constraints into CNF
- Preprocessing for DQBF
- Recognition of Nested Gates in CNF Formulas
- Evaluating CDCL variable scoring schemes
- A Generalized Framework for Conflict Analysis
- Adaptive Restart Strategies for Conflict Driven SAT Solvers
- Finding Guaranteed MUSes Fast
- Hierarchical Hardness Models for SAT
- Simulating circuit-level simplifications on CNF
- LCF-Style Propositional Simplification with BDDs and SAT Solvers
- Eliminating Redundant Clauses in SAT Instances
- Applying Logic Synthesis for Speeding Up SAT
- Automatic Termination
- Finding Lean Induced Cycles in Binary Hypercubes
- Symmetry in Gardens of Eden
- Elimination of Infrequent Variables Improves Average Case Performance of Satisfiability Algorithms
- Learning from conflicts in propositional satisfiability
- A pearl on SAT and SMT solving in Prolog
- SAT-solving in CSP trace refinement
- Symbolic algorithmic verification of intransitive generalized noninterference
- Incremental preprocessing methods for use in BMC
- Local redundancy in SAT: generalizations of blocked clauses
- scientific article; zbMATH DE number 6970794 (Why is no real title available?)
- Subsumed label elimination for maximum satisfiability
- Computational approaches to finding and measuring inconsistency in arbitrary knowledge bases
- Constraint answer set solver EZCSP and why integration schemas matter
- Guarantees and limits of preprocessing in constraint satisfaction and reasoning
- On the completeness of pruning techniques for planning with conditional effects
- An overview of parallel SAT solving
- Local search for Boolean satisfiability with configuration checking and subscore
- Algorithm runtime prediction: methods \& evaluation
- Inst-Gen -- a modular approach to instantiation-based automated reasoning
- Reconstructing solutions after blocked clause elimination
- The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
- On quantifying literals in Boolean logic and its applications to explainable AI
- Simplifying clausal satisfiability problems
- Inconsistency proofs for ASP: the ASP-DRUPE format
- Cost-optimal constrained correlation clustering via weighted partial maximum satisfiability
- Automatic construction of parallel portfolios via algorithm configuration
- Resizing cardinality constraints for MaxSAT
- Blocked clause elimination for QBF
- Experimental study of the shortest reset word of random automata
- Constraint CNF: SAT and CSP Language Under One Roof.
- Practical algorithms for finding extremal sets
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Cardinality networks: a theoretical and empirical study
- Cost-effective hyper-resolution for preprocessing CNF formulas
- NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances
- A Gröbner Basis Approach to CNF-Formulae Preprocessing
This page was built for publication: Effective preprocessing in SAT through variable and clause elimination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5713748)
