Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories

DOI10.1007/s10601-012-9131-1zbMath1309.90083OpenAlexW1981106240WikidataQ57979694 ScholiaQ57979694MaRDI QIDQ487655

Josep Suy, Miquel Bofill, Mateu Villaret, Carlos Ansótegui, Miquel Palahí

Publication date: 22 January 2015

Published in: Constraints (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10601-012-9131-1

zbMATH Keywords

modelling languagesSMTreformulationmeta-constraintsweighted CSPweighted maxsat

Mathematics Subject Classification ID

Combinatorial optimization (90C27)

Related Items

A constraint programming-based iterated greedy algorithm for the open shop with sequence-dependent processing times and makespan minimization ⋮ Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories ⋮ Exploiting subproblem optimization in SAT-based maxsat algorithms ⋮ \textsc{OptiMathSAT}: a tool for optimization modulo theories ⋮ MiniBrass: soft constraints for MiniZinc

Uses Software

• MiniSat
• Zchaff2004
• COMET
• SMT-LIB
• Yices
• MiniZinc
• PicoSAT
• SIMPLY
• NSPLib
• Essence

Cites Work

• Unnamed Item
• Unnamed Item
• Solving constraint satisfaction problems with SAT modulo theories
• Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories
• Solving weighted CSP by maintaining arc consistency
• Essence: A constraint language for specifying combinatorial problems
• Parallel and distributed local search in COMET
• Maintaining reversible DAC for Max-CSP
• Partition-based lower bound for Max-CSP
• The state of the art of nurse rostering
• Solving SAT and SAT Modulo Theories
• Solving (Weighted) Partial MaxSAT through Satisfiability Testing
• Algorithms for Weighted Boolean Optimization
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• On SAT Modulo Theories and Optimization Problems