Simulating circuit-level simplifications on CNF

DOI10.1007/S10817-011-9239-9zbMATH Open1267.94144OpenAlexW2038777323MaRDI QIDQ352967FDOQ352967

Authors: 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

Recommendations

• Blocked clause elimination
• Clause elimination procedures for CNF formulas
• Circuit Based Encoding of CNF Formula
• Efficient CNF simplification based on binary implication graphs
• Clause elimination for SAT and QSAT

zbMATH Keywords

Boolean circuitspreprocessingblocked clausesBoolean satisfiabilityproblem structurevariable elimination

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cites Work

• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Blocked clause elimination for QBF
• A Decision Procedure for Bit-Vectors and Arrays
• A structure-preserving clause form translation
• Title not available (Why is that?)
• Theory and Applications of Satisfiability Testing
• A Computing Procedure for Quantification Theory
• Theory and Applications of Satisfiability Testing
• Blocked clause elimination
• Exact DFA Identification Using SAT Solvers
• 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
• Balance and filtering in structured satisfiable problems. (Preliminary report)
• Exploiting the real power of unit propagation lookahead
• Solving Satisfiability with Less Searching
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Reconstructing solutions after blocked clause elimination
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Title not available (Why is that?)
• Extended clause learning

Cited In (24)

• Local redundancy in SAT: generalizations of blocked clauses
• Clause redundancy and preprocessing in maximum satisfiability
• Certified SAT solving with GPU accelerated inprocessing
• On preprocessing techniques and their impact on propositional model counting
• Theory and Applications of Satisfiability Testing
• Finding Effective SAT Partitionings Via Black-Box Optimization
• Propositional SAT solving
• Recognition of Nested Gates in CNF Formulas
• Applying Logic Synthesis for Speeding Up SAT
• Circuit Based Encoding of CNF Formula
• Efficient CNF simplification based on binary implication graphs
• Simplification in a satisfiability checker for VLSI applications
• Clause elimination procedures for CNF formulas
• Super-blocked clauses
• SAT-Based Model Checking
• Definability for model counting
• Truth assignments as conditional autarkies
• Strong extension-free proof systems
• Theory and Applications of Satisfiability Testing
• Title not available (Why is that?)
• Blocked clause elimination
• Simulation of hybrid circuits in constraint logic programming
• SAT solver management strategies in IC3: an experimental approach
• Incremental column-wise verification of arithmetic circuits using computer algebra

Uses Software

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

This page was built for publication: Simulating circuit-level simplifications on CNF

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q352967)