Recognition of Nested Gates in CNF Formulas

DOI10.1007/978-3-319-24318-4_19zbMath1471.68246OpenAlexW2125663207MaRDI QIDQ3453230

Carsten Sinz, Markus Iser, Norbert Manthey

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-24318-4_19

Mathematics Subject Classification ID

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

Related Items (4)

SAT race 2015 ⋮ Unnamed Item ⋮ Super-Blocked Clauses ⋮ cnf2aig

Uses Software

• MiniSat
• Oz
• Kodkod
• LLBMC
• Coprocessor
• Lingeling

Cites Work

• Unnamed Item
• Simulating circuit-level simplifications on CNF
• A structure-preserving clause form translation
• An optimality result for clause form translation
• Visualizing SAT instances and runs of the DPLL algorithm
• Blocked Clause Decomposition
• Detecting Cardinality Constraints in CNF
• Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask)
• Counterexample-guided abstraction refinement for symbolic model checking
• Blocked Clause Elimination
• Theory and Applications of Satisfiability Testing
• A Constraint Satisfaction Approach for Programmable Logic Detailed Placement
• Minimizing Models for Tseitin-Encoded SAT Instances
• A Computing Procedure for Quantification Theory
• Theory and Applications of Satisfiability Testing
• Kodkod: A Relational Model Finder

This page was built for publication: Recognition of Nested Gates in CNF Formulas