Some computational aspects of DISTANCE SAT

DOI10.1007/S10817-006-9063-9MaRDI QIDQ877840zbMATH OpenOpenAlexFDO

Authors Olivier Bailleux, Pierre Marquis

Publication date 3 May 2007

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-006-9063-9

zbMATH Keywords

propositional 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) Classical propositional logic (03B05)

Recommendations

• Minimal distance of propositional models
• An Isomorphism-Invariant Distance Function on Propositional Formulas in CNF
• Recent Advances in Constraints
• optsat: A Tool for Solving SAT Related Optimization Problems
• As Close as It Gets

Cites work

• scientific article; zbMATH DE number 67483 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 2038892 (Why is no real title available?)
• scientific article; zbMATH DE number 1849163 (Why is no real title available?)
• scientific article; zbMATH DE number 1414299 (Why is no real title available?)
• scientific article; zbMATH DE number 4185089 (Why is no real title available?)
• A linear-time transformation of linear inequalities into conjunctive normal form
• A logical approach to interpolation based on similarity relations
• A machine program for theorem-proving
• A theory of diagnosis from first principles
• BerkMin: A fast and robust SAT-solver
• Consequence finding algorithms
• Decomposable negation normal form
• Efficient CNF encoding of Boolean cardinality constraints
• Many hard examples for resolution
• Reducing belief revision to circumscription (and vice versa)
• Theory and Applications of Satisfiability Testing
• Towards an Optimal CNF Encoding of Boolean Cardinality Constraints

Cited in

(8)

• Recent Advances in Constraints
• Reducing chaos in SAT-like search: finding solutions close to a given one
• An abstract view on optimizations in propositional frameworks
• Minimal distance of propositional models
• Simplified forms of computerized reasoning with distance semantics
• The next whisky bar
• Boosting distance-based revision using SAT encodings
• Implementing semantic merging operators using binary decision diagrams

Describes a project that uses

Uses Software

• BerkMin
• Jerusat

This page was built for publication: Some computational aspects of DISTANCE SAT

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