Boolean satisfiability with transitivity constraints

DOI10.1007/10722167_10MaRDI QIDQ2754075zbMATH OpenFDO

Authors Randal E. Bryant, Miroslav N. Velev

Publication date 11 November 2001

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

Full work available at URL https://doi.org/10.1007/10722167_10

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Boolean satisfiability with transitivity constraints
• A satisfiability procedure for quantified Boolean formulae
• Ordered binary decision diagrams and the Davis-Putnam procedure
• Generating minimum transitivity constraints in P-time for deciding equality logic
• Satisfiability checking using Boolean expression diagrams

Cited in

(10)

• A framework for satisfiability modulo theories
• Building small equality graphs for deciding equality logic with uninterpreted functions
• p-constraint and the transitivity theorem
• Generating minimum transitivity constraints in P-time for deciding equality logic
• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• scientific article; zbMATH DE number 5139168 (Why is no real title available?)
• scientific article; zbMATH DE number 5547835 (Why is no real title available?)
• Complete Problems Involving Boolean Labelled Structures and Projection Transactions
• Transforming equality logic to propositional logic
• Boolean satisfiability with transitivity constraints

Describes a project that uses

Uses Software

• Velev SAT Benchmarks

This page was built for publication: Boolean satisfiability with transitivity constraints

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