Conflict Resolution

DOI10.1007/978-3-642-04244-7_41MaRDI QIDQ3182526zbMATH OpenOpenAlexFDO

Authors Konstantin Korovin, Nestan Tsiskaridze, Andrei Voronkov

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

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

Recommendations

• Solving systems of linear inequalities by bound propagation
• Generalized resolution for 0--1 linear inequalities
• A simultaneous projections method for linear inequalities
• Locally polynomial method for solving systems of linear inequalities
• A strongly polynomial algorithm for a new class of linear inequalities¹

Cites work

• scientific article; zbMATH DE number 1234104 (Why is no real title available?)
• Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
• Projecting CLP(\({\mathcal R}\)) constraints
• Variable Elimination in Linear Constraints

Cited in

(20)

• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
• Better answers to real questions
• FMplex: exploring a bridge between Fourier-Motzkin and simplex
• Semantically-guided goal-sensitive reasoning: model representation
• VIRAS: conflict-driven quantifier elimination for integer-real arithmetic
• How to resolve doxastic disagreement
• The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints
• scientific article; zbMATH DE number 465390 (Why is no real title available?)
• Conflict analysis
• Solving systems of linear inequalities by bound propagation
• Cutting to the chase. Solving linear integer arithmetic
• Satisfiability modulo theories
• The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
• Implementing conflict resolution
• Cutting to the chase.
• Conflict model with negotiation
• Machine Learning: ECML 2004
• Linear quantifier elimination as an abstract decision procedure
• ALASCA: reasoning in quantified linear arithmetic
• FMplex: a novel method for solving linear real arithmetic problems

Describes a project that uses

Uses Software

• cvc3
• SMT-LIB
• BarcelogicTools

This page was built for publication: Conflict Resolution

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