/usr/lib/swi-prolog/doc/Manual/clpb.html

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">

<html>
<head>
<title>SWI-Prolog 7.3.6 Reference Manual: Section A.7</title><link rel="home" href="index.html">
<link rel="contents" href="Contents.html">
<link rel="index" href="DocIndex.html">
<link rel="summary" href="summary.html">
<link rel="previous" href="check.html">
<link rel="next" href="clpfd.html">

<style type="text/css">

/* Style sheet for SWI-Prolog latex2html
*/

dd.defbody
{ margin-bottom: 1em;
}

dt.pubdef, dt.multidef
{ color: #fff;
padding: 2px 10px 0px 10px;
margin-bottom: 5px;
font-size: 18px;
vertical-align: middle;
overflow: hidden;
}

dt.pubdef { background-color: #0c3d6e; }
dt.multidef { background-color: #ef9439; }

.bib dd
{ margin-bottom: 1em;
}

.bib dt
{ float: left;
margin-right: 1.3ex;
}

pre.code
{ margin-left: 1.5em;
margin-right: 1.5em;
border: 1px dotted;
padding-top: 5px;
padding-left: 5px;
padding-bottom: 5px;
background-color: #f8f8f8;
}

div.navigate
{ text-align: center;
background-color: #f0f0f0;
border: 1px dotted;
padding: 5px;
}

div.title
{ text-align: center;
padding-bottom: 1em;
font-size: 200%;
font-weight: bold;
}

div.author
{ text-align: center;
font-style: italic;
}

div.abstract
{ margin-top: 2em;
background-color: #f0f0f0;
border: 1px dotted;
padding: 5px;
margin-left: 10%; margin-right:10%;
}

div.abstract-title
{ text-align: center;
padding: 5px;
font-size: 120%;
font-weight: bold;
}

div.toc-h1
{ font-size: 200%;
font-weight: bold;
}

div.toc-h2
{ font-size: 120%;
font-weight: bold;
margin-left: 2em;
}

div.toc-h3
{ font-size: 100%;
font-weight: bold;
margin-left: 4em;
}

div.toc-h4
{ font-size: 100%;
margin-left: 6em;
}

span.sec-nr
{
}

span.sec-title
{
}

span.pred-ext
{ font-weight: bold;
}

span.pred-tag
{ float: right;
padding-top: 0.2em;
font-size: 80%;
font-style: italic;
color: #fff;
}

div.caption
{ width: 80%;
margin: auto;
text-align:center;
}

/* Footnotes */
.fn {
color: red;
font-size: 70%;
}

.fn-text, .fnp {
position: absolute;
top: auto;
left: 10%;
border: 1px solid #000;
box-shadow: 5px 5px 5px #888;
display: none;
background: #fff;
color: #000;
margin-top: 25px;
padding: 8px 12px;
font-size: larger;
}

sup:hover span.fn-text
{ display: block;
}

/* Lists */

dl.latex
{ margin-top: 1ex;
margin-bottom: 0.5ex;
}

dl.latex dl.latex dd.defbody
{ margin-bottom: 0.5ex;
}

/* PlDoc Tags */

dl.tags
{ font-size: 90%;
margin-left: 5ex;
margin-top: 1ex;
margin-bottom: 0.5ex;
}

dl.tags dt
{ margin-left: 0pt;
font-weight: bold;
}

dl.tags dd
{ margin-left: 3ex;
}

td.param
{ font-style: italic;
font-weight: bold;
}

/* Index */

dt.index-sep
{ font-weight: bold;
font-size: +1;
margin-top: 1ex;
}

/* Tables */

table.center
{ margin: auto;
}

table.latex
{ border-collapse:collapse;
}

table.latex tr
{ vertical-align: text-top;
}

table.latex td,th
{ padding: 2px 1em;
}

table.latex tr.hline td,th
{ border-top: 1px solid black;
}

table.frame-box
{ border: 2px solid black;
}

</style>
</head>
<body style="background:white">
<div class="navigate"><a class="nav" href="index.html"><img src="home.gif" alt="Home"></a>
<a class="nav" href="Contents.html"><img src="index.gif" alt="Contents"></a>
<a class="nav" href="DocIndex.html"><img src="yellow_pages.gif" alt="Index"></a>
<a class="nav" href="summary.html"><img src="info.gif" alt="Summary"></a>
<a class="nav" href="check.html"><img src="prev.gif" alt="Previous"></a>
<a class="nav" href="clpfd.html"><img src="next.gif" alt="Next"></a>
</div>
<h2 id="sec:clpb"><a id="sec:A.7"><span class="sec-nr">A.7</span> <span class="sec-title">library(clpb): 
Constraint Logic Programming over Boolean Variables</span></a></h2>

<p><a id="sec:clpb"></a>

<dl class="tags">
<dt class="tag">author</dt>
<dd>
Markus Triska
</dd>
</dl>

<p><h4 id="sec:clpb-intro"><a id="sec:A.7.1"><span class="sec-nr">A.7.1</span> <span class="sec-title">Introduction</span></a></h4>

<p><a id="sec:clpb-intro"></a>

<p>Constraint programming is a declarative formalism that lets you state 
relations between terms. This library provides CLP(B), Constraint Logic 
Programming over Boolean Variables. It can be used to model and solve 
combinatorial problems such as verification, allocation and covering 
tasks.

<p>The implementation is based on reduced and ordered Binary Decision 
Diagrams (BDDs).

<p><h4 id="sec:clpb-exprs"><a id="sec:A.7.2"><span class="sec-nr">A.7.2</span> <span class="sec-title">Boolean 
expressions</span></a></h4>

<p><a id="sec:clpb-exprs"></a>

<p>A <i>Boolean expression</i> is one of:
<blockquote>
<table class="latex frame-box">
<tr><td><code>0</code> </td><td>false </td></tr>
<tr><td><code>1</code> </td><td>true </td></tr>
<tr><td><i>variable</i> </td><td>unknown truth value </td></tr>
<tr><td><code>~</code> <i>Expr</i> </td><td>logical NOT </td></tr>
<tr><td><i>Expr</i> + <i>Expr</i> </td><td>logical OR </td></tr>
<tr><td><i>Expr</i> * <i>Expr</i> </td><td>logical AND </td></tr>
<tr><td><i>Expr</i> # <i>Expr</i> </td><td>exclusive OR </td></tr>
<tr><td><i>Var</i> <code>^</code> <i>Expr</i> </td><td>existential 
quantification </td></tr>
<tr><td><i>Expr</i> <code>=:=</code> <i>Expr</i> </td><td>equality </td></tr>
<tr><td><i>Expr</i> <code>=\=</code> <i>Expr</i> </td><td>disequality 
(same as #) </td></tr>
<tr><td><i>Expr</i> <code>=&lt;</code> <i>Expr</i> </td><td>less or 
equal (implication) </td></tr>
<tr><td><i>Expr</i> <code>&gt;=</code> <i>Expr</i> </td><td>greater or 
equal </td></tr>
<tr><td><i>Expr</i> <var>&lt;</var> <i>Expr</i> </td><td>less than </td></tr>
<tr><td><i>Expr</i> <var>&gt;</var> <i>Expr</i> </td><td>greater than </td></tr>
<tr><td><code>card(Is,Exprs)</code> </td><td><i>see below</i> </td></tr>
<tr><td><code>+(Exprs)</code> </td><td><i>see below</i> </td></tr>
<tr><td><code>*(Exprs)</code> </td><td><i>see below</i> </td></tr>
</table>
</blockquote>

<p>where <i>Expr</i> again denotes a Boolean expression.

<p>The Boolean expression <code>card(Is,Exprs)</code> is true iff the 
number of true expressions in the list <var>Exprs</var> is a member of 
the list <var>Is</var> of integers and integer ranges of the form <code>From-To</code>.

<p><code>+(Exprs)</code> and <code>*(Exprs)</code> denote, respectively, 
the disjunction and conjunction of all elements in the list <var>Exprs</var> 
of Boolean expressions.

<p><h4 id="sec:clpb-interface"><a id="sec:A.7.3"><span class="sec-nr">A.7.3</span> <span class="sec-title">Interface 
predicates</span></a></h4>

<p><a id="sec:clpb-interface"></a>

<p>Important interface predicates of CLP(B) are:

<dl class="latex">
<dt><strong>sat</strong>(<var>+Expr</var>)</dt>
<dd class="defbody">
True iff the Boolean expression <var>Expr</var> is satisfiable.
</dd>
<dt><strong>taut</strong>(<var>+Expr, -T</var>)</dt>
<dd class="defbody">
If <var>Expr</var> is a tautology with respect to the posted 
constraints, succeeds with <b><var>T</var> = 1</b>. If <var>Expr</var> 
cannot be satisfied, succeeds with <b><var>T</var> = 0</b>. Otherwise, 
it fails.
</dd>
<dt><strong>labeling</strong>(<var>+Vs</var>)</dt>
<dd class="defbody">
Assigns truth values to the variables <var>Vs</var> such that all 
constraints are satisfied.
</dd>
</dl>

<p>The unification of a CLP(B) variable <i>X</i> with a term <i>T</i> is 
equivalent to posting the constraint <code>sat(X=:=T)</code>.

<p><h4 id="sec:clpb-examples"><a id="sec:A.7.4"><span class="sec-nr">A.7.4</span> <span class="sec-title">Examples</span></a></h4>

<p><a id="sec:clpb-examples"></a>

<p>Here is an example session with a few queries and their answers:

<pre class="code">
?- use_module(library(clpb)).
true.

?- sat(X*Y).
X = Y, Y = 1.

?- sat(X * ~X).
false.

?- taut(X * ~X, T).
T = 0,
sat(X=:=X).

?- sat(X^Y^(X+Y)).
sat(X=:=X),
sat(Y=:=Y).

?- sat(X*Y + X*Z), labeling([X,Y,Z]).
X = Z, Z = 1, Y = 0 ;
X = Y, Y = 1, Z = 0 ;
X = Y, Y = Z, Z = 1.

?- sat(X =&lt; Y), sat(Y =&lt; Z), taut(X =&lt; Z, T).
T = 1,
sat(1#X#X*Y),
sat(1#Y#Y*Z).
</pre>

<p>The pending residual goals constrain remaining variables to Boolean 
expressions and are declaratively equivalent to the original query.

<dl class="latex">
<dt class="pubdef"><span class="pred-tag">[semidet]</span><a id="sat/1"><strong>sat</strong>(<var>+Expr</var>)</a></dt>
<dd class="defbody">
True iff <var>Expr</var> is a satisfiable Boolean expression.</dd>
<dt class="pubdef"><span class="pred-tag">[semidet]</span><a id="taut/2"><strong>taut</strong>(<var>+Expr, 
-T</var>)</a></dt>
<dd class="defbody">
Succeeds with <var>T</var> = 0 if the Boolean expression <var>Expr</var> 
cannot be satisfied, and with <var>T</var> = 1 if <var>Expr</var> is 
always true with respect to the current constraints. Fails otherwise.</dd>
<dt class="pubdef"><span class="pred-tag">[multi]</span><a id="labeling/1"><strong>labeling</strong>(<var>+Vs</var>)</a></dt>
<dd class="defbody">
Assigns truth values to the Boolean variables <var>Vs</var> such that 
all stated constraints are satisfied.</dd>
<dt class="pubdef"><span class="pred-tag">[det]</span><a id="sat_count/2"><strong>sat_count</strong>(<var>+Expr, 
-N</var>)</a></dt>
<dd class="defbody">
<var>N</var> is the number of different assignments of truth values to 
the variables in the Boolean expression <var>Expr</var>, such that <var>Expr</var> 
is true and all posted constraints are satisfiable.

<p>Example:

<pre class="code">
?- length(Vs, 120), sat_count(+Vs, CountOr), sat_count(*(Vs), CountAnd).
Vs = [...],
CountOr = 1329227995784915872903807060280344575,
CountAnd = 1.
</pre>

<p></dd>
</dl>

<p></body></html>
swi-prolog-nox 7.2.3-2 / usr / lib / swi-prolog / doc / Manual / clpb.html
