rpms/minisat2/F-8 import.log, NONE, 1.1 minisat-user-guide-1.0.html, NONE, 1.1 minisat2-FPU.patch, NONE, 1.1 minisat2-template.patch, NONE, 1.1 minisat2-test.in, NONE, 1.1 minisat2.spec, NONE, 1.1 .cvsignore, 1.1, 1.2 sources, 1.1, 1.2

Thu Aug 14 04:29:30 UTC 2008

Author: dwheeler

Update of /cvs/pkgs/rpms/minisat2/F-8
In directory cvs-int.fedora.redhat.com:/tmp/cvs-serv25076/F-8

Modified Files:
	.cvsignore sources 
Added Files:
	import.log minisat-user-guide-1.0.html minisat2-FPU.patch 
	minisat2-template.patch minisat2-test.in minisat2.spec 
Log Message:


* Tue Aug 14 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-7.20070721
- Initial submission to repository

--- NEW FILE import.log ---
minisat2-2_0-7_20070721_fc9:F-8:minisat2-2.0-7.20070721.fc9.src.rpm:1218688114


--- NEW FILE minisat-user-guide-1.0.html ---
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html lang="en-US">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<title>MiniSAT User Guide: How to use the MiniSAT SAT Solver</title>
<meta name="description" content="A user guide (documentation) for the MiniSAT (MiniSAT2) program, a minimalistic, open-source Boolean satisfiability problem (SAT) solver. It describes how to use MiniSAT, including its input format, options, and output format.">
<meta name="keywords" content="miniSAT, miniSAT2, SAT, satisfiability, boolean satisfiability solver, documentation, howto, user guide, input, format, open source, open source software, formal methods, free software, FLOSS, David, Wheeler, David A. Wheeler, David Wheeler">
<meta name="generator" content="vim">
</head>
<body>
<h1>MiniSAT User Guide: How to use the MiniSAT SAT Solver</h1>
<p>
<i>by <a href="http://www.dwheeler.com">David A. Wheeler</a>, version 1.00 (2008-06-28)</i>
<p>
MiniSat is a minimalistic, open-source Boolean satisfiability problem
(SAT) solver, developed for both researchers and developers; it
is released under the "MIT license".
<p>
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 it's satisfiable, most SAT solvers (including MiniSAT)
can also show a set of assignments that make the expression true.
Many problems can be broken down into a large SAT problem
(perhaps with thousands of variables), so SAT solvers have a variety
of uses.
<p>
This article is a brief
user guide (documentation) for the MiniSAT (MiniSAT2) program.
It describes how to use MiniSAT, including its input format, options,
and output format.
<p>
<p>
<h1>Conjunctive Normal Form (CNF)</h1>
<p>
Like many SAT solvers, MiniSAT requires that its input be in
conjunctive normal form (CNF or cnf).
CNF is built from these building blocks:
<ul>
<li><i>term</i>: A term is either a boolean variable (e.g., x4)
or a negated boolean variable (NOT x4, written here as -x4).
<li><i>clause</i>: A clause is a set of one or more terms, connected with OR
(written here as |); boolean variables may not repeat  inside a clause.
<li><i>expression</i>: An expression is a set of one or more clauses,
each connected by AND (written here as &).
</ul>
<p>
An example of CNF is:
<pre>
  (x1 | -x5 | x4) &
  (-x1 | x5 | x3 | x4) &
  (-x3 | x4).
</pre>
<p>
Any boolean expression can be converted into CNF;
algorithms and code for doing so are available elsewhere
(e.g., see "Artificial Intelligence: A modern Approach"
by Russel and Norvig, 1995).

<p>
<h1>MiniSAT input format</h1>
<p>
MiniSAT, like most SAT solvers, accepts its input in a simplified
"DIMACS CNF" format, which is a simple text format.
Every line beginning "c" is a comment.
The first non-comment line must be of the form:
<pre>
 p cnf NUMBER_OF_VARIABLES NUMBER_OF_CLAUSES
</pre>
<p>
Each of the non-comment lines afterwards defines a clause.
Each of these lines is a space-separated list of variables;
a positive value means that corresponding variable
(so 4 means x4), and a negative value means the negation of that variable
(so -5 means -x5).
Each line must end in a space and the number 0.
<p>
So the CNF expression above would be written as:
<pre>
 c Here is a comment.
 p cnf 5 3
 1 -5 4 0
 -1 5 3 4 0
 -3 -4 0
</pre>
<p>
The "p cnf" line means that this is SAT problem in CNF format with
5 variables and 3 clauses.   The first line after it is the first clause,
meaning x1 | -x5 | x4.
<p>
You can view this as a single expression.
Alternatively, you can view this as a set of clauses, and the
solver's job is to find the set of boolean variable assignments that
make all the clauses true.
<p>
The
<a href="http://www.satcompetition.org/2004/format-solvers2004.html">
SAT 2004 competition</a> has more information.

<p>
<h1>Invoking MiniSAT</h1>
<p>
MiniSAT's usage is:
<pre>
 minisat [options] [INPUT-FILE [RESULT-OUTPUT-FILE]]
</pre>
<p>
The INPUT-FILE is in DIMACS CNF format as described above, either
plain text or gzipped.
You can invoke it with the options "-h" or "--help" to see the other options.
<p>
The program's options include:
<pre>
  -pre           = {none,once} [Turn on preprocessor]
  -asymm
  -rcheck
  -grow          = NUM [ must be greater than 0 ]
  -polarity-mode = {true,false,rnd}
  -decay         = NUM [ 0 - 1 ]
  -rnd-freq      = NUM [ 0 - 1 ]
  -dimacs        = OUTPUT-FILE
  -verbosity     = {0,1,2}
</pre>
<p>
Options with a value must be immediately followed by "=" and its value, e.g.:
<pre>
 minisat -pre=once 
</pre>
<p>
For many problems, using the preprocessor is a good idea (-pre=once).
<p>

<p>
<h1>MiniSAT output format</h1>
<p>
When run, miniSAT sends to standard error a number of different
statistics about its execution.
It will output to standard output either
"SATISFIABLE" or "UNSATISFIABLE" (without the quote marks), depending
on whether or not the expression is satisfiable or not.
<p>
If you give it a RESULT-OUTPUT-FILE, miniSAT will write text to the file.
The first line will be "SAT" (if it is satisfiable) or "UNSAT"
(if it is not).
If it is SAT, the second line will be set of assignments to the
boolean variables that satisfies the expression.
(There may be many others; it simply has to produce <i>one</i> assignment).
<p>
So for the example above, it will produce in the output file:
<pre>
 SAT
 1 2 -3 4 5 0
</pre>
<p>
This means that it <i>is</i> satisfiable, with
x1=t, x2=t, x3=f, x4=t, and x5=t (where t is true and f is false).
Going back to our original example, we should see that this is a
solution:
<pre>
 (x1 | -x5 | x4)  = t | -t | t = t
 (-x1 | x5 | x3 | x4)  = -t | t | f | t = t
 (-x3 | x4) = -f | t = t
</pre>

<p>
<h1>Getting more solutions</h1>
<p>
If you want to get another solution, the "obvious" way is to
add, as a new clause, the negated form of the previous solution.
E.G., for our example, we could take:
<pre>
 1 2 -3 4 5 0
</pre>
and create this new input (note that the count of clauses has increased):
<pre>
 p cnf 5 4
 1 -5 4 0
 -1 5 3 4 0
 -3 -4 0
 -1 -2 3 -4 -5 0
</pre>
<p>
If we put this in file "second.in", and run:
<pre>
 minisat second.in second.out
</pre>
We will get a new solution; here's second.out:
<pre>
 SAT
 1 -2 -3 4 5 0
</pre>
IE., x1=t, x2=f, x3=f, x4=t, and x5=t.
This is a different solution from the previous one, because x2=f instead of
x2=t.
We can confirm this (it's the same as last time,
because x2 isn't even in any of the clauses):
<pre>
 (x1 | -x5 | x4)  = t | -t | t = t
 (-x1 | x5 | x3 | x4)  = -t | t | f | t = t
 (-x3 | x4) = -f | t = t
</pre>


<p>
<h1>For more information</h1>
<p>
You can get more information from:
<ul>
<li>
<a href="http://en.wikipedia.org/wiki/Boolean_satisfiability_problem">
Wikipedia's article "Boolean satisfiability problem"</a>
<li>
<a href="http://en.wikipedia.org/wiki/Conjunctive_normal_form">
Wikipedia's article "Conjunctive normal form"</a>
<li>
<a href="http://www.satlive.org/">SAT Live!</a> - links/news about the
SAT problem
<li><a href="http://www.satisfiability.org/">
The International Conferences on
Theory and Applications of Satisfiability Testing (SAT)</a>
<li>
<a href="http://www.satlib.org">SATLIB - The Satisfiability Library</a>
<li>
<a href="http://www.dwheeler.com/essays/high-assurance-floss.html">
High Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS)... with Lots on Formal Methods (aka high confidence or high integrity)</a> has a long list of FLOSS tools that support high assurance efforts,
including SAT solvers.
</ul>

<p>
<hr>
<p>
This article was written by
<a href="http://www.dwheeler.com">David A. Wheeler</a>, and is released
to the public domain.
If you use it or reference it, please credit David A. Wheeler
(though this is not a requirement for its use).
You can get this version at
<a href="http://www.dwheeler.com/essays/minisat-user-guide-1.0.html">
http://www.dwheeler.com/essays/minisat-user-guide-1.0.html</a>, or
the latest version at
<a href="http://www.dwheeler.com/essays/minisat-user-guide.html">
http://www.dwheeler.com/essays/minisat-user-guide.html</a>.

</body>


minisat2-FPU.patch:

--- NEW FILE minisat2-FPU.patch ---
--- minisat2-070721.orig/simp/Main.C
+++ minisat2-070721/simp/Main.C
@@ -244,7 +244,7 @@
 int main(int argc, char** argv)
 {
     reportf("This is MiniSat 2.0 beta\n");
-#if defined(__linux__)
+#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE)
     fpu_control_t oldcw, newcw;
     _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
     reportf("WARNING: for repeatability, setting FPU to use double precision\n");

minisat2-template.patch:

--- NEW FILE minisat2-template.patch ---
--- minisat2-070721.orig/mtl/template.mk
+++ minisat2-070721/mtl/template.mk
@@ -75,7 +75,7 @@
 ## Clean rule
 clean:
 	@rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \
-	  $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mak lib$(LIB).a lib$(LIB)d.a
+	  $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mk lib$(LIB).a lib$(LIB)d.a
 
 ## Make dependencies
 depend.mk: $(CSRCS) $(CHDRS)



--- NEW FILE minisat2-test.in ---
c
c start with comments
c
c 
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0


--- NEW FILE minisat2.spec ---
# Deal with odd and inconsistent upstream naming:
%define myname minisat
%define myversion 070721

Summary: A minimalistic, open-source SAT solver
Name: minisat2
Version: 2.0
# Use Fedora 'Snapshot' naming convention due to odd upstream version naming:
Release: 7.20070721%{?dist}
License: MIT
Group: Applications/Engineering
Source: http://minisat.se/downloads/%{name}-%{myversion}.zip
# Sent sources, test, patches (below) to upstream via email on 2008-07-08:
Source1: http://www.dwheeler.com/essays/minisat-user-guide-1.0.html
Source2: minisat2-test.in
Patch1: minisat2-FPU.patch
Patch2: minisat2-template.patch
BuildRoot: %{_tmppath}/%{name}-%{version}-%{release}-root
URL: http://minisat.se/
BuildRequires: zlib-devel

%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.

%prep
%setup -q -n %{myname}
%patch1 -p1 
%patch2 -p1 

%build
cp -p %{SOURCE1} .
cp -p %{SOURCE2} .
mv minisat-user-guide-*.html minisat-user-guide.html

# Show key execution steps, so we can see that the right flags are used.
sed -i 's/@$(CXX)/$(CXX)/' mtl/template.mk 

# Note: Could get a 1-2% speed boost by building as static (use "rs" instead
# of "r" when invoking "make"), but static executables are dispreferred by
# Fedora (they create update complications and are larger).
# If static executables were added later, they would need to
# add a dependency on zlib-static.

# Build "simp", which adds simplification capabilities, instead of just "core"
pushd simp
 make CFLAGS="-I../mtl -I../core -Wall -ffloat-store %{optflags}" r
 cp -p %{myname}* ../%{myname}
popd

%install
rm -rf %{buildroot}
mkdir -p %{buildroot}%{_bindir}
install -m 0755 %{myname} %{buildroot}%{_bindir}/

%check
# Test "minisat2-test.in" is a brief quote from
# http://www.satcompetition.org/2004/format-solvers2004.html
./minisat minisat2-test.in minisat2-test.out
echo
echo "RESULTS:"
cat minisat2-test.out
result=`head -1 minisat2-test.out`
if [ "$result" = "SAT" ]; then
  echo "SUCCESS - Correctly found that it was satisfiable"
  true
else
  echo "Failed test."
  false
fi

%clean
rm -rf %{buildroot}

%files
%defattr(-,root,root)
%doc LICENSE
%doc minisat-user-guide.html
%doc minisat2-test.in
%doc minisat2-test.out
%attr(755,root,root) %{_bindir}/%{myname}


%changelog
* Tue Aug 7 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-7.20070721
- Removed code for switching between -O2 and -O3, per reviewer request.

* Tue Aug 7 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-6.20070721
- Timing tests found -O3 was unhelpful; switched back to -O2, but left stub
  in case a switch to another -O level would help in the future.
  -O3 real 0m35.714s, 0m35.714s, 0m35.834s vs. -O2 real 0m35.296s, 0m35.301s

* Tue Jul 8 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-5.20070721
- Moved to higher optimization level (-O3); speed is critical for this app.

* Tue Jul 8 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-4.20070721
- Different version number convention to better conform to Fedora guidelines
- Made macro use consistent (not used for simple commands)
- Documented when patches and documentation sent upstream

* Sat Jun 28 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-3.20070721
- Use "make r" instead of "make" to create "released" version
- Wrote brief user guide, included as part of this package.

* Fri Jun 27 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-2.20070721
- Switched from minimal "core" to more-capable "simp" (simplifier)
- Change "make" invocation so CFLAGS includes %%{optflags}
- Add test file and %%check section (so we'd know if it worked!)
- Modified description for people who don't know what SAT solvers are.

* Thu Jun 26 2008 Earl Sammons <esammons at, hush.com> 2.0-1.20070721
- Initial build
- Include Debian patches minisat2-FPU.patch and minisat2-template.patch



Index: .cvsignore
===================================================================
RCS file: /cvs/pkgs/rpms/minisat2/F-8/.cvsignore,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- .cvsignore	10 Aug 2008 01:34:52 -0000	1.1
+++ .cvsignore	14 Aug 2008 04:28:59 -0000	1.2
@@ -0,0 +1 @@
+minisat2-070721.zip


Index: sources
===================================================================
RCS file: /cvs/pkgs/rpms/minisat2/F-8/sources,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -r1.1 -r1.2
--- sources	10 Aug 2008 01:34:52 -0000	1.1
+++ sources	14 Aug 2008 04:28:59 -0000	1.2
@@ -0,0 +1 @@
+fb12db9a13f86a2133758abfba239546  minisat2-070721.zip


