Conflict Resolution

DOI10.1007/978-3-642-04244-7_41zbMath1336.68236OpenAlexW4243587093MaRDI QIDQ3182526

Andrei Voronkov, Konstantin Korovin, Nestan Tsiskaridze

Publication date: 9 October 2009

Published in: Principles and Practice of Constraint Programming - CP 2009 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04244-7_41

Mathematics Subject Classification ID

Linear inequalities of matrices (15A39) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (10)

Semantically-guided goal-sensitive reasoning: model representation ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Satisfiability Modulo Theories ⋮ The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints ⋮ Better answers to real questions ⋮ Linear Quantifier Elimination as an Abstract Decision Procedure ⋮ Cutting to the Chase Solving Linear Integer Arithmetic ⋮ Solving Systems of Linear Inequalities by Bound Propagation ⋮ The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints ⋮ Cutting to the chase.

Uses Software

• BarcelogicTools
• SMT-LIB
• cvc3

Cites Work

• Unnamed Item
• Projecting CLP(\({\mathcal R}\)) constraints
• Variable Elimination in Linear Constraints
• Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools

This page was built for publication: Conflict Resolution