Constraint solving in Logic Programming and in Automated Deduction: A comparison

Constraint Logic Programming (CLP) began as a natural merger of two declarative paradigms: constraint solving and logic programming. This combination helps make CLP programs both expressive and flexible, and in some cases, more efficient than other kinds of programs. Though a relatively new field, CLP has progressed in several and quite different directions. In particular, the early fundamental concepts have been adapted to better serve in different areas of applications. In this survey of CLP, a primary goal is to give a systematic description of the major trends in terms of common fundamental concepts. Consider first an example program in order to identify some crucial CLP concepts. The program below defines the relation sumto(n, 1 + 2 + . . . . . + n) for natural numbers n. . . . sumto(0, 0). . . . . . sumto(N, S) :- N >= 1, N <= S, sumto(N - 1, S - N). . . . The query S <= 3, sumto(N, S) gives rise to three answers (N = 0, S = 0), (N = 1, S =1), and (N = 2, S = 3), and terminates.

Download Full-text

Constraint Solving Specializations for Equality on an Interval-Variable Domain

Journal of Advanced Computational Intelligence and Intelligent Informatics ◽

10.20965/jaciii.2007.p0210 ◽

2007 ◽

Vol 11 (2) ◽

pp. 210-219

Author(s):

Hiroshi Mabuchi ◽

◽

Kiyoshi Akama ◽

Katsunori Miura ◽

Takahiko Ishikawa ◽

...

Keyword(s):

Logic Programming ◽

Variable Domain ◽

Equality Constraint ◽

Constraint Solving ◽

Equivalent Transformation ◽

Interval Variable ◽

Interval Variables ◽

The Relationship

In the equivalent transformation (ET) model, where computation is regarded as ET using rules that constitute a program, this paper develops a theory for equality-constraint solving which unification does in the theory of logic programming. This paper clarifies the relationship between Constraint Solving Specializations for Equality (CSSEs) and unifiers. The concept of CSSE can be used to solve equality constraint in a clause, and promotes component-based programming. An algorithm for finding CSSEs in the domain including interval variables is constructed by combining simpler ET rules. Termination and correctness of the algorithm is proven.

Download Full-text

Sequences constraint solving in constraint logic programming

Proceedings Sixth International Conference on Tools with Artificial Intelligence. TAI 94 ◽

10.1109/tai.1994.346397 ◽

2002 ◽

Author(s):

P. Baptiste ◽

B. Legeard ◽

H. Zidoum

Keyword(s):

Logic Programming ◽

Constraint Logic Programming ◽

Constraint Solving

Download Full-text

SUNNY: a Lazy Portfolio Approach for Constraint Solving

Theory and Practice of Logic Programming ◽

10.1017/s1471068414000179 ◽

2014 ◽

Vol 14 (4-5) ◽

pp. 509-524 ◽

Cited By ~ 11

Author(s):

ROBERTO AMADINI ◽

MAURIZIO GABBRIELLI ◽

JACOPO MAURO

Keyword(s):

Logic Programming ◽

Constraint Satisfaction ◽

State Of The Art ◽

Constraint Satisfaction Problem ◽

Answer Set Programming ◽

Constraint Solving ◽

Explicit Model ◽

Actual Performance ◽

Portfolio Approach ◽

Empirical Tests

AbstractWithin the context of constraint solving, a portfolio approach allows one to exploit the synergy between different solvers in order to create a globally better solver. In this paper we present SUNNY: a simple and flexible algorithm that takes advantage of a portfolio of constraint solvers in order to compute — without learning an explicit model — a schedule of them for solving a given Constraint Satisfaction Problem (CSP). Motivated by the performance reached by SUNNY vs. different simulations of other state of the art approaches, we developedsunny-csp, an effective portfolio solver that exploits the underlying SUNNY algorithm in order to solve a given CSP. Empirical tests conducted on exhaustive benchmarks of MiniZinc models show that the actual performance ofsunny-cspconforms to the predictions. This is encouraging both for improving the power of CSP portfolio solvers and for trying to export them to fields such as Answer Set Programming and Constraint Logic Programming.

Download Full-text

The relation between logic programming and logic specification

Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences ◽

10.1098/rsta.1984.0064 ◽

1984 ◽

Vol 312 (1522) ◽

pp. 345-361 ◽

Cited By ~ 9

Keyword(s):

Logic Programming ◽

Programming Languages ◽

Programming Language ◽

Specification Language ◽

Formal Logic ◽

Automated Deduction ◽

Logic Programs ◽

Computing Science ◽

Complete Specification ◽

Representation Of Knowledge

Formal logic is widely accepted as a program specification language in computing science. It is ideally suited to the representation of knowledge and the description of problems without regard to the choice of programming language. Its use as a specification language is compatible not only with conventional programming languages but also with programming languages based entirely on logic itself. In this paper I shall investigate the relation that holds when both programs and program specifications are expressed in formal logic. In many cases, when a specification completely defines the relations to be computed, there is no syntactic distinction between specification and program. Moreover the same mechanism that is used to execute logic programs, namely automated deduction, can also be used to execute logic specifications. Thus all relations defined by complete specifications are executable. The only difference between a complete specification and a program is one of efficiency. A program is more efficient than a specification.

Download Full-text

Logic Programming with Graph Automorphism: Integratingnautywith Prolog (Tool Description)

Theory and Practice of Logic Programming ◽

10.1017/s1471068416000223 ◽

2016 ◽

Vol 16 (5-6) ◽

pp. 688-702

Author(s):

MICHAEL FRANK ◽

MICHAEL CODISH

Keyword(s):

Logic Programming ◽

Software Component ◽

Constraint Solving ◽

Finite Domain ◽

Graph Automorphism ◽

Sat Solvers ◽

Ramsey Graphs ◽

Domain Constraints

AbstractThis paper presents thepl-nautylibrary, a Prolog interface to thenautygraph-automorphism tool. Adding the capabilities ofnautyto Prolog combines the strength of the “generate and prune” approach that is commonly used in logic programming and constraint solving, with the ability to reduce symmetries while reasoning over graph objects. Moreover, it enables the integration ofnautyin existing tool-chains, such as SAT-solvers or finite domain constraints compilers which exist for Prolog. The implementation consists of two components:pl-nauty, an interface connectingnauty's C library with Prolog, andpl-gtools, a Prolog framework integrating the software component ofnauty, calledgtools, with Prolog. The complete tool is available as a SWI-Prolog module. We provide a series of usage examples including two that apply to generate Ramsey graphs.

Download Full-text