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

SMTreformulationmeta-constraintsmodelling languagesweighted 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

• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• Algorithms for Weighted Boolean Optimization
• Essence: A constraint language for specifying combinatorial problems
• 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 SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Solving constraint satisfaction problems with SAT modulo theories
• 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)

• On the Implementation of Weight Constraint Rules in Conflict-Driven ASP Solvers
• \textsc{OptiMathSAT}: a tool for optimization modulo theories
• MiniBrass: soft constraints for MiniZinc
• 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

Describes a project that uses

Uses Software

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

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)