Simulating circuit-level simplifications on CNF
From MaRDI portal
Publication:352967
DOI10.1007/s10817-011-9239-9zbMath1267.94144OpenAlexW2038777323MaRDI QIDQ352967
Matti Järvisalo, Armin Biere, Marijn J. H. Heule
Publication date: 5 July 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-011-9239-9
Boolean satisfiabilityvariable eliminationBoolean circuitspreprocessingblocked clausesproblem structure
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (14)
On preprocessing techniques and their impact on propositional model counting ⋮ Recognition of Nested Gates in CNF Formulas ⋮ Propositional SAT Solving ⋮ SAT-Based Model Checking ⋮ Incremental column-wise verification of arithmetic circuits using computer algebra ⋮ Truth Assignments as Conditional Autarkies ⋮ Finding Effective SAT Partitionings Via Black-Box Optimization ⋮ SAT solver management strategies in IC3: an experimental approach ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Strong extension-free proof systems ⋮ Definability for model counting ⋮ Super-Blocked Clauses ⋮ Clause redundancy and preprocessing in maximum satisfiability
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Extended clause learning
- A structure-preserving clause form translation
- An optimality result for clause form translation
- Toward leaner binary-clause reasoning in a satisfiability solver
- New methods for 3-SAT decision and worst-case analysis
- On a generalization of extended resolution
- Solving Satisfiability with Less Searching
- Blocked Clause Elimination
- Exact DFA Identification Using SAT Solvers
- Combining Adaptive Noise and Look-Ahead in Local Search for SAT
- Applying Logic Synthesis for Speeding Up SAT
- Towards feasible solutions of the tautology problem
- Reconstructing Solutions after Blocked Clause Elimination
- Blocked Clause Elimination for QBF
- Theory and Applications of Satisfiability Testing
- A Decision Procedure for Bit-Vectors and Arrays
- A Computing Procedure for Quantification Theory
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
This page was built for publication: Simulating circuit-level simplifications on CNF
