From owner-freebsd-ports@freebsd.org Thu Nov 24 12:13:52 2016 Return-Path: Delivered-To: freebsd-ports@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id E8028C53F9F for ; Thu, 24 Nov 2016 12:13:52 +0000 (UTC) (envelope-from vsevolod@highsecure.ru) Received: from mailman.ysv.freebsd.org (unknown [127.0.1.3]) by mx1.freebsd.org (Postfix) with ESMTP id CB75B19C for ; Thu, 24 Nov 2016 12:13:52 +0000 (UTC) (envelope-from vsevolod@highsecure.ru) Received: by mailman.ysv.freebsd.org (Postfix) id CAE4EC53F9D; Thu, 24 Nov 2016 12:13:52 +0000 (UTC) Delivered-To: ports@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id CA726C53F9C; Thu, 24 Nov 2016 12:13:52 +0000 (UTC) (envelope-from vsevolod@highsecure.ru) Received: from mail.highsecure.ru (mail6.highsecure.ru [IPv6:2a01:4f8:190:43b5::99]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mx1.freebsd.org (Postfix) with ESMTPS id 8853E19B; Thu, 24 Nov 2016 12:13:52 +0000 (UTC) (envelope-from vsevolod@highsecure.ru) Received: from secret-bunker.localdomain (unknown [81.145.134.172]) (using TLSv1.2 with cipher AECDH-AES256-SHA (256/256 bits)) (No client certificate requested) (Authenticated sender: vsevolod@highsecure.ru) by mail.highsecure.ru (Postfix) with ESMTPSA id 300A2300A6E; Thu, 24 Nov 2016 13:13:40 +0100 (CET) Received: from [127.0.0.1] (localhost [127.0.0.1]) by secret-bunker.localdomain (Postfix) with ESMTP id A4A1B2D11F5A; Thu, 24 Nov 2016 12:13:39 +0000 (GMT) Subject: Re: Optimising generated rules for SAT solving (5/12 are duplicates) To: Ed Schouten , Hans Petter Selasky 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> Cc: Baptiste Daroussin , Slawa Olhovchenkov , ports@freebsd.org, FreeBSD Current From: Vsevolod Stakhov Message-ID: Date: Thu, 24 Nov 2016 12:13:39 +0000 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.11; rv:45.0) Gecko/20100101 Thunderbird/45.5.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 7bit DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=highsecure.ru; s=dkim; t=1479989621; bh=IxRdE/0FY7Fb0Jn5PUPm/AeIZq5adcAa1pj/EIve62A=; h=Subject:To:References:Cc:From:Message-ID:Date:MIME-Version:In-Reply-To:Content-Type:Content-Transfer-Encoding; b=j05lhEUOI72/Ai643oIq7IaeaP+5r3mukm7REIajYukLuZe87YXg30jxbb6P5wyM3SnoZJuwlkIU+kMGHBjbT0JvENtGF8kwzlfqSWbaDz13yKqAZn0W5L0DOVx0+x8l4ZAVPLeD7S6DUvV0WmqpdtSnjUVrgSFTPeqNRBY2UDY= X-BeenThere: freebsd-ports@freebsd.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: Porting software to FreeBSD List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 24 Nov 2016 12:13:53 -0000 On 23/11/2016 16:27, Ed Schouten wrote: > Hi Hans, > > 2016-11-23 15:27 GMT+01:00 Hans Petter Selasky : >> 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. > By the way, why attach a zip file with a diff? GitHub's pull requests > are awesome! :-) > > [1] Davis-Putnam-Logemann-Loveland algorithm: > https://en.wikipedia.org/wiki/DPLL_algorithm > -- Vsevolod Stakhov