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

DOI10.1007/S10601-012-9131-1zbMATH Open1309.90083OpenAlexW1981106240WikidataQ57979694 ScholiaQ57979694MaRDI QIDQ487655FDOQ487655

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

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

zbMATH Keywords

SMTreformulationmeta-constraintsmodelling languagesweighted CSPweighted maxsat

Mathematics Subject Classification ID

Combinatorial optimization (90C27)

Cites Work

• Theory and Applications of Satisfiability Testing
• Parallel and distributed local search in COMET
• Title not available (Why is that?)
• Theory and Applications of Satisfiability Testing
• Solving constraint satisfaction problems with SAT modulo theories
• Essence: A constraint language for specifying combinatorial problems
• Lazy satisfiability modulo theories
• Solving (Weighted) Partial MaxSAT through Satisfiability Testing
• Algorithms for Weighted Boolean Optimization
• The state of the art of nurse rostering
• 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
• Maintaining reversible DAC for Max-CSP
• Partition-based lower bound for Max-CSP
• Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories
• On SAT Modulo Theories and Optimization Problems

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

Uses Software

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

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)