Skip site navigation (1)Skip section navigation (2)
Date:      Thu, 24 Nov 2016 14:05:18 +0100
From:      Hans Petter Selasky <hps@selasky.org>
To:        Vsevolod Stakhov <vsevolod@highsecure.ru>, Ed Schouten <ed@nuxi.nl>
Cc:        Baptiste Daroussin <bapt@freebsd.org>, Slawa Olhovchenkov <slw@zxy.spb.ru>, ports@freebsd.org, FreeBSD Current <freebsd-current@freebsd.org>
Subject:   Re: Optimising generated rules for SAT solving (5/12 are duplicates)
Message-ID:  <9b0469bb-ab2b-4992-1d40-de748163f2c8@selasky.org>
In-Reply-To: <d786cde5-89af-cb14-c42e-cc649cb32bdb@highsecure.ru>
References:  <20150414200459.GE39658@ivaldir.etoilebsd.net> <20150421103454.GR1394@zxy.spb.ru> <5593D0AE.2010205@selasky.org> <416359ce-1dcd-1160-5c56-f120a0f6358f@selasky.org> <20160627115533.gqvdsmtzwnvrrfuo@ivaldir.etoilebsd.net> <0671148b-d7cd-f8ad-906d-a0baa1b98cf5@selasky.org> <cbc964a7-5f90-6ea1-630d-414de68867b1@selasky.org> <CABh_MKm7LAtQzp9KEBpaRZWQQHnsUtNFiKVSVF70-wj4GmytuA@mail.gmail.com> <d786cde5-89af-cb14-c42e-cc649cb32bdb@highsecure.ru>

next in thread | previous in thread | raw e-mail | index | archive | help
This is a multi-part message in MIME format.
--------------6177813FFD2C97BC114024A6
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit

On 11/24/16 13:13, Vsevolod Stakhov wrote:
> On 23/11/2016 16:27, Ed Schouten wrote:
>> Hi Hans,
>>
>> 2016-11-23 15:27 GMT+01:00 Hans Petter Selasky <hps@selasky.org>:
>>> I've made a patch to hopefully optimise SAT solving in our pkg utility.
>>
>> Nice! Do you by any chance have any numbers that show the performance
>> improvements made by this change? Assuming that the SAT solver of
>> pkg(1) uses an algorithm similar to DPLL[1], a change like this would
>> affect performance linearly. My guess is therefore that the running
>> time is reduced by approximately 5/12. Is this correct?
>
> There won't be any improvement if you just remove duplicates from SAT
> formula. This situation is handled by picosat internally and even for
> naive DPLL there is no significant influence of duplicate KNF clauses:
> once you've assumed all vars in some clause, you automatically resolve
> all duplicates.
>
> Is there any real improvement of SAT solver speed with this patch? From
> my experiences, SAT solving is negligible in terms of CPU time comparing
> to other tasks performed by pkg.

Hi,

I added some code to measure the time for SAT solving. During my test 
run I'm seeing values in the range 8-10ms for both versions, so I 
consider that neglible. However, the unpatched version wants to 
reinstall 185 packages while the non-patched version wants to reinstall 
1 package. That has a huge time influential. I'm not that familar with 
PKG that I can draw any conclusions from this.

# Test1:
echo "n" | /xxx/pkg/src/pkg-static upgrade --no-repo-update > b.txt

# Test2:
echo "n" | env PKG_NO_SORT=YES /xxx/pkg/src/pkg-static upgrade 
--no-repo-update > a.txt

Please find the material attached including a debug version patch you 
can play with.

--HPS

--------------6177813FFD2C97BC114024A6
Content-Type: text/plain; charset=UTF-8;
 name="b.txt"
Content-Transfer-Encoding: 7bit
Content-Disposition: attachment;
 filename="b.txt"

Checking for upgrades (748 candidates): .......... done
Processing candidates (748 candidates): . done
Skipped 3702 identical rules
Reiterate
SAT solving took 0s and 7370 usecs
The following 52 package(s) will be affected (of 0 checked):

Installed packages to be UPGRADED:
	xapian-core: 1.2.23,1 -> 1.2.24,1
	webp: 0.5.0 -> 0.5.1_1
	webkit2-gtk3: 2.8.5_6 -> 2.8.5_7
	webkit-gtk2: 2.4.11_4 -> 2.4.11_5
	vlc: 2.2.4_3,4 -> 2.2.4_4,4
	trousers: 0.3.13_1 -> 0.3.14
	tiff: 4.0.6_2 -> 4.0.7
	thunderbird: 45.4.0_2 -> 45.5.0_1
	sqlite3: 3.15.1 -> 3.15.1_1
	spidermonkey170: 17.0.0_2 -> 17.0.0_3
	soundtouch: 1.9.2 -> 1.9.2_1
	raptor2: 2.0.15_4 -> 2.0.15_5
	qt5-core: 5.6.2 -> 5.6.2_1
	qt4-corelib: 4.8.7_5 -> 4.8.7_6
	polkit: 0.113_1 -> 0.113_2
	pciids: 20161029 -> 20161119
	openimageio: 1.6.12_2 -> 1.6.12_3
	openblas: 0.2.18_1,1 -> 0.2.18_2,1
	openal-soft: 1.17.2 -> 1.17.2_1
	libx264: 0.148.2708 -> 0.148.2708_1
	libvpx: 1.6.0 -> 1.6.0_1
	libvisio01: 0.1.5_3 -> 0.1.5_4
	libreoffice: 5.2.3_2 -> 5.2.3_3
	libpci: 3.5.1 -> 3.5.2
	libmspub01: 0.1.2_4 -> 0.1.2_5
	libfreehand: 0.1.1_3 -> 0.1.1_4
	libe-book: 0.1.2_5 -> 0.1.2_6
	libcdr01: 0.1.3_1 -> 0.1.3_2
	lcms2: 2.7_2 -> 2.8
	inkscape: 0.91_8 -> 0.91_9
	icu: 57.1,1 -> 58.1,1
	harfbuzz: 1.3.3 -> 1.3.3_1
	gstreamer1-plugins: 1.8.0 -> 1.8.0_1
	gstreamer-plugins: 0.10.36_6,3 -> 0.10.36_7,3
	gstreamer: 0.10.36_4 -> 0.10.36_5
	gnupg: 2.1.15 -> 2.1.16
	glib: 2.46.2_3 -> 2.46.2_4
	gcc: 4.8.5_2 -> 4.9.4
	firefox: 50.0_2,1 -> 50.0_4,1
	firebird25-client: 2.5.6_1 -> 2.5.6_2
	ffmpeg: 2.8.8_5,1 -> 2.8.8_8,1
	dejavu: 2.35 -> 2.37
	chromium: 52.0.2743.116_2 -> 52.0.2743.116_4
	boost-libs: 1.55.0_13 -> 1.55.0_14
	blender: 2.77a -> 2.77a_1
	belle-sip: 1.5.0 -> 1.5.0_1
	bash: 4.4 -> 4.4.5
	argyllcms: 1.7.0_1 -> 1.7.0_2
	OpenEXR: 2.2.0_5 -> 2.2.0_6
	ImageMagick: 6.9.5.10,1 -> 6.9.5.10_1,1
	GraphicsMagick: 1.3.24,1 -> 1.3.24_1,1

Installed packages to be REINSTALLED:
	baresip-0.4.19 (options changed)

Number of packages to be upgraded: 51
Number of packages to be reinstalled: 1

The process will require 19 MiB more space.
446 MiB to be downloaded.

Proceed with this action? [y/N]: 
--------------6177813FFD2C97BC114024A6
Content-Type: text/plain; charset=UTF-8;
 name="a.txt"
Content-Transfer-Encoding: 7bit
Content-Disposition: attachment;
 filename="a.txt"

Checking for upgrades (748 candidates): .......... done
Processing candidates (748 candidates): . done
Reiterate
SAT solving took 0s and 5790 usecs
The following 236 package(s) will be affected (of 0 checked):

Installed packages to be UPGRADED:
	xapian-core: 1.2.23,1 -> 1.2.24,1
	webp: 0.5.0 -> 0.5.1_1
	webkit2-gtk3: 2.8.5_6 -> 2.8.5_7
	webkit-gtk2: 2.4.11_4 -> 2.4.11_5
	vlc: 2.2.4_3,4 -> 2.2.4_4,4
	trousers: 0.3.13_1 -> 0.3.14
	tiff: 4.0.6_2 -> 4.0.7
	thunderbird: 45.4.0_2 -> 45.5.0_1
	sqlite3: 3.15.1 -> 3.15.1_1
	spidermonkey170: 17.0.0_2 -> 17.0.0_3
	soundtouch: 1.9.2 -> 1.9.2_1
	raptor2: 2.0.15_4 -> 2.0.15_5
	qt5-core: 5.6.2 -> 5.6.2_1
	qt4-corelib: 4.8.7_5 -> 4.8.7_6
	polkit: 0.113_1 -> 0.113_2
	pciids: 20161029 -> 20161119
	openimageio: 1.6.12_2 -> 1.6.12_3
	openblas: 0.2.18_1,1 -> 0.2.18_2,1
	openal-soft: 1.17.2 -> 1.17.2_1
	libx264: 0.148.2708 -> 0.148.2708_1
	libvpx: 1.6.0 -> 1.6.0_1
	libvisio01: 0.1.5_3 -> 0.1.5_4
	libreoffice: 5.2.3_2 -> 5.2.3_3
	libpci: 3.5.1 -> 3.5.2
	libmspub01: 0.1.2_4 -> 0.1.2_5
	libfreehand: 0.1.1_3 -> 0.1.1_4
	libe-book: 0.1.2_5 -> 0.1.2_6
	libcdr01: 0.1.3_1 -> 0.1.3_2
	lcms2: 2.7_2 -> 2.8
	inkscape: 0.91_8 -> 0.91_9
	icu: 57.1,1 -> 58.1,1
	harfbuzz: 1.3.3 -> 1.3.3_1
	gstreamer1-plugins: 1.8.0 -> 1.8.0_1
	gstreamer-plugins: 0.10.36_6,3 -> 0.10.36_7,3
	gstreamer: 0.10.36_4 -> 0.10.36_5
	gnupg: 2.1.15 -> 2.1.16
	glib: 2.46.2_3 -> 2.46.2_4
	gcc: 4.8.5_2 -> 4.9.4
	firefox: 50.0_2,1 -> 50.0_4,1
	firebird25-client: 2.5.6_1 -> 2.5.6_2
	ffmpeg: 2.8.8_5,1 -> 2.8.8_8,1
	dejavu: 2.35 -> 2.37
	chromium: 52.0.2743.116_2 -> 52.0.2743.116_4
	boost-libs: 1.55.0_13 -> 1.55.0_14
	blender: 2.77a -> 2.77a_1
	belle-sip: 1.5.0 -> 1.5.0_1
	bash: 4.4 -> 4.4.5
	argyllcms: 1.7.0_1 -> 1.7.0_2
	OpenEXR: 2.2.0_5 -> 2.2.0_6
	ImageMagick: 6.9.5.10,1 -> 6.9.5.10_1,1
	GraphicsMagick: 1.3.24,1 -> 1.3.24_1,1

Installed packages to be REINSTALLED:
	yaml-cpp03-0.3.0
	yajl-2.1.0
	xvid-1.3.4,1
	xcb-util-renderutil-0.3.9_1
	xcb-util-keysyms-0.4.0_1
	xcb-util-0.4.0_1,1
	twolame-0.3.13_4
	tpm-emulator-0.7.4_1
	tinyxml-2.6.2_1
	taglib-1.10
	startup-notification-0.12_4
	speexdsp-1.2.r3_1
	speex-1.2.r2,1
	speech-dispatcher-0.8.3_1
	spandsp-0.0.6
	snappy-1.1.3
	serf-1.3.9_1
	schroedinger-1.0.11_4
	redland-1.0.17_4
	readline-6.3.8
	re2-20151101
	rasqal-0.9.33
	qt5-x11extras-5.6.2
	qt5-widgets-5.6.2
	python35-3.5.2
	python27-2.7.12
	popt-1.16_1
	poppler-glib-0.46.0
	poppler-0.46.0_2
	pixman-0.34.0
	perl5-5.24.1.r4
	pcre-8.39
	pangomm-2.36.0
	pango-1.38.0_1
	p11-kit-0.23.2
	orc-0.4.25
	opus-1.1.3
	opensubdiv-3.0.5_2
	openldap-client-2.4.44
	openjpeg15-1.5.2_1
	openjpeg-2.1.2_1
	opencv2-core-2.4.13.1_1
	opencolorio-1.0.9
	opencollada-1.6.25
	nss-3.27.1_1
	nspr-4.13.1
	npth-1.2
	nettle-3.2
	mythes-1.2.4
	mpfr-3.1.5
	mpc-1.0.3
	lua52-5.2.4
	libxslt-1.1.29
	libxml2-2.9.4
	libxcb-1.12
	libwps-0.4.4
	libwpg03-0.3.1
	libwpd010-0.10.1
	libwmf-0.2.8.4_15
	libvorbis-1.3.5,3
	libvdpau-1.1.1
	libva-1.7.2
	libv4l-1.6.3_2
	libtheora-1.1.1_6
	libtasn1-4.9
	libsoup-2.52.2
	libsndfile-1.0.27
	libsigc++-2.4.1
	libsecret-0.18.4
	libsamplerate-0.1.9
	librsvg2-2.40.16
	librevenge-0.0.4_1
	libpthread-stubs-0.3_6
	libpciaccess-0.13.4
	libpaper-1.1.24.4
	libpagemaker-0.0.3
	libogg-1.3.2_1,4
	libodfgen01-0.1.6
	libmwaw03-0.3.8
	libmpeg2-0.5.1_6
	libmatroska-1.4.5
	libmad-0.15.1b_6
	libltdl-2.4.6
	liblqr-1-0.4.2
	libidn-1.33_1
	libiconv-1.14_9
	libgltf-0.0.2_1
	libglapi-11.2.2
	libgcrypt-1.7.3
	libfpx-1.3.1.4_1
	libffi-3.2.1
	libexttextcat-3.4.4
	libevent2-2.0.22_1
	libetonyek01-0.1.6,1
	libepoxy-1.3.1
	libedit-3.1.20150325_2,1
	libdvdread-5.0.3
	libdvdnav-5.0.3
	libdvbpsi-1.3.0
	libdrm-2.4.66,1
	libdca-0.0.5_1
	libcroco-0.6.11
	libcmis-0.5.1
	libcddb-1.3.2_4
	libassuan-2.4.3
	libantlr3c-3.4_1
	libabw-0.1.1_1
	liba52-0.7.4_3
	libXxf86vm-1.1.4_1
	libXvMC-1.0.10
	libXv-1.0.11,1
	libXtst-1.2.3
	libXt-1.1.5,1
	libXrender-0.9.10
	libXrandr-1.5.1
	libXmu-1.1.2_3,1
	libXinerama-1.1.3_3,1
	libXi-1.7.8,1
	libXft-2.3.2_1
	libXfixes-5.0.3
	libXext-1.3.3_1,1
	libXdmcp-1.1.2
	libXdamage-1.1.4_3
	libXcursor-1.1.14_3
	libXcomposite-0.4.4_3,1
	libXaw-1.0.13,2
	libXau-1.0.8_3
	libXScrnSaver-1.2.2_3
	libX11-1.6.4,1
	libSM-1.2.2_3,1
	libIDL-0.8.14_2
	libICE-1.0.9_1,1
	libGLU-9.0.0_2
	libGL-11.2.2
	libEGL-11.2.2
	jpeg-turbo-1.5.1
	jbigkit-2.1_1
	jasper-1.900.1_16
	ilmbase-2.2.0
	hyphen-2.8.8
	hunspell-1.3.3
	gtkspell-2.0.16_5
	gtkmm24-2.24.4_2
	gtk3-3.18.8_3
	gtk2-2.24.29_2
	gstreamer1-1.8.0
	gsl-1.16_2
	gnutls-3.4.16
	gmp-5.1.3_3
	glibmm-2.44.0,1
	glew-1.13.0
	giflib-5.1.4
	gettext-runtime-0.19.8.1
	gdk-pixbuf2-2.32.3_1
	gconf2-3.2.6_4
	gbm-11.2.2
	freetype2-2.6.3
	fontconfig-2.12.1,1
	flac-1.3.1_2
	fftw3-3.3.5
	faad2-2.7_6,1
	expat-2.2.0
	espeak-1.48.04_1
	enchant-1.6.0_5
	dotconf-1.3_1
	dbus-glib-0.104
	dbus-1.8.20
	db5-5.3.28_6
	curl-7.51.0_1
	cups-2.2.1
	colord-1.2.11_1
	clucene-2.3.3.4_7
	cairomm-1.10.0_3
	cairo-1.14.6_1,2
	boehm-gc-7.6.0
	bctoolbox-0.2.0
	baresip-0.4.19 (options changed)
	avahi-app-0.6.31_5
	atkmm-2.22.7
	atk-2.18.0
	at-spi2-atk-2.18.1
	apr-1.5.2.1.5.4_2
	alsa-lib-1.1.2
	ORBit2-2.14.19_1
	CoinMP-1.8.3

Number of packages to be upgraded: 51
Number of packages to be reinstalled: 185

The process will require 19 MiB more space.
491 MiB to be downloaded.

Proceed with this action? [y/N]: 
--------------6177813FFD2C97BC114024A6
Content-Type: text/x-patch;
 name="0001-Optimise-SAT-solving.patch"
Content-Transfer-Encoding: 7bit
Content-Disposition: attachment;
 filename="0001-Optimise-SAT-solving.patch"

>From 135812278d74a3dd632713885ba47daa05a2b175 Mon Sep 17 00:00:00 2001
From: Hans Petter Selasky <hps@selasky.org>
Date: Thu, 24 Nov 2016 13:35:37 +0100
Subject: [PATCH] Optimise SAT solving.

Signed-off-by: Hans Petter Selasky <hps@selasky.org>
---
 libpkg/pkg_solve.c | 317 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 315 insertions(+), 2 deletions(-)

diff --git a/libpkg/pkg_solve.c b/libpkg/pkg_solve.c
index 9cf08e2..d50281f 100644
--- a/libpkg/pkg_solve.c
+++ b/libpkg/pkg_solve.c
@@ -1074,8 +1074,299 @@ pkg_solve_set_initial_assumption(struct pkg_solve_problem *problem,
 	}
 }
 
-int
-pkg_solve_sat_problem(struct pkg_solve_problem *problem)
+static int
+pkg_solve_item_compare(const void *ppa, const void *ppb)
+{
+	struct pkg_solve_item *ia = *(struct pkg_solve_item **)ppa;
+	struct pkg_solve_item *ib = *(struct pkg_solve_item **)ppb;
+	int va = ia->var->order * ia->inverse;
+	int vb = ib->var->order * ib->inverse;
+
+	if (va > vb)
+		return (1);
+	else if (va < vb)
+		return (-1);
+	return (0);
+}
+
+static int
+pkg_solve_rule_compare(const void *ppa, const void *ppb)
+{
+	struct pkg_solve_rule *ra = *(struct pkg_solve_rule **)ppa;
+	struct pkg_solve_rule *rb = *(struct pkg_solve_rule **)ppb;
+	struct pkg_solve_item *ia;
+	struct pkg_solve_item *ib;
+	size_t na = 0;
+	size_t nb = 0;
+
+	LL_FOREACH(ra->items, ia)
+		na++;
+	LL_FOREACH(rb->items, ib)
+		nb++;
+
+	if (na > nb)
+		return (1);
+	else if (na < nb)
+		return (-1);
+
+	ia = ra->items;
+	ib = rb->items;
+	while (ia != 0 && ib != 0) {
+		int va = ia->var->order * ia->inverse;
+		int vb = ib->var->order * ib->inverse;
+		if (va > vb)
+			return (1);
+		else if (va < vb)
+			return (-1);
+		ia = ia->next;
+		ib = ib->next;
+	}
+	return (0);
+}
+
+static int
+pkg_solve_sat_problem_sub(struct pkg_solve_problem *problem)
+{
+	struct pkg_solve_rule **rule_array;
+	struct pkg_solve_rule *rule;
+	struct pkg_solve_item *item;
+	int res, iter = 0;
+	size_t skipped = 0;
+	size_t i;
+	size_t n;
+	bool need_reiterate = false;
+	const int *failed = NULL;
+	int attempt = 0;
+	struct pkg_solve_variable *var;
+
+	rule_array = (struct pkg_solve_rule **)calloc(kv_size(problem->rules), sizeof(void *));
+	if (rule_array == NULL)
+		return (EPKG_FATAL);
+
+	n = kv_size(problem->rules);
+	for (i = 0; i != n; i++) {
+		size_t j;
+		size_t k;
+
+		rule = kv_A(problem->rules, i);
+		rule_array[i] = rule;
+
+		j = 0;
+		LL_FOREACH(rule->items, item)
+			j++;
+
+		struct pkg_solve_item *item_array[j];
+
+		j = 0;
+		LL_FOREACH(rule->items, item)
+			item_array[j++] = item;
+
+		mergesort(item_array, j, sizeof(void *), pkg_solve_item_compare);
+
+		rule->items = 0;
+		for (k = 0; k != j; k++) {
+			/* if items are identical, skip them */
+			if (k != j - 1 &&
+			    pkg_solve_item_compare(item_array + k, item_array + k + 1) == 0) {
+				free(item_array[k]);
+				continue;
+			}
+			item_array[k]->next = rule->items;
+			rule->items = item_array[k];
+		}
+	}
+
+	mergesort(rule_array, n, sizeof(void *), pkg_solve_rule_compare);
+
+	for (i = 0; i != n; i++) {
+		/* if rules are identical, skip them */
+		if (i != n - 1 &&
+		    pkg_solve_rule_compare(rule_array + i, rule_array + i + 1) == 0) {
+			skipped++;
+			continue;
+		}
+		rule = rule_array[i];
+		LL_FOREACH(rule->items, item) {
+			picosat_add(problem->sat, item->var->order * item->inverse);
+		}
+
+		picosat_add(problem->sat, 0);
+		pkg_debug_print_rule(rule);
+	}
+
+	for (i = 0; i != n; i++) {
+		/* if rules are identical, skip them */
+		if (i != n - 1 &&
+		    pkg_solve_rule_compare(rule_array + i, rule_array + i + 1) == 0)
+			continue;
+		rule = rule_array[i];
+		pkg_solve_set_initial_assumption(problem, rule);
+	}
+
+	free(rule_array);
+
+	pkg_emit_notice("Skipped %lld identical rules", (long long)skipped);
+
+reiterate:
+	pkg_emit_notice("Reiterate");
+
+	res = pkg_solve_picosat_iter(problem, iter);
+
+	if (res != PICOSAT_SATISFIABLE) {
+		/*
+		 * in case we cannot satisfy the problem it appears by
+		 * experience that the culprit seems to always be the latest of
+		 * listed in the failed assumptions.
+		 * So try to remove them for the given problem.
+		 * To avoid endless loop allow a maximum of 10 iterations no
+		 * more
+		 */
+		failed = picosat_failed_assumptions(problem->sat);
+		attempt++;
+
+		/* get the last failure */
+		while (*failed) {
+			failed++;
+		}
+		failed--;
+
+		if (attempt >= 10) {
+			pkg_emit_error("Cannot solve problem using SAT solver");
+			UT_string *sb;
+			utstring_new(sb);
+
+			while (*failed) {
+				var = &problem->variables[abs(*failed) - 1];
+				for (i = 0; i < kv_size(problem->rules); i++) {
+					rule = kv_A(problem->rules, i);
+
+					if (rule->reason != PKG_RULE_DEPEND) {
+						LL_FOREACH(rule->items, item) {
+							if (item->var == var) {
+								pkg_print_rule_buf(rule, sb);
+								utstring_printf(sb, "%c", '\n');
+								break;
+							}
+						}
+					}
+				}
+
+				utstring_printf(sb, "cannot %s package %s, remove it from request? ",
+						var->flags & PKG_VAR_INSTALL ? "install" : "remove", var->uid);
+
+				if (pkg_emit_query_yesno(true, utstring_body(sb))) {
+					var->flags |= PKG_VAR_FAILED;
+				}
+
+				failed++;
+				need_reiterate = true;
+			}
+			utstring_clear(sb);
+		} else {
+			pkg_emit_notice("Cannot solve problem using SAT solver, trying another plan");
+			var = &problem->variables[abs(*failed) - 1];
+
+			var->flags |= PKG_VAR_FAILED;
+
+			need_reiterate = true;
+		}
+
+#if 0
+		failed = picosat_next_maximal_satisfiable_subset_of_assumptions(problem->sat);
+
+		while (*failed) {
+			struct pkg_solve_variable *var = &problem->variables[*failed - 1];
+
+			pkg_emit_notice("var: %s", var->uid);
+
+			failed ++;
+		}
+
+		return (EPKG_AGAIN);
+#endif
+	}
+	else {
+
+		/* Assign vars */
+		for (i = 0; i < problem->nvars; i ++) {
+			int val = picosat_deref(problem->sat, i + 1);
+			struct pkg_solve_variable *var = &problem->variables[i];
+
+			if (val > 0)
+				var->flags |= PKG_VAR_INSTALL;
+			else
+				var->flags &= ~PKG_VAR_INSTALL;
+
+			pkg_debug(2, "decided %s %s-%s to %s",
+					var->unit->pkg->type == PKG_INSTALLED ? "local" : "remote",
+							var->uid, var->digest,
+							var->flags & PKG_VAR_INSTALL ? "install" : "delete");
+		}
+
+		/* Check for reiterations */
+		if ((problem->j->type == PKG_JOBS_INSTALL ||
+				problem->j->type == PKG_JOBS_UPGRADE) && iter == 0) {
+			for (i = 0; i < problem->nvars; i ++) {
+				bool failed_var = false;
+				struct pkg_solve_variable *var = &problem->variables[i], *cur;
+
+				if (!(var->flags & PKG_VAR_INSTALL)) {
+					LL_FOREACH(var, cur) {
+						if (cur->flags & PKG_VAR_INSTALL) {
+							failed_var = false;
+							break;
+						}
+						else if (cur->unit->pkg->type == PKG_INSTALLED) {
+							failed_var = true;
+						}
+					}
+				}
+
+				/*
+				 * If we want to delete local packages on installation, do one more SAT
+				 * iteration to ensure that we have no other choices
+				 */
+				if (failed_var) {
+					pkg_debug (1, "trying to delete local package %s-%s on install/upgrade,"
+							" reiterate on SAT",
+							var->unit->pkg->name, var->unit->pkg->version);
+					need_reiterate = true;
+
+					LL_FOREACH(var, cur) {
+						cur->flags |= PKG_VAR_FAILED;
+					}
+				}
+			}
+		}
+	}
+
+	if (need_reiterate) {
+		iter ++;
+
+		/* Restore top-level assumptions */
+		for (i = 0; i < problem->nvars; i ++) {
+			struct pkg_solve_variable *var = &problem->variables[i];
+
+			if (var->flags & PKG_VAR_TOP) {
+				if (var->flags & PKG_VAR_FAILED) {
+					var->flags ^= PKG_VAR_INSTALL | PKG_VAR_FAILED;
+				}
+
+				picosat_assume(problem->sat, var->order *
+						(var->flags & PKG_VAR_INSTALL ? 1 : -1));
+			}
+		}
+
+		need_reiterate = false;
+
+		goto reiterate;
+	}
+
+	return (EPKG_OK);
+}
+
+static int
+pkg_solve_sat_problem_old(struct pkg_solve_problem *problem)
 {
 	struct pkg_solve_rule *rule;
 	struct pkg_solve_item *item;
@@ -1103,6 +1394,7 @@ pkg_solve_sat_problem(struct pkg_solve_problem *problem)
 	}
 
 reiterate:
+	pkg_emit_notice("Reiterate");
 
 	res = pkg_solve_picosat_iter(problem, iter);
 
@@ -1259,6 +1551,27 @@ reiterate:
 	return (EPKG_OK);
 }
 
+int
+pkg_solve_sat_problem(struct pkg_solve_problem *problem)
+{
+	struct timeval tv0;
+	gettimeofday(&tv0, NULL);
+	int err;
+
+	if (getenv("PKG_NO_SORT") != NULL)
+		err = pkg_solve_sat_problem_old(problem);
+	else
+		err = pkg_solve_sat_problem_sub(problem);
+	struct timeval tv1;
+	gettimeofday(&tv1, NULL);
+
+	timersub(&tv1, &tv0, &tv1);
+
+	pkg_emit_notice("SAT solving took %llds and %lld usecs", (long long)tv1.tv_sec, (long long)tv1.tv_usec);
+
+	return (err);
+}
+
 void
 pkg_solve_dot_export(struct pkg_solve_problem *problem, FILE *file)
 {
-- 
2.10.1


--------------6177813FFD2C97BC114024A6--



Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?9b0469bb-ab2b-4992-1d40-de748163f2c8>