Some progress in satisfiability checking for difference logic

DOI10.1007/978-3-540-30206-3_19MaRDI QIDQ5464752zbMATH OpenOpenAlexFDO

Authors Scott Cotton, Eugene Asarin, Oded Maler, Peter Niebert

Publication date 19 August 2005

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

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• DPLL(T) with exhaustive theory propagation and its application to difference logic
• A SAT-based decision procedure for the Boolean combination of difference constraints
• Theory and Applications of Satisfiability Testing
• Verification of timed automata via satisfiability checking
• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures

Cited in

(19)

• Empirical analysis of algorithms for the shortest negative cost cycle problem
• Randomized algorithms for finding the shortest negative cost cycle in networks
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• On the parametrized complexity of read-once refutations in UTVPI+ constraint systems
• Analyzing unit read-once refutations in difference constraint systems
• Efficient theory combination via Boolean search
• Speeding up the constraint-based method in difference logic
• Logical Difference Computation with CEX2.5
• Model Checking Real-Time Systems
• Solving difference constraints over modular arithmetic
• Disequality management in integer difference logic via finite instantiations.
• SDSAT: Tight integration of small domain encoding and lazy approaches in solving difference logic.
• A SAT-based decision procedure for the Boolean combination of difference constraints
• Unit read-once refutations for systems of difference constraints
• Finding short tree-like unit refutations in UTVPI constraint systems
• Optimal length resolution refutations of difference constraint systems
• The SAT-based approach to separation logic
• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
• An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty

Describes a project that uses

Uses Software

• Chaff
• BerkMin

This page was built for publication: Some progress in satisfiability checking for difference logic

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