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

automatic generation of problem reformulationexecutable specificationsNP-complete problemsSAT problem

Mathematics Subject Classification ID

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

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

• 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
• 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?)
• 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)

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