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

DOI10.1007/S10601-012-9131-1MaRDI QIDQ487655zbMATH OpenOpenAlexWikidataFDO

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

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

meta-constraintsmodelling languagesreformulationSMTweighted CSPweighted maxsat

Mathematics Subject Classification ID

Combinatorial optimization (90C27)

Recommendations

• Solving Max-SAT as weighted CSP
• Solving weighted CSP by maintaining arc consistency
• Solving weighted constraint satisfaction problems with memetic/exact hybrid algorithms
• On SAT Modulo Theories and Optimization Problems
• Bounds arc consistency for weighted CSPs

Cites work

• Algorithms for Weighted Boolean Optimization
• Essence: A constraint language for specifying combinatorial problems
• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• Lazy satisfiability modulo theories
• Maintaining reversible DAC for Max-CSP
• On SAT Modulo Theories and Optimization Problems
• Parallel and distributed local search in COMET
• Partition-based lower bound for Max-CSP
• Solving (Weighted) Partial MaxSAT through Satisfiability Testing
• Solving constraint satisfaction problems with SAT modulo theories
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Solving weighted CSP by maintaining arc consistency
• Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories
• The state of the art of nurse rostering
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(6)

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

Describes a project that uses

Uses Software

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

This page was built for publication: Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories

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