Created
April 18, 2017 18:14
-
-
Save rndmcnlly/aa100fa479e012fccfa2b4ba2e9c7551 to your computer and use it in GitHub Desktop.
Tutorial from a lecture on Modeling Optimization Problems in an Applied Answer Set Programming course at UC Santa Cruz (Spring 2017)
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{ | |
"cells": [ | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"In this notebook, I'm sketching ideas for a lecture on *Modeling Optimization Problems*\n", | |
"\n", | |
"Outline from my ideation notes:\n", | |
" - basic syntax\n", | |
" - cardinality optimization\n", | |
" - weighted optimization\n", | |
" - prioritized optimization\n", | |
" - approximate optimization (incomplete b&b)\n", | |
" - comparison with heuristics\n", | |
" - Subset minimality\n", | |
" - Pareto optimality" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"# Running Example: Making Change\n", | |
"\n", | |
"Types of US coins:\n", | |
"- penny, 1¢\n", | |
"- nickel, 5¢\n", | |
"- dime, 10¢\n", | |
"- quarter, 25¢\n", | |
"\n", | |
"Let suppose we have 10 instances of each type of coin. Each type of coin obviously has a different monetary value, but they also have a weight that does not scale proportionally to monetary value. Additionally, each instance is unique, with different scuffs and scratches. Given a target amount of money to transfer, how should we select the individual coins?" | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 1, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"Overwriting coin-specs.lp\n" | |
] | |
} | |
], | |
"source": [ | |
"%%file coin-specs.lp\n", | |
"\n", | |
"% coin_spec(Type,Cents,MassInMilligrams)\n", | |
"coin_spec(penny, 1, 2500).\n", | |
"coin_spec(nickel, 5, 5000).\n", | |
"coin_spec(dime, 10, 2268).\n", | |
"coin_spec(quarter, 25, 5670).\n", | |
"\n", | |
"% some unique coins of each type\n", | |
"coin((Type,0..9)) :- coin_spec(Type,_,_)." | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"# Just Making Change" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"Give me a buck fifteen, however you like." | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 2, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"Overwriting buck-fifteen.lp\n" | |
] | |
} | |
], | |
"source": [ | |
"%%file buck-fifteen.lp\n", | |
"\n", | |
"#const target=115.\n", | |
"\n", | |
"{ select(C) } :- coin(C). % I could give you any of these coins.\n", | |
":- not target = #sum { Cents,C: select(C), C=(Type,I), coin_spec(Type,Cents,Mass) }.\n", | |
" \n", | |
"#show select/1." | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 3, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"clingo version 5.1.0\r\n", | |
"Reading from coin-specs.lp ...\r\n", | |
"Solving...\r\n", | |
"Answer: 1\r\n", | |
"select((nickel,0)) select((dime,0)) select((quarter,0)) select((nickel,1)) select((dime,1)) select((quarter,1)) select((dime,2)) select((quarter,2))\r\n", | |
"SATISFIABLE\r\n", | |
"\r\n", | |
"Models : 1+\r\n", | |
"Calls : 1\r\n", | |
"Time : 0.002s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)\r\n", | |
"CPU Time : 0.000s\r\n" | |
] | |
} | |
], | |
"source": [ | |
"!clingo coin-specs.lp buck-fifteen.lp" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"Let's clean that up a bit. The `select2glyph.py` will throw away the individual coin identities to make things more readable." | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 4, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"10¢ 10¢ 10¢ 5¢ 5¢ 25¢ 25¢ 25¢\r\n" | |
] | |
} | |
], | |
"source": [ | |
"!clingo coin-specs.lp buck-fifteen.lp --outf=2 | python select2glyph.py" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"# Optimize the Coin Count (Cardinality Optimization)" | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 5, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"Overwriting min-count.lp\n" | |
] | |
} | |
], | |
"source": [ | |
"%%file min-count.lp\n", | |
"#minimize { 1,C: select(C) }." | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 6, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"clingo version 5.1.0\n", | |
"Reading from coin-specs.lp ...\n", | |
"Solving...\n", | |
"Answer: 1\n", | |
"select((nickel,0)) select((dime,0)) select((quarter,0)) select((nickel,1)) select((dime,1)) select((quarter,1)) select((dime,2)) select((quarter,2))\n", | |
"Optimization: 8\n", | |
"Answer: 2\n", | |
"select((dime,0)) select((quarter,0)) select((dime,1)) select((quarter,1)) select((dime,2)) select((quarter,2)) select((dime,3))\n", | |
"Optimization: 7\n", | |
"Answer: 3\n", | |
"select((quarter,0)) select((nickel,1)) select((quarter,1)) select((dime,2)) select((quarter,2)) select((quarter,3))\n", | |
"Optimization: 6\n", | |
"OPTIMUM FOUND\n", | |
"\n", | |
"Models : 3\n", | |
" Optimum : yes\n", | |
"Optimization : 6\n", | |
"Calls : 1\n", | |
"Time : 1.634s (Solving: 1.63s 1st Model: 0.00s Unsat: 1.63s)\n", | |
"CPU Time : 1.620s\n" | |
] | |
} | |
], | |
"source": [ | |
"!clingo coin-specs.lp buck-fifteen.lp min-count.lp" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"The solver found a first solution, and then sequentially tried to find solutions that improved on that, until it finally hit an UNSAT case (proving the previous solution was optimal). According to the timing data, almost all of the time was spent on that last UNSAT case.\n", | |
"\n", | |
"If we don't want to see anything but an optimal solution, we can ask for that." | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 7, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"clingo version 5.1.0\n", | |
"Reading from coin-specs.lp ...\n", | |
"Solving...\n", | |
"Answer: 3\n", | |
"select((quarter,0)) select((nickel,1)) select((quarter,1)) select((dime,2)) select((quarter,2)) select((quarter,3))\n", | |
"Optimization: 6\n", | |
"OPTIMUM FOUND\n", | |
"\n", | |
"Models : 3\n", | |
" Optimum : yes\n", | |
"Optimization : 6\n", | |
"Calls : 1\n", | |
"Time : 1.516s (Solving: 1.51s 1st Model: 0.00s Unsat: 1.51s)\n", | |
"CPU Time : 1.510s\n" | |
] | |
} | |
], | |
"source": [ | |
"!clingo coin-specs.lp buck-fifteen.lp min-count.lp --quiet=1" | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 8, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"6 : 10¢ 5¢ 25¢ 25¢ 25¢ 25¢\r\n" | |
] | |
} | |
], | |
"source": [ | |
"!clingo coin-specs.lp buck-fifteen.lp min-count.lp --quiet=1 --outf=2 | python select2glyph.py" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"Maximization is also possible:" | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 9, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"Overwriting max-count.lp\n" | |
] | |
} | |
], | |
"source": [ | |
"%%file max-count.lp\n", | |
"#maximize { 1,C: select(C) }." | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 10, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"-25 : 10¢ 10¢ 10¢ 10¢ 10¢ 10¢ 5¢ 5¢ 5¢ 5¢ 5¢ 5¢ 5¢ 5¢ 5¢ 1¢ 1¢ 1¢ 1¢ 1¢ 1¢ 1¢ 1¢ 1¢ 1¢\r\n" | |
] | |
} | |
], | |
"source": [ | |
"!clingo coin-specs.lp buck-fifteen.lp max-count.lp --quiet=1 --outf=2 | python select2glyph.py" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"# Optimize the Coin Mass (Weight Optimization)" | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 11, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"Overwriting min-mass.lp\n" | |
] | |
} | |
], | |
"source": [ | |
"%%file min-mass.lp\n", | |
"#minimize { Mass,C: select(C),C=(T,I),coin_spec(T,Cents,Mass) }." | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 12, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"26082 : 10¢ 10¢ 10¢ 10¢ 25¢ 25¢ 25¢\r\n" | |
] | |
} | |
], | |
"source": [ | |
"!clingo coin-specs.lp buck-fifteen.lp min-mass.lp --quiet=1 --outf=2 | python select2glyph.py" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"# Optimize by Denomination (Prioritized Optimization)" | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 13, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"Overwriting min-count-prio.lp\n" | |
] | |
} | |
], | |
"source": [ | |
"%%file min-count-prio.lp\n", | |
"#minimize { 1@Cents,C: select(C),C=(T,I),coin_spec(T,Cents,Mass) }." | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 14, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"0 6 9 10 : 10¢ 10¢ 10¢ 10¢ 10¢ 10¢ 5¢ 5¢ 5¢ 5¢ 5¢ 5¢ 5¢ 5¢ 5¢ 1¢ 1¢ 1¢ 1¢ 1¢ 1¢ 1¢ 1¢ 1¢ 1¢\r\n" | |
] | |
} | |
], | |
"source": [ | |
"!clingo coin-specs.lp buck-fifteen.lp min-count-prio.lp --quiet=1 --outf=2 | python select2glyph.py" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"This looks equivalent to when we tried to maximize the count count, but we were trying to minimze What gives?\n", | |
"\n", | |
"Prioritized minimization said this: At high priority (level 25) try to give out as few quarters as possible. Amongst solutions tied for giving out the fewest quarters, minimize the number of dimes given out (level 10), and so on. By squeezing down the usage if higher denominations, we had to use more pennies. The limited supply of pennies and nickels forced usage of six dimes, however." | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"# Early Termination (Approximate Optimization)" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"Let's revisit one of those slower cases. Almost all of these problems found solutions quickly, but they bogged down in proving optimality. What if we were making an interactive application where we needed to respond within one second?" | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 15, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"clingo version 5.1.0\n", | |
"Reading from coin-specs.lp ...\n", | |
"Solving...\n", | |
"OPTIMUM FOUND\n", | |
"\n", | |
"Models : 2\n", | |
" Optimum : yes\n", | |
"Optimization : 26082\n", | |
"Calls : 1\n", | |
"Time : 7.958s (Solving: 7.96s 1st Model: 0.00s Unsat: 7.96s)\n", | |
"CPU Time : 7.940s\n" | |
] | |
} | |
], | |
"source": [ | |
"!clingo coin-specs.lp buck-fifteen.lp min-mass.lp -q" | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 16, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"clingo version 5.1.0\n", | |
"Reading from coin-specs.lp ...\n", | |
"Solving...\n", | |
"*** Info : (clingo): INTERRUPTED by signal!\n", | |
"SATISFIABLE\n", | |
"\n", | |
"TIME LIMIT : 1\n", | |
"Models : 2+\n", | |
" Optimum : unknown\n", | |
"Optimization : 26082\n", | |
"Calls : 1\n", | |
"Time : 1.002s (Solving: 1.00s 1st Model: 0.00s Unsat: 0.00s)\n", | |
"CPU Time : 1.000s\n" | |
] | |
} | |
], | |
"source": [ | |
"!clingo coin-specs.lp buck-fifteen.lp min-mass.lp --time-limit=1 -q" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"This roughly says \"I could find a solution with mass $26.082$ grams, but I don't know if it is optimal.\"" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"While the user is thinking about this candidate solution, we can continue to check in the background:" | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 17, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"clingo version 5.1.0\n", | |
"Reading from coin-specs.lp ...\n", | |
"Solving...\n", | |
"OPTIMUM FOUND\n", | |
"\n", | |
"Models : 1\n", | |
" Optimum : yes\n", | |
"Optimization : 26082\n", | |
"Calls : 1\n", | |
"Time : 6.997s (Solving: 6.99s 1st Model: 0.00s Unsat: 6.99s)\n", | |
"CPU Time : 6.980s\n" | |
] | |
} | |
], | |
"source": [ | |
"!clingo coin-specs.lp buck-fifteen.lp min-mass.lp --opt-bound=26082 -q" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"# Comparison with Heuristics (Heuristic Optimization)" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"Sometimes we'd be happy with any solution, but we'd like to specify information similar to optimization criteria as a way of speeding up the search process.\n", | |
"\n", | |
"Let's add some side constraints so that the problem isn't completely trivial. These constraints will rule out the first solution to the non-optimization problem." | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 18, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"Overwriting no-triples.lp\n" | |
] | |
} | |
], | |
"source": [ | |
"%%file no-triples.lp\n", | |
":- coin_spec(T,_,_), 3 { select((T,I)):coin((T,I)) } 3." | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 19, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"clingo version 5.1.0\r\n", | |
"Reading from coin-specs.lp ...\r\n", | |
"Solving...\r\n", | |
"SATISFIABLE\r\n", | |
"\r\n", | |
"Models : 1+\r\n", | |
"Calls : 1\r\n", | |
"Time : 0.005s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)\r\n", | |
"CPU Time : 0.000s\r\n", | |
"\r\n", | |
"Choices : 130 \r\n", | |
"Conflicts : 83 (Analyzed: 83)\r\n", | |
"Restarts : 1 (Average: 83.00 Last: 10)\r\n", | |
"Model-Level : 25.0 \r\n", | |
"Problems : 1 (Average Length: 0.00 Splits: 0)\r\n", | |
"Lemmas : 83 (Deleted: 0)\r\n", | |
" Binary : 0 (Ratio: 0.00%)\r\n", | |
" Ternary : 0 (Ratio: 0.00%)\r\n", | |
" Conflict : 83 (Average Length: 12.4 Ratio: 100.00%) \r\n", | |
" Loop : 0 (Average Length: 0.0 Ratio: 0.00%) \r\n", | |
" Other : 0 (Average Length: 0.0 Ratio: 0.00%) \r\n", | |
"Backjumps : 83 (Average: 1.07 Max: 2 Sum: 89)\r\n", | |
" Executed : 83 (Average: 1.07 Max: 2 Sum: 89 Ratio: 100.00%)\r\n", | |
" Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)\r\n", | |
"\r\n", | |
"Rules : 108 \r\n", | |
" Choice : 40 \r\n", | |
"Atoms : 103 \r\n", | |
"Bodies : 16 \r\n", | |
" Sum : 2 \r\n", | |
" Count : 8 \r\n", | |
"Equivalences : 12 (Atom=Atom: 1 Body=Body: 0 Other: 11)\r\n", | |
"Tight : Yes\r\n", | |
"Variables : 49 (Eliminated: 0 Frozen: 49)\r\n", | |
"Constraints : 14 (Binary: 28.6% Ternary: 0.0% Other: 71.4%)\r\n", | |
"\r\n" | |
] | |
} | |
], | |
"source": [ | |
"!clingo coin-specs.lp buck-fifteen.lp no-triples.lp --stats -q" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"The solver had to backtrack 83 times before finding a solution (using whatever default heuristics it uses internally). We can do better.\n", | |
"\n", | |
"Let's tell the solver to decide on the most valuable coins first, and when deciding a coin, it should include it by default. Once it has included enough of a certain type of big coin, constraint propagation will automatically make the rest of the coins of that type unavailable." | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 20, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"Overwriting tips.lp\n" | |
] | |
} | |
], | |
"source": [ | |
"%%file tips.lp\n", | |
"#heuristic select((T,I)):coin_spec(T,Cents,Mass). [Cents,level]\n", | |
"#heuristic select((T,I)):coin_spec(T,Cents,Mass). [1,sign]" | |
] | |
}, | |
{ | |
"cell_type": "code", | |
"execution_count": 21, | |
"metadata": { | |
"collapsed": false, | |
"deletable": true, | |
"editable": true | |
}, | |
"outputs": [ | |
{ | |
"name": "stdout", | |
"output_type": "stream", | |
"text": [ | |
"clingo version 5.1.0\r\n", | |
"Reading from coin-specs.lp ...\r\n", | |
"Solving...\r\n", | |
"SATISFIABLE\r\n", | |
"\r\n", | |
"Models : 1+\r\n", | |
"Calls : 1\r\n", | |
"Time : 0.003s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)\r\n", | |
"CPU Time : 0.000s\r\n", | |
"\r\n", | |
"Choices : 6 (Domain: 6)\r\n", | |
"Conflicts : 0 (Analyzed: 0)\r\n", | |
"Restarts : 0 \r\n", | |
"Model-Level : 6.0 \r\n", | |
"Problems : 1 (Average Length: 0.00 Splits: 0)\r\n", | |
"Lemmas : 0 (Deleted: 0)\r\n", | |
" Binary : 0 (Ratio: 0.00%)\r\n", | |
" Ternary : 0 (Ratio: 0.00%)\r\n", | |
" Conflict : 0 (Average Length: 0.0 Ratio: 0.00%) \r\n", | |
" Loop : 0 (Average Length: 0.0 Ratio: 0.00%) \r\n", | |
" Other : 0 (Average Length: 0.0 Ratio: 0.00%) \r\n", | |
"Backjumps : 0 (Average: 0.00 Max: 0 Sum: 0)\r\n", | |
" Executed : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)\r\n", | |
" Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 100.00%)\r\n", | |
"\r\n", | |
"Rules : 188 \r\n", | |
" Choice : 40 \r\n", | |
" Heuristic : 80 \r\n", | |
"Atoms : 103 \r\n", | |
"Bodies : 16 \r\n", | |
" Sum : 2 \r\n", | |
" Count : 8 \r\n", | |
"Equivalences : 12 (Atom=Atom: 1 Body=Body: 0 Other: 11)\r\n", | |
"Tight : Yes\r\n", | |
"Variables : 49 (Eliminated: 0 Frozen: 49)\r\n", | |
"Constraints : 14 (Binary: 28.6% Ternary: 0.0% Other: 71.4%)\r\n", | |
"\r\n" | |
] | |
} | |
], | |
"source": [ | |
"!clingo coin-specs.lp buck-fifteen.lp no-triples.lp tips.lp --heu=domain --stats -q" | |
] | |
}, | |
{ | |
"cell_type": "markdown", | |
"metadata": { | |
"deletable": true, | |
"editable": true | |
}, | |
"source": [ | |
"Whee! The search terminated after six choices and *no* conflicts.\n", | |
"\n", | |
"This had the same effect as using prioritized optimization to maximize the number of coins in each class, starting at the highest." | |
] | |
} | |
], | |
"metadata": { | |
"kernelspec": { | |
"display_name": "Python 2", | |
"language": "python", | |
"name": "python2" | |
}, | |
"language_info": { | |
"codemirror_mode": { | |
"name": "ipython", | |
"version": 2 | |
}, | |
"file_extension": ".py", | |
"mimetype": "text/x-python", | |
"name": "python", | |
"nbconvert_exporter": "python", | |
"pygments_lexer": "ipython2", | |
"version": "2.7.12" | |
} | |
}, | |
"nbformat": 4, | |
"nbformat_minor": 2 | |
} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment