Formalizing Dangerous SAT Encodings

DOI10.1007/978-3-540-72788-0_18zbMATH Open1214.68177OpenAlexW1570066695MaRDI QIDQ3612464FDOQ3612464

Authors: Alexander Wolfgang Karl Kurt Hertel, Philipp Hertel, Alasdair Urquhart 

Publication date: 10 March 2009

Published in: Theory and Applications of Satisfiability Testing – SAT 2007 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-72788-0_18

Recommendations

• Automatic generation of propagation complete SAT encodings
• Towards Robust CNF Encodings of Cardinality Constraints
• Logical cryptanalysis as a SAT problem
• Logical cryptanalysis as a SAT problem: Encoding and analysis of the U. S. Data Encryption Standard
• Circuit Based Encoding of CNF Formula

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25) Graph theory (including graph drawing) in computer science (68R10) Complexity of proofs (03F20)

Cited In (9)

• Regular resolution effectively simulates resolution
• Chinese remainder encoding for Hamiltonian cycles
• Curriculum-based course timetabling with SAT and MaxSAT
• Principles and Practice of Constraint Programming – CP 2004
• Automatic generation of propagation complete SAT encodings
• Title not available (Why is that?)
• A Logical Autobiography
• New Encodings of Pseudo-Boolean Constraints into CNF
• SAT-Based Synthesis Methods for Safety Specs

This page was built for publication: Formalizing Dangerous SAT Encodings

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