Fast and Flexible Difference Constraint Propagation for DPLL(T)
From MaRDI portal
Publication:5756581
DOI10.1007/11814948_19zbMath1187.68537OpenAlexW1488662850MaRDI QIDQ5756581
Publication date: 4 September 2007
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11814948_19
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (22)
Problem Decomposition and Multi-shot ASP Solving for Job-shop Scheduling ⋮ Stochastic Local Search for SMT: Combining Theory Solvers with WalkSAT ⋮ Empirical analysis of algorithms for the shortest negative cost cycle problem ⋮ Satisfiability Modulo Theories ⋮ Model Checking Real-Time Systems ⋮ Learning general constraints in CSP ⋮ A logic-based Benders decomposition for microscopic railway timetable planning ⋮ SAT Modulo Graphs: Acyclicity ⋮ Set covering heuristics in a benders decomposition for railway timetabling ⋮ Clingo goes linear constraints over reals and integers ⋮ Randomized algorithms for finding the shortest negative cost cycle in networks ⋮ Unit read-once refutations for systems of difference constraints ⋮ A mechanical verification of the stressing algorithm for negative cost cycle detection in networks ⋮ Interpolant Generation for UTVPI ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Efficient Interpolant Generation in Satisfiability Modulo Theories ⋮ On the parametrized complexity of Read-once refutations in UTVPI+ constraint systems ⋮ Analyzing unit read-once refutations in difference constraint systems ⋮ Stable models and difference logic ⋮ Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis ⋮ Solving strong controllability of temporal problems with uncertainty using SMT ⋮ Feasibility checking in Horn constraint systems through a reduction based approach
Uses Software
This page was built for publication: Fast and Flexible Difference Constraint Propagation for DPLL(T)