Formalizing Dangerous SAT Encodings

DOI10.1007/978-3-540-72788-0_18MaRDI QIDQ3612464zbMATH OpenOpenAlexFDO

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

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)

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

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
• scientific article; zbMATH DE number 2016108 (Why is no real title available?)
• 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)