📄 logic.htm
字号:
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<html>
<head>
<meta http-equiv="Content-Language" content="en-us">
<title>YALMIP Example : Logic programming</title>
<meta http-equiv="Content-Type" content="text/html; charset=windows-1251">
<meta content="Microsoft FrontPage 6.0" name="GENERATOR">
<meta name="ProgId" content="FrontPage.Editor.Document">
<link href="yalmip.css" type="text/css" rel="stylesheet">
<base target="_self">
</head>
<body leftMargin="0" topMargin="0">
<div align="left">
<table border="0" cellpadding="4" cellspacing="3" style="border-collapse: collapse" bordercolor="#000000" width="100%" align="left" height="100%">
<tr>
<td width="100%" align="left" height="100%" valign="top">
<h2>Logic programming</h2>
<hr noShade SIZE="1" color="#000000">
<p>By using <a href="extoperators.htm">nonlinear operators</a>,
logic programming is easily added to YALMIP. The logic programming
module is not intended to be used for large logic programs, but is
only implemented to help the user to add a small number of logic
constraints to a standard model. Note that logic constraints leads
to a problem with binary variables, hence mixed integer programming
is needed to solve the problem. The logic functionality has not been
tested much, and was mainly implemented to
show the strength of <a href="extoperators.htm">nonlinear operators</a>. A lot of features are
still lacking, but are typically easy to add. If you need it,
make a feature request!</p>
<h3>Simple logic constraints</h3>
<p>As a first example, let us solve a simple
satisfiability problem. Note the use of binary variables
and the <b>TRUE</b> operator (the <b>true</b> operator
takes a variable <b>x </b>and returns the constraint <b>
x≥1</b>.)</p>
<table cellPadding="10" width="100%">
<tr>
<td class="xmpcode">
<pre>binvar a b c d e f
F = set(true((a & b & c) | (d & e & f)));
solvesdp(F);
double([a b c d e f])
<font color="#000000">ans =
0 0 0 1 1 1</font></pre>
</td>
</tr>
</table>
<p>A constraint with a scalar logic expression, generated by
the operators <b>AND</b> or <b>OR</b>, is automatically handled as a truth
constrained variable (although it is strongly advised to
use the truth operator.) Hence the following constraint is
equivalent.</p>
<table cellPadding="10" width="100%">
<tr>
<td class="xmpcode">
<pre>F = set((a & b & c) | (d & e & f));
solvesdp(F);
double([a b c d e f])
<font color="#000000">ans =
0 0 0 1 1 1</font></pre>
</td>
</tr>
</table>
<p>A truth constraint on a standard variable must however be
explicitly stated</p>
<table cellPadding="10" width="100%">
<tr>
<td class="xmpcode">
<pre>F = set((a & b & c) | (d & e & f)) + set(true(d));
solvesdp(F);
double([a b c d e f])
<font color="#000000">ans =
0 0 0 1 1 1</font></pre>
</td>
</tr>
</table>
<p>or equivalently</p>
<table cellPadding="10" width="100%">
<tr>
<td class="xmpcode">
<pre>F = set((a & b & c) | (d & e & f)) + set(d >= 1);
solvesdp(F);
double([a b c d e f])
<font color="#000000">ans =
0 0 0 1 1 1</font></pre>
</td>
</tr>
</table>
<p>To constrain an expression to be false, use the <b>
FALSE</b> operator,</p>
<table cellPadding="10" width="100%">
<tr>
<td class="xmpcode">
<pre>F = set(false((a & b & c) | (d & e & f)));
solvesdp(F);
double([a b c d e f])
<font color="#000000">ans =
1 0 0 1 0 0</font></pre>
</td>
</tr>
</table>
<p>or simply add the corresponding numerical constraint (Notice that
we use inequality instead of equality constraint. The reason is
rather technical but it is recommended, since the convexity
propagation algorithm used for expanding the
<a href="extoperators.htm">nonlinear operators</a> might fail
otherwise)</p>
<table cellPadding="10" width="100%">
<tr>
<td class="xmpcode">
<pre>F = set(((a & b & c) | (d & e & f)) <= 0);
solvesdp(F);
double([a b c d e f])
<font color="#000000">ans =
1 0 0 1 0 0</font></pre>
</td>
</tr>
</table>
<p>Objective functions are allowed.</p>
<table cellPadding="10" width="100%">
<tr>
<td class="xmpcode">
<pre>F = set(((a & b & c) | (d & e & f)) <= 0);
solvesdp(F,-a-b-c-d-e-f);
double([a b c d e f])
<font color="#000000">ans =
1 0 1 1 0 1</font></pre>
</td>
</tr>
</table>
<p>In addition to the operators <b>AND</b> (&), <b>OR</b>
(|) and <b>NOT</b> (~), the operator <b>IMPLIES(X,Y)</b>
is implemeted. To force <b>e</b> to be true if <b>f</b> is
true, we use <b>IMPLIES</b>.</p>
<table cellPadding="10" width="100%">
<tr>
<td class="xmpcode">
<pre>F = set(((a & b & c) | (d & e & f)) <= 0) + set(implies(f,e));
solvesdp(F,-a-b-c-d-e-f);
double([a b c d e f])</pre>
</td>
</tr>
</table>
<p>An equivalent formulation is</p>
<table cellPadding="10" width="100%" id="table2">
<tr>
<td class="xmpcode">
<pre>F = set(((a & b & c) | (d & e & f)) <= 0) + set(e >= f);
solvesdp(F,-a-b-c-d-e-f);
double([a b c d e f])</pre>
</td>
</tr>
</table>
<h3>Mixed logic and conic constraints</h3>
<p>The first construction for creating mixed constraints
is <b>IMPLIES</b>. The following trivial program ensures the
symmetric matrix <b>X</b> to have eigenvalues larger than 1 if
<b>a</b> or <b>b</b> is true. The result is a mixed
integer semidefinite problem which will be solved using
YALMIPs mixed integer solver. Be warned, a lot of the
functionality here is experimental. Please validate your
results and report any oddities as usual.</p>
<table cellPadding="10" width="100%" id="table1">
<tr>
<td class="xmpcode">
<pre>binvar a b
X = sdpvar(3,3);
F = set(implies(a | b, X > eye(3)));
solvesdp(F)</pre>
</td>
</tr>
</table>
<p>The following construction ensures the variable <b>x</b>
to be contained in a polytope if <b>d</b> is true</p>
<table cellPadding="10" width="100%" id="table3">
<tr>
<td class="xmpcode">
<pre>A = randn(5,2);
b = rand(5,1);
x = sdpvar(2,1);
d = binvar(1,1);
F = set(implies(d,A*x <=b))</pre>
</td>
</tr>
</table>
<p>A related command is if-and-only-if, <b>IFF</b>, i.e.
logic equivalence. The following code force the
variable <b>x</b> to be contained in a polytope if <b>y</b> is
contained in the polytope, and vice versa.</p>
<table cellPadding="10" width="100%" id="table4">
<tr>
<td class="xmpcode">
<pre>A = randn(5,2);
b = rand(5,1);
x = sdpvar(2,1);
y = sdpvar(2,1);
F = set(iff(A*x <= b, A*y <= b))</pre>
</td>
</tr>
</table>
<p>This functionality can be used to model various logic
constraints. Consider for instance the constraint that a
variable is in one of several polytopes.
<img border="0" src="polytopes.jpg" width="809" height="472"></p>
<p>The data and plot was generated with the following
code (assuming <a href="solvers.htm#mpt">MPT</a> is
installed)</p>
<table cellPadding="10" width="100%" id="table5">
<tr>
<td class="xmpcode">
<pre>A1 = randn(8,2);
b1 = rand(8,1)*2-A1*[3;3];
A2 = randn(8,2);
b2 = rand(8,1)*2-A2*[-3;3];
A3 = randn(8,2);
b3 = rand(8,1)*2-A3*[3;-3];
A4 = randn(8,2);
b4 = rand(8,1)*2-A4*[-3;-3];
plot(polytope(A1,b1),polytope(A2,b2),polytope(A3,b3),polytope(A4,b4))</pre>
</td>
</tr>
</table>
<p>We will now try to find a point <b>x</b> as far up in
the figure as possible, but still in one of the
polytope. First, we define 4 binary
variables, each one describing whether we are in the
corresponding polytope, and add the constraint that we
are in at least one polytope.</p>
<table cellPadding="10" width="100%" id="table6">
<tr>
<td class="xmpcode">
<pre>binvar inp1 inp2 inp3 inp4
F = set(inp1 | inp2 | inp3 | inp4);</pre>
</td>
</tr>
</table>
<p>To connect the binary variables with the polytopes, we
use the <b>IFF</b> operator.</p>
<table cellPadding="10" width="100%" id="table7">
<tr>
<td class="xmpcode">
<pre>x = sdpvar(2,1);</pre>
<pre>F = F + set(iff(inp1,A1*x < b1));
F = F + set(iff(inp2,A2*x < b2));
F = F + set(iff(inp3,A3*x < b3));
F = F + set(iff(inp4,A4*x < b4));</pre>
</td>
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -