-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathREADME.txt
181 lines (138 loc) · 5.1 KB
/
README.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
#FFASP
#A finite-valued fuzzy answer set solver
#(c) 2017 Mushthofa
Mushthofa.Mushthofa (AT) UGent.be
==============================================================================
HOW TO BUILD
-------------
System requirements:
*NIX system (Linux, FreeBSD, MacOS X) with GCC>=4.7 and CMake>=2.8
Might compile on Windows (with Cygwin), but never tested.
1) Install Boost Libraries (>=1.55).
http://www.boost.org/
Make sure it can be found in your include path
e.g. : in '/usr/include/', /'usr/local/include/' etc.
On Debian/Ubuntu, this is usually done using:
$ sudo apt-get install libboost-dev
2) Download 'clingo' (>=4.3.0) from the Potassco suite.
http://potassco.sourceforge.net/
Install it in your binary path, e.g. '/usr/bin/' or '/usr/local/bin/'
Make sure it can be called using the following command
$ clingo
3) Install GLPK libraries (https://www.gnu.org/software/glpk/).
On Debian/Ubuntu, this is usually done using:
sudo apt-get install libglpk-dev glpk-utils
4) Install Coinor-Cbc libraries (https://projects.coin-or.org/Cbc)
On Debian/Ubuntu, this is usually done using:
sudo apt-get install coinor-cbc coinor-libcbc-dev
5) Run the following commands in the directory ffasp :
$ mkdir build
$ cd build
$ cmake ../
$ make
Compilation will proceed and an executable named 'ffasp' will be created in the build directory.
USAGE
-----------------
Run with option '-h' to get the usage information.
$ ./ffasp -h
USAGE: ./ffasp [options] [<input-file>]
E.g.: ./ffasp --maxk=200 -c program.lp
Options are:
--maxk=<n> = find k-answer sets up to k=<n> (default <n>=100).
--maxt=<t> = stop after computation exceeds <t> seconds, approximately (default <t>=600 s).
--trans=<k> = only perform translation with k=<k> and print the result to <STDOUT>.
--rnd=<d> = only perform rewriting of the program and rounding the constants
in the program to rational numbers with denominator=<d>.
-c/--check = only check for satisfiability/consistency, no answer set is printed.
-h/--help = show this help and exit.
If no <input-file> is given, input is read from <STDIN>
INPUT LANGUAGE
----------------
- A term is either a constant symbol ([a-z][(A-Z)|(0-9)]*) or a quoted string or an integer.
e.g. : abc123, "Hello World", 2012.
- A variable is symbol which starts with either a capital, or the character '_' (anonymous variables).
e.g. : X, VAR1, _
- A regular atom is an expression of the form 'p(T1, T2, ..., Tn)', where p is the atom name (symbol)
and T1..Tn are its arguments, which are either a term or a variable.
e.g. : a, p(0), connect(X, Y, 1)
- A constant atom is an expression of the form '#a/b' or '#c' where a and b are integers such that 0<b<=a
and c is a rational number from [0,1] written in decimal format. If the value of a/b or c is outside of [0,1],
it will be converted to 0 or 1 accordingly.
e.g. : #2/5, #0.35
- A literal is either an atom 'a' or a constant atom #c
- A comparison predicate is an expression of the form
T1 op T2
where T1 and T2 are either variables or terms and op is one of the operators {=, !=, >, <, >=, <=}.
e.g. : X<Y, VAR_1>=0
- A body literal is either a positive literal 'l', or a NAF-literal 'not l', where l is a regular atom, or a comparison predicate.
e.g. : not edge(1,3).
- A fact is an expression of the form
a :- #c.
where a is a regular atom and #c is a constant atom.
The special fact
a.
is a shorthand for
a :- #1.
- A constraint is an expression of the form
#c :- a.
The special constraint
:- a.
is a shorthand for
#0 :- a.
- A rule is an expression of the form
a1 op_1 a2 op_1 ... op_1 an :- b1 op_2 b2 op_2 ... op_2 bm.
where a1,...,an are literals and b1, b2, ..., bm are body literals,
while each of op_1 and op_2 is one of the Lukasiewicz operators:
* = T-norm (alias: ',')
+ = T-conorm (alias: '|')
& = max
^ = min
E.g. :
a+b :- c * not d * #0.2.
p(X,Y)^r(Y) :- q(X)*s(Y)*X>Y.
t :- t+t.
- Rules must be safe, i.e. each variable appearing in a rule must also appear in one of the positive body literals.
Rules such as:
p(X,Y) :- q(X)+not r(Y).
q(X) :- p(X), X>Y.
are not safe.
- Comparison predicates can only be used in the body of a rule in conjunction with the operator *, i.e. rules such as
p(X,Y) :- q(X,Y)+X>Y.
are not allowed.
- Only one fact/constraint/rule is allowed per line of input.
EXAMPLES
---------------
1) Run 'ffasp'
$ ./ffasp
% Reading from <STDIN> (finish with Ctrl-D) %
Type in the following program and end with 'Ctrl-D':
a :- not b.
b :- not a.
#0.4 :- a.
#0.9 :- b.
<Ctrl-D>
{a[0.1], b[0.9]}
Satisfiable.
2) Run ffasp with the following program
$ ./ffasp
% Reading from <STDIN> (finish with Ctrl-D) %
a+b.
#0.2 :- a.
#0.3 :- b.
No k-answer set is found until k = 100 and time = 2 s
3) Write the following program:
a1 :- not a1.
a2 + a2 :- a1.
a3 + a3 :- a2.
a4 + a4 :- a3.
a5 + a5 :- a4.
and save it to a file named 'test.lp'
This program has only one answer set, which is
{a1[1/2], a2[1/4], a3[1/8], a4[1/16], a5[1/32]}
Run ffasp on the program:
$ ./ffasp test.lp
{a1[0.5], a2[0.25], a3[0.125], a4[0.0625], a5[0.03125]}
Satisfiable.
Now run while setting the maximum value of k to 30
$./ffasp --maxk=30 test.lp
No k-answer set is found until k = 30 and time = 2 s