Compiling problem specifications into SAT

DOI10.1016/j.artint.2004.01.006zbMath1132.68693OpenAlexW2143775744MaRDI QIDQ2457689

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

Theory of compilers and interpreters (68N20) 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) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Related Items

Curriculum-based course timetabling with SAT and MaxSAT ⋮ Automated reformulation of specifications by safe delay of constraints ⋮ atalog: A logic language for expressing search and optimization problems ⋮ Compiling finite domain constraints to SAT withBEE ⋮ Evaluating ASP and commercial solvers on the CSPLib ⋮ Exploiting functional dependencies in declarative problem specifications ⋮ Writing Declarative Specifications for Clauses ⋮ meSAT: multiple encodings of CSP to SAT

Uses Software

• NP-SPEC
• DIMACS

Cites Work

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