Bug 453701 - Review Request: minisat2 - A minimalistic, open-source SAT solver
Summary: Review Request: minisat2 - A minimalistic, open-source SAT solver
Keywords:
Status: CLOSED NEXTRELEASE
Alias: None
Product: Fedora
Classification: Fedora
Component: Package Review
Version: rawhide
Hardware: All
OS: Linux
medium
medium
Target Milestone: ---
Assignee: Jason Tibbitts
QA Contact: Fedora Extras Quality Assurance
URL:
Whiteboard:
Depends On:
Blocks:
TreeView+ depends on / blocked
 
Reported: 2008-07-02 04:18 UTC by David A. Wheeler
Modified: 2008-09-10 07:07 UTC (History)
3 users (show)

Fixed In Version:
Doc Type: Bug Fix
Doc Text:
Clone Of:
Environment:
Last Closed: 2008-09-05 12:19:02 UTC
Type: ---
Embargoed:
j: fedora-review+
kevin: fedora-cvs+


Attachments (Terms of Use)

Description David A. Wheeler 2008-07-02 04:18:28 UTC
Spec URL: http://www.dwheeler.com/minisat2.spec
SRPM URL: http://www.dwheeler.com/minisat2-070721-3.fc9.src.rpm
Description:
MiniSat is a minimalistic, open-source Boolean satisfiability problem
(SAT) solver, developed for researchers and developers alike.
Winning all the industrial categories of the SAT 2005 competition,
MiniSat is a good starting point both for future research in SAT, and
for applications using SAT.

A SAT solver can determine if it is possible to find assignments to boolean
variables that would make a given expression true, if the expression is
written with only AND, OR, NOT, parentheses, and boolean variables.
If the expression is satisfiable, MiniSAT can also produce a
set of assignments that make the expression true.
Although the problem is NP-complete, SAT solvers (like this one)
are often able to decide this problem in a reasonable time frame.



================================================

* CLean rpmlint (.spec/.rpm/.src.rpm)
* Clean koji build for all f9 archs
* Open source software license (MIT)
* Meets all guidelines (to the best of my knowledge)

They used to use x.y versioning, but now seem to emphasize dates;
have posted a question about version numbering to the packaging list.

The package is named "minisat2" in part because that is its name in Debian
(consistency seemed like a good idea).

The program doesn't come with any (useful) documentation, so I wrote
documentation, which is posted on the web and included in the package.

The program didn't come with any tests, so I created a simple "smoke test",
which is included in %check.

Comment 1 Jason Tibbitts 2008-07-04 19:03:09 UTC
This looks mostly good to me.  It's unfortunate to see that some people seem to
have forgotten what happened a little under nine years ago and have fallen back
to using two-digit years, but that's not up to you.

I think the package in Debian is named minisat2 because that's actually the name
of the software according to upstream, and of course that's the best name to use.

Please consistently use the macro-ized forms; either use things like "cp -p" or
use "%{cp_p}" but don't use both.  (You have two macro forms in %install.) 
Personally I don't see the point in the extra typing that comes with the macros,
but it's your choice; you just need to be consistent.

Please add comments on the upstream status of the included patches. 
http://fedoraproject.org/wiki/Packaging/PatchUpstreamStatus

Nice touch providing documentation, although it would be good if that was sent
upstream as well.

It's interesting that a few source files aren't in the debuginfo package; it
looks like they're just dead code (e.g. BasicHeap.h isn't referenced anywhere).

* source files match upstream:
  ddc2ed421a538a349ddab58d3958076d73813925ff08361e6292583d3b87248e  
   minisat2-070721.zip
  c02847f5dedcf757917a8dd321a8314d1d21268f54823e17ef392311d539afe1  
   minisat-user-guide-1.0.html
* package meets naming and versioning guidelines.
* specfile is properly named and is cleanly written.
X specfile does not use macros consistently.
* summary is OK.
* description is OK.
* dist tag is present.
* build root is OK.
* license field matches the actual license.
* license is open source-compatible.
* license text included in package.
* latest version is being packaged.
* BuildRequires are proper.
* compiler flags are appropriate.
* %clean is present.
* package builds in mock (rawhide, x86_64).
* package installs properly.
* debuginfo package looks complete.
* rpmlint is silent.
* final provides and requires are sane:
   minisat2 = 070721-3.fc10
  =
   libgcc_s.so.1()(64bit)
   libgcc_s.so.1(GCC_3.0)(64bit)
   libstdc++.so.6()(64bit)
   libstdc++.so.6(CXXABI_1.3)(64bit)
   libz.so.1()(64bit)

* %check is present and all tests pass.
* no shared libraries are added to the regular linker search paths.
* owns the directories it creates.
* doesn't own any directories it shouldn't.
* no duplicates in %files.
* file permissions are appropriate.
* no scriptlets present.
* code, not content.
* documentation is small, so no -doc subpackage is necessary.
* %docs are not necessary for the proper functioning of the package.
* no headers.
* no pkgconfig files.
* no static libraries.
* no libtool .la files.

Comment 2 David A. Wheeler 2008-07-05 02:29:27 UTC
Thanks SO MUCH for reviewing the package! I'll fix the "specfile does not use
macros consistently" issue. (Thanks, I hadn't noticed that.)  I'll just switch
to normal commands and not macros for them.

I'm not fond of upstream's version system either.  If you're going to use a
date, use YYYYMMDD!  I'm thinking of changing the version field to "2.0" and
placing the date in the release value instead (treating it as if it were an
"interim" release): 0.1.YYYYMMDD or some such.  That way, if they switch back to
a more traditional version numbering system, no epoch will be needed.  Sound
reasonable?

> Nice touch providing documentation, although it would be good if that was sent
upstream as well.

Thanks!  I agree with getting the docs upstream, that was my plan anyway. (I'm
treating the added documentation as a patch.)  It's ridiculous to create a
program with NO documentation of any kind, yet this sure isn't the only one :-(.



Comment 3 David A. Wheeler 2008-07-09 01:43:39 UTC
Ok, I'm back from vacation. Here's the revised spec/SRPM that addresses
everything I know of:
http://www.dwheeler.com/minisat2.spec
http://www.dwheeler.com//minisat2-2.0-4.20070721.fc9.src.rpm

This version:
- Addresses comment 1 "Please consistently use the macro-ized forms"
- Changes the version/release numbering convention to match Fedora
NamingGuidelines even more precisely.
- Documents when patches/documentation was sent upstream
  (I sent the documentation earlier; I've sent everything today via email
  to Niklas Sorensson.  Niklas is interested in including the docs in
  an upcoming version.)

rpmlint reports no errors or warnings on .spec, SRPM, and generated binary rpm.

It builds for both dist-f9 and dist-f10 on all architectures (via koji).



Comment 4 David A. Wheeler 2008-07-16 03:17:16 UTC
I've talked with upstream; I think I've convinced them to switch to a sensible
"2.1"-style version naming convention for their next release.  If they do so,
this package can be easily updated to match.  

Please review this new version, and let me know if it's approved.  Thanks.


Comment 5 David A. Wheeler 2008-07-20 03:12:10 UTC
I've made a small tweak, and uploaded a new release:
 http://www.dwheeler.com/minisat2-2.0-5.20070721.fc9.src.rpm
 http://www.dwheeler.com/minisat2.spec

This release adds use of the "-O3" optimization flag, to get more
speed out of it. This program is often compiled with -O3,
and speed is absolutely critical to it.

I believe this package is ready:
* All issues raised above have been resolved.
* rpmlint 100% clean on spec, SRPM, and a binary RPM (i386/f9)
* koji scratch build are 100% successful on dist-f8, dist-f9, and dist-f10.

So, any additional comments or approval?


Comment 6 Jason Tibbitts 2008-07-20 14:52:57 UTC
Unfortunately at the moment I'm on vacation up near the arctic circle in Norway
and have only limited access to the Internet and hence my build systems.  It's
not realy possible to do package reviews with only web access but if I have a
slack day when I can get my laptop in range of some wireless network then I'll
try to finish this up.

Comment 7 David A. Wheeler 2008-07-29 22:33:56 UTC
FYI, my miniSAT2 documentation is also available on the web, here:
 http://www.dwheeler.com/essays/minisat-user-guide.html
It's included in my package, because without at least some documentation
on its input, there's no way to USE this tool.  My documentation is released
to the public domain (see the bottom), so there's no license issue.

I've already offered up my documentation to the Debian packager of
miniSAT, which unsurprisingly has lousy documentation.  Thread here:
http://groups.google.com/group/minisat/browse_thread/thread/4680c4579611d714

As I noted earlier, I've already sent the patches and the new documentation to
upstream, and have hopes that upstream will eventually incorporate them.

Note: Novell/SuSE has changed their package manager to use a SAT solver
to speed up dependency analysis (to speed up installation). Presentation here:
http://en.opensuse.org/Libzypp/Sat_Solver
I do _not_ know which SAT solver SuSE uses; miniSAT is a possibility.



Comment 8 David A. Wheeler 2008-08-07 18:57:52 UTC
Hi - any chance you (or someone else) could look over
this proposed package?

This is now a blocker for this proposed Fedora 10 feature:
https://fedoraproject.org/wiki/Features/Provers

Comment 9 Jason Tibbitts 2008-08-07 19:12:11 UTC
I'm back in the country now (although badly jetlagged); I will try to get this finished up this evening.

Comment 10 Jason Tibbitts 2008-08-08 00:23:29 UTC
Everything looks fine to me except the -O3 ricing.  I have no specific problems with this if you have some results which actually indicate a performance improvement, but if you're just assuming that it must somehow be faster because the number is bigger then you really should just use the default flags.

Can you provide some evidence that this makes a difference?

Comment 11 David A. Wheeler 2008-08-08 00:45:56 UTC
The -O3 option is the _normal_ optimization level for MiniSAT.  If you look at their makefile, you'll see that upstream adds -O3 when THEY do a release version ("make release").

So, I'm really just being consistent with upstream, and I think that's a reasonable reason.

I could develop some test suites to do timing tests, but is that necessary if it's just being consistent with upstream?

Comment 12 Rahul Sundaram 2008-08-08 01:17:23 UTC
Just a quick note that the SAT resolver used by SUSE for their new package management system - zypper is available for review at 

https://bugzilla.redhat.com/show_bug.cgi?id=442714

Comment 13 David A. Wheeler 2008-08-08 01:45:25 UTC
I went and got some numbers, and -O3 is a waste of time.  I'll need to tell upstream that.  I created a test sample, and got these:

With -O3:
real    0m35.714s
real    0m35.714s
real    0m35.834s

With -O2:
real    0m35.296s
real    0m35.301s

So -O3 will be dumped.

Comment 14 David A. Wheeler 2008-08-08 01:54:26 UTC
Okay, new miniSAT2 uploaded:
 http://www.dwheeler.com/minisat2.spec
 http://www.dwheeler.com/minisat2-2.0-6.20070721.fc9.src.rpm

This one leaves -O2, as it was.  I left in the (tricky) lines that switch optimization level, in case it actually helps in a future version of gcc.

Comment 15 David A. Wheeler 2008-08-08 02:08:40 UTC
I should add that my -O2 vs. -O3 numbers were for 32-bit i386.  Your mileage may vary.  Indeed, it almost CERTAINLY will vary :-). 2-CPU, where for each:

vendor_id	: GenuineIntel
cpu family	: 15
model		: 6
model name	: Intel(R) Pentium(R) D CPU 3.60GHz
stepping	: 4
cpu MHz		: 3591.136
cache size	: 2048 KB
...
bogomips	: 7187.56

Comment 16 Jason Tibbitts 2008-08-08 16:22:14 UTC
Thanks for doing that.  We rarely see any measurable improvement with -O3 so it's always viewed with some skepticism.  That doesn't mean that you can't turn it on in the future if you find that it actually makes a difference, but in that case you should docuemnt the performance issues in the specfile and be prepared to re-evaluate as the compiler evolves.

Anyway, things look good to me now; sorry that my vacation slowed things down.

APPROVED

Comment 17 David A. Wheeler 2008-08-08 20:47:16 UTC
New Package CVS Request
=======================
Package Name: minisat2
Short Description:  A minimalistic, open-source SAT solver
Owners: dwheeler
Branches: F-8 F-9
InitialCC: tibbs
Cvsextras Commits: yes

Comment 18 Jason Tibbitts 2008-08-08 21:31:49 UTC
Please do not include me in the InitialCC for this package.  I review far too many packages to be CC'd on all of them.

Also, one comment I might add is that there's no need to play any games with "newoptflags" because you're not changing anything.  You might as well just remove, or at least comment out, that portion of the spec.

Comment 19 Kevin Fenzi 2008-08-10 01:35:05 UTC
cvs done.

Comment 20 Fedora Update System 2008-08-14 04:55:35 UTC
minisat2-2.0-7.20070721.fc9 has been submitted as an update for Fedora 9.
/updates/minisat2-2.0-7.20070721.fc9

Comment 21 Fedora Update System 2008-09-05 12:18:57 UTC
minisat2-2.0-7.20070721.fc9 has been pushed to the Fedora 9 stable repository.  If problems still persist, please make note of it in this bug report.

Comment 22 Fedora Update System 2008-09-10 07:07:55 UTC
minisat2-2.0-7.20070721.fc9 has been pushed to the Fedora 9 stable repository.  If problems still persist, please make note of it in this bug report.


Note You need to log in before you can comment on or make changes to this bug.