Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[Hans Petter Selasky]

On 12/06/16 11:04, Hans Petter Selasky wrote:

On 11/24/16 14:11, Vsevolod Stakhov wrote:


Then I don't understand how your patch should affect the solving
procedure. If pkg tries to reinstall something without *reason* it is a
good sign of bug in pkg itself and/or your database/repo and not in SAT
solver.

I'll try to review your issue but I'll likely need your local packages
database for this test.


Hi Vsevolod,

Did you have a chance to look at this?



Ping.

--HPS

___
freebsd-current@freebsd.org mailing list
https://lists.freebsd.org/mailman/listinfo/freebsd-current
To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"

Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[Hans Petter Selasky]

On 11/24/16 14:11, Vsevolod Stakhov wrote:


Then I don't understand how your patch should affect the solving
procedure. If pkg tries to reinstall something without *reason* it is a
good sign of bug in pkg itself and/or your database/repo and not in SAT
solver.

I'll try to review your issue but I'll likely need your local packages
database for this test.


Hi Vsevolod,

Did you have a chance to look at this?

--HPS
___
freebsd-current@freebsd.org mailing list
https://lists.freebsd.org/mailman/listinfo/freebsd-current
To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"

Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[David Chisnall]

On 23 Nov 2016, at 18:11, A. Wilcox  wrote:
> 
> Or you could just, I don't know, email the diff as a patch using git
> send-email like normal people instead of using GitHub's walled garden.
> That way, people without GitHub accounts can still comment on it.

GitHub pull requests are branches in the recipient’s git repo.  Anyone can see 
the patch without logging in, either via the web interface or by pulling the 
relevant branch.  If you want to send comments via email based on this copy of 
the patch, then that’s up to you, though personally I’d much prefer the GitHub 
code review interface to anything email based.

David



smime.p7s
Description: S/MIME cryptographic signature

Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[A. Wilcox]

On 23/11/16 10:47, Ed Schouten wrote:
> 2016-11-23 17:41 GMT+01:00 Hans Petter Selasky :
>> GitHub wouldn't allow me to make a .diff attachment.
> 
> But there's absolutely no need for doing that in the first place! :-)
> 
> 1. Go to https://github.com/freebsd/pkg
> 2. Click 'Fork' on the top right. This will probably create a
> https://github.com/hselasky/pkg
> 3. Check out that repository using git(1), create a separate branch
> and commit the changes to the SAT solver.
> 4. Go to https://github.com/hselasky/pkg and click on 'New pull request'.
> 5. Fill in the form.
> 

Or you could just, I don't know, email the diff as a patch using git
send-email like normal people instead of using GitHub's walled garden.
That way, people without GitHub accounts can still comment on it.

Just my 2¢.

--arw
-- 
A. Wilcox (awilfox)
Open-source programmer (C, C++, Python)
https://code.foxkit.us/u/awilfox/



signature.asc
Description: OpenPGP digital signature

Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[Ed Schouten]

2016-11-24 13:13 GMT+01:00 Vsevolod Stakhov :
> 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.

Exactly. This is why I've stated: it affects performance linearly.
Referring to Wikipedia's pseudo-code of the algorithm: the number of
calls to unit-propagate() and pure-literal-assign() drops linearly,
but the recursion will stay the same.

-- 
Ed Schouten 
Nuxi, 's-Hertogenbosch, the Netherlands
KvK-nr.: 62051717
___
freebsd-current@freebsd.org mailing list
https://lists.freebsd.org/mailman/listinfo/freebsd-current
To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"

Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[Hans Petter Selasky]

On 11/24/16 14:11, Vsevolod Stakhov wrote:

On 24/11/2016 13:05, Hans Petter Selasky wrote:

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 :

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



Then I don't understand how your patch should affect the solving
procedure. If pkg tries to reinstall something without *reason* it is a
good sign of bug in pkg itself and/or your database/repo and not in SAT
solver.

I'll try to review your issue but I'll likely need your local packages
database for this test.



Hi,

Maybe it is a bug somewhere.

I noticed some rules repeating the same variable two times for example.

Send me the list of files you need off-list.

Thank you!

--HPS
___
freebsd-current@freebsd.org mailing list
https://lists.freebsd.org/mailman/listinfo/freebsd-current
To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"

Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[Hans Petter Selasky]

On 11/24/16 14:05, Hans Petter Selasky wrote:

the non-patched version wants to reinstall 1 package.


Spelling: patched version wants to reinstall 1 package only.

--HPS
___
freebsd-current@freebsd.org mailing list
https://lists.freebsd.org/mailman/listinfo/freebsd-current
To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"

Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[Vsevolod Stakhov]

On 24/11/2016 13:05, Hans Petter Selasky wrote:
> 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 :
 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
> 

Then I don't understand how your patch should affect the solving
procedure. If pkg tries to reinstall something without *reason* it is a
good sign of bug in pkg itself and/or your database/repo and not in SAT
solver.

I'll try to review your issue but I'll likely need your local packages
database for this test.

-- 
Vsevolod Stakhov
___
freebsd-current@freebsd.org mailing list
https://lists.freebsd.org/mailman/listinfo/freebsd-current
To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"

Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[Hans Petter Selasky]

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 :

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
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]: 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
  

Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[Vsevolod Stakhov]

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
___
freebsd-current@freebsd.org mailing list
https://lists.freebsd.org/mailman/listinfo/freebsd-current
To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"

Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[Konstantin Tokarev]

23.11.2016, 19:42, "Hans Petter Selasky" :
> On 11/23/16 17: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?
>
> Hi Ed,
>
> I tried measuring with "time", but figured out that it was doing a lot
> of other stuff too. Isolating this piece of code was not so easy.
>
>  > 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?
>>
>>  By the way, why attach a zip file with a diff? GitHub's pull requests
>>  are awesome! :-)
>
> GitHub wouldn't allow me to make a .diff attachment.

If you really want to be nasty and not submit your change as a pull request,
GitHub allows you to paste your patch as a comment:

```diff

```


>
>>  [1] Davis-Putnam-Logemann-Loveland algorithm:
>>  https://en.wikipedia.org/wiki/DPLL_algorithm
>
> --HPS
> ___
> freebsd-po...@freebsd.org mailing list
> https://lists.freebsd.org/mailman/listinfo/freebsd-ports
> To unsubscribe, send any mail to "freebsd-ports-unsubscr...@freebsd.org"

-- 
Regards,
Konstantin
___
freebsd-current@freebsd.org mailing list
https://lists.freebsd.org/mailman/listinfo/freebsd-current
To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"

Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[Ed Schouten]

2016-11-23 17:41 GMT+01:00 Hans Petter Selasky :
> GitHub wouldn't allow me to make a .diff attachment.

But there's absolutely no need for doing that in the first place! :-)

1. Go to https://github.com/freebsd/pkg
2. Click 'Fork' on the top right. This will probably create a
https://github.com/hselasky/pkg
3. Check out that repository using git(1), create a separate branch
and commit the changes to the SAT solver.
4. Go to https://github.com/hselasky/pkg and click on 'New pull request'.
5. Fill in the form.

-- 
Ed Schouten 
Nuxi, 's-Hertogenbosch, the Netherlands
KvK-nr.: 62051717
___
freebsd-current@freebsd.org mailing list
https://lists.freebsd.org/mailman/listinfo/freebsd-current
To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"

Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[Hans Petter Selasky]

On 11/23/16 17: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?


Hi Ed,

I tried measuring with "time", but figured out that it was doing a lot 
of other stuff too. Isolating this piece of code was not so easy.


> 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?

By the way, why attach a zip file with a diff? GitHub's pull requests
are awesome! :-)


GitHub wouldn't allow me to make a .diff attachment.



[1] Davis-Putnam-Logemann-Loveland algorithm:
https://en.wikipedia.org/wiki/DPLL_algorithm



--HPS
___
freebsd-current@freebsd.org mailing list
https://lists.freebsd.org/mailman/listinfo/freebsd-current
To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"

Re: Optimising generated rules for SAT solving (5/12 are duplicates)

[Ed Schouten]

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?

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

-- 
Ed Schouten 
Nuxi, 's-Hertogenbosch, the Netherlands
KvK-nr.: 62051717
___
freebsd-current@freebsd.org mailing list
https://lists.freebsd.org/mailman/listinfo/freebsd-current
To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"