From e6d13becb5e9566d6d12ffa247bd076237c34180 Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Mon, 26 Oct 2015 16:24:02 +0100 Subject: [PATCH] update with dynamic solution for problem 1 --- .gitignore | 1 + 1.tex | 20 +++----------- Makefile | 24 ++++++++++------- a.tex | 4 +-- ar.tex | 17 ++++++++++++ preamble.tex => pre.tex | 0 src/a1.bash | 60 ++++++++++++++++++++++++++++++++++++++++- src/a1.py | 29 ++++++++++++++++++++ src/a1.smt | 60 ----------------------------------------- 9 files changed, 126 insertions(+), 89 deletions(-) rename preamble.tex => pre.tex (100%) create mode 100644 src/a1.py delete mode 100644 src/a1.smt diff --git a/.gitignore b/.gitignore index 94feb01..52dfa5e 100644 --- a/.gitignore +++ b/.gitignore @@ -6,3 +6,4 @@ *.toc *.pdf *.png +a[1234].tex diff --git a/1.tex b/1.tex index 098a2e3..585e0cd 100644 --- a/1.tex +++ b/1.tex @@ -79,13 +79,13 @@ going over all pallets. \subsection{SMT format solution} The formula is easily convertable to SMT format by literal conversion and is -listed in Listing~\ref{listing:a1.smt}. The maximization is done by +listed in Listing~\ref{listing:a1.bash}. The maximization is done by incrementing a special variable called \texttt{} which is an instantiation of $n(p)$. When the iteration yields unsat we know that the current number minus one is the maximum amount of prittles the trucks can carry. The maximization is done with a bash script shown in Listing~\ref{listing:1.bash}. -\lstinputlisting[language=bash, +\lstinputlisting[language=bash,firstline=66, caption={Iteratively find the largest solution for problem 1}, label={listing:1.bash}]{src/a1.bash} @@ -95,21 +95,7 @@ this solution takes less then $0.12$ seconds and is shown in Table~\ref{tab:s1}. \begin{table}[H] \centering - \begin{tabular}{l|lllll|ll} - \toprule - Truck & Nuzzles & Prittles & Skipples & Crottles & Dupples & - Weight & Pallets\\ - \midrule - 1 & 0 & 0 & 4 & 2 & 1 & 7100 & 7\\ - 2 & 0 & 3 & 4 & 0 & 1 & 6500 & 8\\ - 3 & 0 & 8 & 0 & 0 & 0 & 6400 & 7\\ - 4 & 0 & 7 & 0 & 0 & 1 & 5700 & 8\\ - 5 & 0 & 0 & 0 & 5 & 1 & 7600 & 6\\ - 6 & 4 & 0 & 0 & 3 & 1 & 7400 & 8\\ - \midrule - total & 4 & 18 & 8 & 10 & 5 & &\\ - \bottomrule - \end{tabular} +\input{a1.tex} \caption{Solution visualization for problem 1} \label{tab:s1} \end{table} diff --git a/Makefile b/Makefile index 376182a..99b075d 100644 --- a/Makefile +++ b/Makefile @@ -1,20 +1,26 @@ LATEX:=pdflatex DOCUMENT:=ar -SOURCES:=$(filter-out preamble.tex,$(shell ls *.tex)) -LISTINGS:=$(shell ls src/*) -IMAGES:=$(shell ls *.png) +PROBLEMS:=1 2 3 4 -.SECONDARY: $(addsuffix .fmt,$(DOCUMENT)) +SOURCES:=$(DOCUMENT).tex $(addsuffix .tex,$(PROBLEMS)) +LISTINGS:=$(addprefix src/a,$(addsuffix .bash,$(PROBLEMS))) +SOLUTIONS:=$(addprefix a,$(addsuffix .tex,$(PROBLEMS))) + +.SECONDARY: $(DOCUMENT).fmt $(SOLUTIONS) +.PHONY: solutions all: $(DOCUMENT).pdf -%.pdf: %.tex %.fmt $(SOURCES) $(LISTINGS) $(IMAGES) - $(LATEX) $(basename $@) - $(LATEX) $(basename $@) +%.pdf: %.tex %.fmt $(SOURCES) $(LISTINGS) $(SOLUTIONS) + $(LATEX) $(basename $<) + $(LATEX) $(basename $<) -%.fmt: preamble.tex +%.fmt: pre.tex $(LATEX) -ini -jobname="$(basename $@)" "&$(LATEX) $<\dump" +a%.tex: src/a%.bash + bash $< $@ >/dev/null + clean: - $(RM) -v $(addprefix $(DOCUMENT).,fmt aux log out toc pdf) + $(RM) -v $(addprefix $(DOCUMENT).,fmt aux log out toc pdf) $(SOLUTIONS) diff --git a/a.tex b/a.tex index 9785572..ef0b82a 100644 --- a/a.tex +++ b/a.tex @@ -6,8 +6,8 @@ RAM: 8GB \end{lstlisting} \newpage -\lstinputlisting[language=lisp,caption={a1.smt}, - label={listing:a1.smt}]{src/a1.smt} +\lstinputlisting[language=lisp,caption={a1.bash}, + label={listing:a1.bash}]{src/a1.bash} \newpage \lstinputlisting[language=python,caption={a2.py}, diff --git a/ar.tex b/ar.tex index 94e25f9..b79c70c 100644 --- a/ar.tex +++ b/ar.tex @@ -3,6 +3,23 @@ \maketitle \tableofcontents +\section{Introduction} +Implementing all the problems by hand in SMT-Lib format would be too much work +and therefore all problems have an accompanying bash script that does the +generation and/or the mini or maximization. The bash scripts all have a +function defined called \lstinline{generate} with a parameter that will be used +for mini or maximization. All solving is done on the benchmark system listed in +Listing~\ref{listing:benchmark}. + +\begin{lstlisting}[caption={Benchmark system},label={listing:benchmark}] +CPU: 3600MHz AMD FX(tm)-4100 Quad-Core Processor +RAM: 8GB + +Yices: 2.4.1 +SMT-Lib: 1.2 +Bash: 4.3.30(1) +\end{lstlisting} + \newpage \input{1.tex} diff --git a/preamble.tex b/pre.tex similarity index 100% rename from preamble.tex rename to pre.tex diff --git a/src/a1.bash b/src/a1.bash index 339536f..5e71a17 100644 --- a/src/a1.bash +++ b/src/a1.bash @@ -1,6 +1,64 @@ +function generate { + cat<= t1p 0) (>= t1n 0) (>= t1s 0) (>= t1c 0) (>= t1d 0) + (>= t2p 0) (>= t2n 0) (>= t2s 0) (>= t2c 0) (>= t2d 0) + (>= t3p 0) (>= t3n 0) (>= t3s 0) (>= t3c 0) (>= t3d 0) + (>= t4p 0) (>= t4n 0) (>= t4s 0) (>= t4c 0) (>= t4d 0) + (>= t5p 0) (>= t5n 0) (>= t5s 0) (>= t5c 0) (>= t5d 0) + (>= t6p 0) (>= t6n 0) (>= t6s 0) (>= t6c 0) (>= t6d 0) + + (<= (+ t1p t1n t1s t1c t1d) 8) + (<= (+ t2p t2n t2s t2c t2d) 8) + (<= (+ t3p t3n t3s t3c t3d) 8) + (<= (+ t4p t4n t4s t4c t4d) 8) + (<= (+ t5p t5n t5s t5c t5d) 8) + (<= (+ t6p t6n t6s t6c t6d) 8) + + (<= (+ (* t1n 700) (* t1p 800) (* t1s 1000) (* t1c 1500) (* t1d 100)) 7800) + (<= (+ (* t2n 700) (* t2p 800) (* t2s 1000) (* t2c 1500) (* t2d 100)) 7800) + (<= (+ (* t3n 700) (* t3p 800) (* t3s 1000) (* t3c 1500) (* t3d 100)) 7800) + (<= (+ (* t4n 700) (* t4p 800) (* t4s 1000) (* t4c 1500) (* t4d 100)) 7800) + (<= (+ (* t5n 700) (* t5p 800) (* t5s 1000) (* t5c 1500) (* t5d 100)) 7800) + (<= (+ (* t6n 700) (* t6p 800) (* t6s 1000) (* t6c 1600) (* t6d 100)) 7800) + + (or (= 0 t1p) (= 0 t1c)) + (or (= 0 t2p) (= 0 t2c)) + (or (= 0 t3p) (= 0 t3c)) + (or (= 0 t4p) (= 0 t4c)) + (or (= 0 t5p) (= 0 t5c)) + (or (= 0 t6p) (= 0 t6c)) + + (<= t1d 1) (<= t2d 1) (<= t3d 1) (<= t4d 1) (<= t5d 1) (<= t6d 1) + + (= t3s 0) (= t4s 0) (= t5s 0) (= t6s 0) + + (= (+ t1n t2n t3n t4n t5n t6n) 4) + (= (+ t1s t2s t3s t4s t5s t6s) 8) + (= (+ t1c t2c t3c t4c t5c t6c) 10) + (= (+ t1d t2d t3d t4d t5d t6d) 5) + + (>= (+ t1p t2p t3p t4p t5p t6p) $1) +) +) +GENERATE +} + i=1 -while [ $(sed "s//$i/g" a1.smt | yices-smt) = "sat" ]; do +while [ $(generate $i | yices-smt) = "sat" ]; do echo "n(p)=$i is still sat" i=$((i+1)) done echo "n(p)=$i is unsat thus maximum n(p)=$((i-1))" +generate $((i-1)) | yices-smt -m | python3 src/a1.py > $1 diff --git a/src/a1.py b/src/a1.py new file mode 100644 index 0000000..bcfa087 --- /dev/null +++ b/src/a1.py @@ -0,0 +1,29 @@ +#!/usr/bin/env python3 +import sys + +trucks = {} +pallets = {'p': 'Prittles', 'n': 'Nuzzles', 'c': 'Crottles', + 's': 'Skipples', 'd': 'Dupples'} + +for line in sys.stdin: + if line.startswith('(='): + truck = line[4] + pallet = line[5] + + number = int(line[7:-2]) + trucks[truck] = trucks.get(truck, {}) + trucks[truck][pallets[pallet]] = number + +print('$\\begin{array}{|l|lllll|}') +print('\t\\toprule') +print('\tTruck & {}\\\\'.format(' & '.join(sorted(pallets.values())))) +print('\t\\midrule') +for truck in sorted(trucks): + print('\t{} & {}\\\\'.format(truck, ' & '.join( + str(p[1]) for p in sorted(trucks[truck].items())))) +print('\t\\midrule') +print('\tTotal & {}\\\\'.format(' & '.join( + str(sum(t[p] for t in trucks.values())) for p in + sorted(pallets.values())))) +print('\t\\bottomrule') +print('\\end{array}$') diff --git a/src/a1.smt b/src/a1.smt deleted file mode 100644 index cf5342e..0000000 --- a/src/a1.smt +++ /dev/null @@ -1,60 +0,0 @@ -(benchmark a1.smt -:logic QF_UFLIA -:extrafuns ( - (t1p Int) (t1n Int) (t1s Int) (t1c Int) (t1d Int) - (t2p Int) (t2n Int) (t2s Int) (t2c Int) (t2d Int) - (t3p Int) (t3n Int) (t3s Int) (t3c Int) (t3d Int) - (t4p Int) (t4n Int) (t4s Int) (t4c Int) (t4d Int) - (t5p Int) (t5n Int) (t5s Int) (t5c Int) (t5d Int) - (t6p Int) (t6n Int) (t6s Int) (t6c Int) (t6d Int) -) -:formula -(and - (>= t1p 0) (>= t1n 0) (>= t1s 0) (>= t1c 0) (>= t1d 0) - (>= t2p 0) (>= t2n 0) (>= t2s 0) (>= t2c 0) (>= t2d 0) - (>= t3p 0) (>= t3n 0) (>= t3s 0) (>= t3c 0) (>= t3d 0) - (>= t4p 0) (>= t4n 0) (>= t4s 0) (>= t4c 0) (>= t4d 0) - (>= t5p 0) (>= t5n 0) (>= t5s 0) (>= t5c 0) (>= t5d 0) - (>= t6p 0) (>= t6n 0) (>= t6s 0) (>= t6c 0) (>= t6d 0) - - (<= (+ t1p t1n t1s t1c t1d) 8) - (<= (+ t2p t2n t2s t2c t2d) 8) - (<= (+ t3p t3n t3s t3c t3d) 8) - (<= (+ t4p t4n t4s t4c t4d) 8) - (<= (+ t5p t5n t5s t5c t5d) 8) - (<= (+ t6p t6n t6s t6c t6d) 8) - - (<= (+ (* t1n 700) (* t1p 800) (* t1s 1000) (* t1c 1500) (* t1d 100)) 7800) - (<= (+ (* t2n 700) (* t2p 800) (* t2s 1000) (* t2c 1500) (* t2d 100)) 7800) - (<= (+ (* t3n 700) (* t3p 800) (* t3s 1000) (* t3c 1500) (* t3d 100)) 7800) - (<= (+ (* t4n 700) (* t4p 800) (* t4s 1000) (* t4c 1500) (* t4d 100)) 7800) - (<= (+ (* t5n 700) (* t5p 800) (* t5s 1000) (* t5c 1500) (* t5d 100)) 7800) - (<= (+ (* t6n 700) (* t6p 800) (* t6s 1000) (* t6c 1600) (* t6d 100)) 7800) - - (or (= 0 t1p) (= 0 t1c)) - (or (= 0 t2p) (= 0 t2c)) - (or (= 0 t3p) (= 0 t3c)) - (or (= 0 t4p) (= 0 t4c)) - (or (= 0 t5p) (= 0 t5c)) - (or (= 0 t6p) (= 0 t6c)) - - (<= t1d 1) - (<= t2d 1) - (<= t3d 1) - (<= t4d 1) - (<= t5d 1) - (<= t6d 1) - - (= t3s 0) - (= t4s 0) - (= t5s 0) - (= t6s 0) - - (= (+ t1n t2n t3n t4n t5n t6n) 4) - (= (+ t1s t2s t3s t4s t5s t6s) 8) - (= (+ t1c t2c t3c t4c t5c t6c) 10) - (= (+ t1d t2d t3d t4d t5d t6d) 5) - - (>= (+ t1p t2p t3p t4p t5p t6p) ) -) -) -- 2.20.1