README.txt 3.54 KB
Newer Older
Masahiko Sakai's avatar
Masahiko Sakai committed
1 2 3 4 5


  naps-1.02-maxsat  is equivalent to naps-1.02 with -max-sat option


Masahiko Sakai's avatar
Masahiko Sakai committed
6 7 8
==== NaPS 1.x solver ==== 

Overall:
Masahiko Sakai's avatar
Masahiko Sakai committed
9 10 11 12 13
NaPS (Nagoya pseudo-Boolean solver) is a pseudo-Boolean solver for 
linear problems with Boolean variables developped at Nagoya University.

Linear constraint y1 - 3*y2 = 0 is described as
  1 y1 -3 y2 = 0 ;
Masahiko Sakai's avatar
Masahiko Sakai committed
14

Masahiko Sakai's avatar
Masahiko Sakai committed
15 16 17 18 19 20 21 22 23 24 25 26 27
NaPS follows MiniSAT+ for the input format, for example:

* #variable= 2 #constraint= 2
min: 1 x1 1 y1 ;
1 x1 -1 y1 >= 0 ;
1 x1  2 y1 <= 2 ;

where the first two lines are optional.


[Negated Boolean variable]
~x1 denotes the negation of x1 as the following example:
  1 ~x1 2 x2 3 ~x3 = 3;
Masahiko Sakai's avatar
Masahiko Sakai committed
28 29

[facility of definition]
Masahiko Sakai's avatar
Masahiko Sakai committed
30 31 32 33 34 35 36 37 38 39
In addition to ordinary constraints interpreted conjunction.  This
solver has a facility of definition, which enables us to write complex 
formulas like CNFs.  For example,
  d x3 => 1 x1 -2 x2 > 0 ;
represents a constraint meaning
  x3 implies x1 - 2*x2 >0

As another example, the following description denotes (c1 or c2) and
((not c2) or (not c3)):
  d x1 => c1 ;
Masahiko Sakai's avatar
Masahiko Sakai committed
40
  d x2 <=> c2 ;
Masahiko Sakai's avatar
Masahiko Sakai committed
41
  d x3 <= c3 ;
Masahiko Sakai's avatar
Masahiko Sakai committed
42
  1 x1 1 x2 >= 1 ;
Masahiko Sakai's avatar
Masahiko Sakai committed
43 44 45
  1 ~x2 1 ~x3 >= 1 ;
where in real description, c1, c2, and c3 should be replaced by
linear constraints.
Masahiko Sakai's avatar
Masahiko Sakai committed
46 47 48 49


[minimization]
Minimizing goal value facility is inherited from minisatp.
Masahiko Sakai's avatar
Masahiko Sakai committed
50 51
e.g.
  min: 1 x1 -1 x2
Masahiko Sakai's avatar
Masahiko Sakai committed
52 53 54

[model counting]
Finding number of models is possible, inherited from minisatp.
Masahiko Sakai's avatar
Masahiko Sakai committed
55 56 57 58
Projection model counting is also possible, where variables
that appear in minimization goal are focused on.  In this case,
minimization goal is ignored and used only for denoting a set of
variables.
Masahiko Sakai's avatar
Masahiko Sakai committed
59 60 61 62

[soft constraint]
Soft constraints are accepted, like
  [3] 1 y1 3 = 0
Masahiko Sakai's avatar
Masahiko Sakai committed
63
[3] shows the penalty in case of the model does not satisfy this.
Masahiko Sakai's avatar
Masahiko Sakai committed
64 65
The solver tries to find a model with minimum sum of penalties.

Masahiko Sakai's avatar
Masahiko Sakai committed
66 67 68 69 70 71 72
[dimacs inputs]
-dimacs option enables to read dimacs cnf files.

[maxsat mode]
-max-sat option states to solve maxsat cnf/wcnf.


Masahiko Sakai's avatar
Masahiko Sakai committed
73 74
===
NaPS 1.00 is a release, renamed version of gpw-2.18, 
Masahiko Sakai's avatar
Masahiko Sakai committed
75
where gpw solvers are developed based on minisatp-1.0: 
Masahiko Sakai's avatar
Masahiko Sakai committed
76
  http://minisat.se/MiniSat+.html
Masahiko Sakai's avatar
Masahiko Sakai committed
77 78 79 80 81 82 83
We thank Niklas Een and Niklas Srensson.

NaPS distribution contains several SAT-solvers.  NaPS invokes
Glueminisat by default.

All versions of gpw-2.x and NaPS-1.x are developped by Masahiko Sakai 
and his colleges.
Masahiko Sakai's avatar
Masahiko Sakai committed
84 85

----------------------------------------------------------------------
Masahiko Sakai's avatar
Masahiko Sakai committed
86
For showing its usage, try 
Masahiko Sakai's avatar
Masahiko Sakai committed
87 88 89
     naps --help
----------------------------------------------------------------------

Masahiko Sakai's avatar
Masahiko Sakai committed
90 91
See INSTALL for its installation.

Masahiko Sakai's avatar
Masahiko Sakai committed
92 93
Known BUG:
- -S may result wrong answer.
Masahiko Sakai's avatar
Masahiko Sakai committed
94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
- Combination of -Simp and -es1 may result wrong answer.

Version 1.02 Apr 13, 2016
  - Modulo reduction for optimized-base [TACAS 2011]
    with primes up to 10000.
  - New cost function for optimized-base calculation (kind_digits).
  - A bug fixed on parsing
  - Parser routing for Dimacs format
  - MaxSAT competition mode
  - Several tunings (binary search, preserving memory in optimization, etc)
  - Added => and <= facility on definition.
  - Added the handler for SIGABRT commonly raised by lack of memory.
  - -Simp and -noSimp option introduced, which switches to
    'simplification solver' (-Simp is default if possible)
    -Simp works with glueminisat or ccminisat.
  - Fixed a bug on -model-check option.
110 111 112 113 114

Version 1.01 Mar 25, 2016.
  - Fixed the following bugs.
    = A bug when calling Simp-solvers in 1.00.
    = A bug when the simplification solver of glueminisat is used.
Masahiko Sakai's avatar
Masahiko Sakai committed
115
    = A bug on displaying 'o' value in rare case. 
Masahiko Sakai's avatar
Masahiko Sakai committed
116 117 118 119 120 121

Version 1.00  July 30, 2015.
  - released.  It was renamed from 'gpw version 2.18'.  In default,
    it uses simplification solver of glueminisat as an underlying
    SAT solver.