Compiling problem specifications into SAT

DOI10.1016/J.ARTINT.2004.01.006MaRDI QIDQ2457689zbMATH OpenOpenAlexFDO

Authors Marco Cadoli, Andrea Schaerf

Publication date 23 October 2007

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.artint.2004.01.006

zbMATH Keywords

NP-complete problemsSAT problemexecutable specificationsautomatic generation of problem reformulation

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Theory of compilers and interpreters (68N20) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Recommendations

• scientific article; zbMATH DE number 1692953
• NP-SPEC: An executable specification language for solving all problems in NP
• Writing declarative specifications for clauses
• Regular-SAT: A many-valued approach to solving combinatorial problems
• Compiling Finite Linear CSP into SAT

Cites work

• scientific article; zbMATH DE number 3474957 (Why is no real title available?)
• scientific article; zbMATH DE number 3635458 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1249657 (Why is no real title available?)
• scientific article; zbMATH DE number 2084742 (Why is no real title available?)
• scientific article; zbMATH DE number 956839 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Circumscribing DATALOG: expressive power and complexity
• Generating hard satisfiability problems
• Logic programs with stable model semantics as a constraint programming paradigm
• Logical cryptanalysis as a SAT problem: Encoding and analysis of the U. S. Data Encryption Standard
• NP-SPEC: An executable specification language for solving all problems in NP
• Optimization by Simulated Annealing: An Experimental Evaluation; Part II, Graph Coloring and Number Partitioning
• Permutation Problems and Channelling Constraints
• Scheduling sport tournaments using constraint logic programming
• The Semantics of Predicate Logic as a Programming Language

Cited in

(13)

• Generating Diverse Solutions in SAT
• meSAT: multiple encodings of CSP to SAT
• NP-SPEC: An executable specification language for solving all problems in NP
• scientific article; zbMATH DE number 2165692 (Why is no real title available?)
• Curriculum-based course timetabling with SAT and MaxSAT
• Automated reformulation of specifications by safe delay of constraints
• Evaluating ASP and commercial solvers on the CSPLib
• Writing declarative specifications for clauses
• Exploiting functional dependencies in declarative problem specifications
• scientific article; zbMATH DE number 1692953 (Why is no real title available?)
• URSA: a system for uniform reduction to SAT
• \(\mathcal {NPD}\)atalog: A logic language for expressing \(\mathcal {NP}\) search and optimization problems
• Compiling finite domain constraints to SAT with BEE

Describes a project that uses

Uses Software

• DIMACS
• NP-SPEC

This page was built for publication: Compiling problem specifications into SAT

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