Simulating circuit-level simplifications on CNF

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

zbMATH Keywords

Boolean satisfiabilityvariable eliminationBoolean circuitspreprocessingblocked clausesproblem structure

Mathematics Subject Classification ID

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

• Beaver
• Boolector
• MiniSat
• UBCSAT
• z3
• NiVER
• OpenSMT
• MathSAT
• STP

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