M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures

DOI10.1007/s10817-005-9004-zzbMath1109.68101OpenAlexW2158995961WikidataQ62041379 ScholiaQ62041379MaRDI QIDQ862395

Roberto Bruttomesso, Stephan Schulz, Tommi Junttila, Peter van Rossum, Roberto Sebastiani, Marco Bozzano, Alessandro Cimatti

Publication date: 24 January 2007

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

Full work available at URL: https://doi.org/10.1007/s10817-005-9004-z

zbMATH Keywords

propositional satisfiability techniques

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

Processes and continuous change in a SAT-based planner, Formal reliability analysis of redundancy architectures, The Strategy Challenge in SMT Solving, Efficient Interpolant Generation in Satisfiability Modulo Theories, Colors Make Theories Hard, MathSAT, Stable models and difference logic, Theory decision by decomposition, Rewrite-Based Decision Procedures

Uses Software

• MiniSat
• QOCA
• Chaff
• CVC Lite
• E Theorem Prover
• ICS
• Zapato
• Cassowary

Cites Work

• Negative-cycle detection algorithms
• Backtracking algorithms for disjunctions of temporal constraints
• An Automatic Method of Solving Discrete Programming Problems
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Computer Aided Verification
• Theory and Applications of Satisfiability Testing
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Theory and Applications of Satisfiability Testing
• Mechanizing Mathematical Reasoning
• Computer Aided Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item