A scalable method for solving satisfiability of integer linear arithmetic logic

DOI10.1007/11499107_18MaRDI QIDQ5713714zbMATH OpenOpenAlexFDO

Authors Hossein M. Sheini, Karem A. Sakallah

Publication date 15 December 2005

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

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

Mathematics Subject Classification ID

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

Recommendations

• A SAT-Based Decision Procedure for Mixed Logical/Integer Linear Problems
• M\textbf{ath}SAT: Tight integration of SAT and mathematical decision procedures
• On solving Boolean combinations of UTVPI constraints.
• From Propositional Satisfiability to Satisfiability Modulo Theories
• An incremental and layered procedure for the satisfiability of linear arithmetic logic

Cited in

(11)

• Cutting the mix
• Satisfiability modulo theories
• On solving Presburger and linear arithmetic with SAT
• Improving IntSat by expressing disjunctions of bounds as linear constraints
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• A SAT-Based Decision Procedure for Mixed Logical/Integer Linear Problems
• scientific article; zbMATH DE number 5263038 (Why is no real title available?)
• An incremental and layered procedure for the satisfiability of linear arithmetic logic
• Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
• Equality detection for linear arithmetic constraints
• Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)

Describes a project that uses

Uses Software

• Chaff
• MiniSat

This page was built for publication: A scalable method for solving satisfiability of integer linear arithmetic logic

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