Compiling finite linear CSP into SAT
From MaRDI portal
Publication:842794
DOI10.1007/s10601-008-9061-0zbMath1186.68076OpenAlexW2605289564MaRDI QIDQ842794
Mutsunori Banbara, Akiko Taga, Satoshi Kitagawa, Naoyuki Tamura
Publication date: 25 September 2009
Published in: Constraints (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10601-008-9061-0
Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Optimal and efficient designs for fMRI experiments via two-level circulant almost orthogonal arrays ⋮ Shift Design with Answer Set Programming ⋮ aspartame: Solving Constraint Satisfaction Problems with Answer Set Programming ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ \textsc{Conjure}: automatic generation of constraint models from problem specifications ⋮ Extending SMT solvers with support for finite domain \texttt{alldifferent} constraint ⋮ Coupling different integer encodings for SAT ⋮ SAT Modulo Graphs: Acyclicity ⋮ Automatically improving constraint models in Savile Row ⋮ A SAT Approach to Clique-Width ⋮ MaxSAT resolution for regular propositional logic ⋮ Time-expanded graph-based propositional encodings for makespan-optimal solving of cooperative path finding problems ⋮ aspeed: Solver scheduling via answer set programming ⋮ Clingcon: The next generation ⋮ Learning to select SAT encodings for pseudo-Boolean and linear Integer constraints ⋮ Constraint programming for planning test campaigns of communications satellites ⋮ Constraint CNF: SAT and CSP Language Under One Roof. ⋮ Automatic generation of basis test paths using variable length genetic algorithm ⋮ Solving constraint satisfaction problems with SAT modulo theories ⋮ Four decades of research on the open-shop scheduling problem to minimize the makespan ⋮ Compiling finite domain constraints to SAT withBEE ⋮ Why CP Portfolio Solvers Are (under)Utilized? Issues and Challenges ⋮ An automated approach to the Collatz conjecture ⋮ Dynamic programming approach for solving the open shop problem ⋮ Space-Efficient Planar Acyclicity Constraints ⋮ meSAT: multiple encodings of CSP to SAT ⋮ The possibilistic Horn non-clausal knowledge bases
Uses Software
Cites Work
- A competitive and cooperative approach to propositional satisfiability
- A branch \(\&\) bound algorithm for the open-shop problem
- Local search with constraint propagation and conflict-based heuristics
- Beam-ACO--hybridizing ant colony optimization with beam search: an application to open shop scheduling
- A new lower bound for the open-shop problem
- Benchmarks for basic scheduling problems
- Compiling Finite Linear CSP into SAT
- Theory and Applications of Satisfiability Testing
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Compiling finite linear CSP into SAT
