You can subscribe to this list here.
2010 
_{Jan}

_{Feb}

_{Mar}

_{Apr}

_{May}

_{Jun}

_{Jul}

_{Aug}

_{Sep}
(1) 
_{Oct}
(8) 
_{Nov}

_{Dec}


2011 
_{Jan}

_{Feb}

_{Mar}
(5) 
_{Apr}
(4) 
_{May}
(2) 
_{Jun}

_{Jul}
(7) 
_{Aug}
(34) 
_{Sep}
(11) 
_{Oct}
(25) 
_{Nov}
(9) 
_{Dec}
(19) 
2012 
_{Jan}
(3) 
_{Feb}

_{Mar}
(7) 
_{Apr}
(13) 
_{May}
(13) 
_{Jun}
(24) 
_{Jul}
(16) 
_{Aug}
(2) 
_{Sep}

_{Oct}
(14) 
_{Nov}
(34) 
_{Dec}
(9) 
2013 
_{Jan}
(38) 
_{Feb}
(18) 
_{Mar}
(17) 
_{Apr}
(17) 
_{May}
(36) 
_{Jun}
(3) 
_{Jul}
(4) 
_{Aug}
(25) 
_{Sep}
(25) 
_{Oct}
(15) 
_{Nov}
(29) 
_{Dec}
(9) 
2014 
_{Jan}
(40) 
_{Feb}
(84) 
_{Mar}
(25) 
_{Apr}
(47) 
_{May}
(28) 
_{Jun}
(21) 
_{Jul}
(19) 
_{Aug}
(27) 
_{Sep}
(16) 
_{Oct}
(68) 
_{Nov}
(33) 
_{Dec}
(15) 
2015 
_{Jan}
(15) 
_{Feb}
(16) 
_{Mar}
(2) 
_{Apr}
(11) 
_{May}
(16) 
_{Jun}
(65) 
_{Jul}
(26) 
_{Aug}
(22) 
_{Sep}
(18) 
_{Oct}
(40) 
_{Nov}
(14) 
_{Dec}
(18) 
2016 
_{Jan}
(8) 
_{Feb}
(38) 
_{Mar}
(11) 
_{Apr}
(47) 
_{May}
(12) 
_{Jun}
(5) 
_{Jul}
(10) 
_{Aug}
(3) 
_{Sep}
(30) 
_{Oct}
(32) 
_{Nov}
(29) 
_{Dec}
(10) 
2017 
_{Jan}
(5) 
_{Feb}
(9) 
_{Mar}
(38) 
_{Apr}
(6) 
_{May}
(2) 
_{Jun}
(10) 
_{Jul}
(26) 
_{Aug}
(14) 
_{Sep}
(5) 
_{Oct}
(26) 
_{Nov}
(15) 
_{Dec}
(1) 
S  M  T  W  T  F  S 






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
(1) 
27
(2) 
28

29
(2) 
30
(2) 
31







From: Martin <mjb@cs...>  20110730 18:05:26

On Fri, 20110729 at 14:07 0500, Linas Vepstas wrote: > On 29 July 2011 11:03, Roland Kaminski <kaminski@...> wrote: <snip> > > it is probably easier to switch to a solver that allows for a more compact > > representation of your constraints, e.g., an SMT solver. > > Well, yes. I have not looked at clingon; it was about linear arithmetic, > and I'm interested in boolean logic. At the risk of telling you things that you already know... there are at least two AnsProlog encoding of the functional units of a processor, one is TOAST, that I wrote back in 2004/2005 and one is in our current project, Riposte ( http://forge.opendo.org/projects/riposte/ ). the code from which you would be welcome to use as it is GPL. To my mind there are fundamentally four ways of reasoning about ranges of integers: 1. A direct discrete encoding with a single Boolean variable for each value assignment and implicit constraints that exactly one must be true. O(domain size) space. 2. As a low and upper bound for the range. O(1) space. 3. A binary / logarithmic encoding, with Boolean variables representing bits in each number. O(log(domain size)) space. 4. Treat as a genuine mathematical integer and use constraints to bound the range. (Ofcourse there are variants of all of these, using sparse bounds, using alternative Boolean encodings (either alternatives to 2's complement or different ways of instantiating these), etc.) ASP solvers allow 1 and 3 to be encoded (we are working on automatically pivoting between these two representations in Riposte). CSP solvers tend to have implicit support for 1 and 2, with 3 possible to encode. SMT solvers have native support for 3 and 4 with 1 possible to encode. Although in the later two cases the amount of effort to encode them would be significant. Which is best  well ... it depends on what you are trying to do. 1. is good for small ranges as it allows powerful propagation but the space overhead will kill performance once the range gets too large. 50100 seems to be the accepted wisdom. 2. is good for large ranges, especially if the constraints are `convex' or cutting plane like. 3. is robust and very good for bitwise reasoning (unsurprisingly) but some nonlinear operations such as multiplication and power can get very costly. 4. allows you to handle unbounded integer ranges and will be good if the constraints are largely linear arithmetic. If you are trying to model processor internals in AnsProlog, I would recommend (from experience) 3, with 1 as a possible optimisation. <rant> Ultimately, these are implementation choices and having to make these at the start of representing a problem shows a weakeness in our modelling languages. Which to pick is not a property of the problem, it is dependent on the instance and the solver(s) used. </rant> HTH Cheers,  Martin 
From: Torsten Schaub <torsten@cs...>  20110730 12:58:06

Hi, just to let you know that I uploaded this year's systemoriented presentations at ICLP, LPNMR, and POS to Potassco's support wiki at http://sourceforge.net/apps/mediawiki/potassco/ Best wishes, torsten 
From: Linas Vepstas <linasvepstas@gm...>  20110729 19:07:51

On 29 July 2011 11:03, Roland Kaminski <kaminski@...> wrote: > On Wednesday, July 27, 2011 04:39:43 pm Linas Vepstas wrote: >> >> Does gringo/clingo have a predicate to distinguish strings from numbers? >> >> So, for example, if a number is small, I can write: >> >> >> >> num(0..5000) . >> >> foo(X) : bar(X), num(X) . >> >> >> >> which works well if X is less than 5000. But what I really want is for >> >> num(X) to be true if X is a number, and undefined if X is a string. >> >> Is there a way to do this? > For a few thousand atoms you will probably not feel any impact on performance. > As soon as you start to define too many, then there is trouble ahead. Well, yes, of course. But I think this misses the point. Practically speaking, I've found that using p(1..60000) requires less than a cpusecond or so, and doubling the range doubles the amount of cpu time. No surprise. The point is that modelling a 32bit hardware register in asp requires 32 atoms, more or less. To be precise, N times 32 atoms, with N depending on the number of adjunct electronic systems attached to the hardware. >From the grounding/solving point of view N*32 is quite doable even if N is in the hundreds. However, such boolean circuits can potentially explore 2^32 truth assignments. Clearly, one does not want to have say p(1..2^32) to deal with this. And, in fact, one doesn't need to: one just needs an atom that responds algorithmically: if X is an unsigned int, then p(X) is true. The lua code you supplied seems to work perfectly for this: its just slightly inelegant; in place of p(X) I now hat to write @isNumber(X) == 1 which is OK .. just not elegant. > it is probably easier to switch to a solver that allows for a more compact > representation of your constraints, e.g., an SMT solver. Well, yes. I have not looked at clingon; it was about linear arithmetic, and I'm interested in boolean logic. I'll look more carefully; but even so, I'm not convinced that I truly need it, just yet; I haven't tripped over anything insurmountable yet, although my lack of the @isNumber(X) == 1 solution had me worried for a while. What this does make clear is that lua can be used to implement "naive SMT" within ASP; I wonder what sort of realworld problems might require deeper SMT support that goes beyond such a naive approach... linas 
From: Roland Kaminski <kaminski@cs...>  20110729 16:04:00

On Wednesday, July 27, 2011 04:39:43 pm Linas Vepstas wrote: > >> Does gringo/clingo have a predicate to distinguish strings from numbers? > >> So, for example, if a number is small, I can write: > >> > >> num(0..5000) . > >> foo(X) : bar(X), num(X) . > >> > >> which works well if X is less than 5000. But what I really want is for > >> num(X) to be true if X is a number, and undefined if X is a string. > >> Is there a way to do this? > > > > One way to do this would be to attach type information: > > p(string("a")). > > p(string("b")). > > p(string("c")). > > p(int(1)). > > p(int(2)). > > p(int(3)). > > Then you can use unification to perform the check: > > foo(int(X)) : bar(int(X)). > > % or foo(X) : bar(int(X)). > > Hmm. unexpected. Any comments about performance of this? > In my case, X can potentially range over 2^32 values, although > realistically, I don't think more than a few thousand ever get > grounded (but I don't know/haven't (yet) looked) (or whatever; > I haven't yet thought about grounding vs. solving...) For a few thousand atoms you will probably not feel any impact on performance. As soon as you start to define too many, then there is trouble ahead. In such a case you might be able to change the representation of your problem to avoid defining too many atoms. Of course it might be very involved to do this. Then it is probably easier to switch to a solver that allows for a more compact representation of your constraints, e.g., an SMT solver. > > Another way would be to utilize lua to create a function that checks > > whether a value is a string: > > #begin_lua > > function isString(x) > > return Val.type(x) == Val.STRING or Val.type(x) == Val.ID > > end > > #end_lua. > > I'll try this, although I believe that this would best be implemented > as a builtin primitive (after all, the other primitives, e.g. add, > subtract) are there, and this one is pretty fundamental.) If the > overwhelming urge hits me, I could prepare a patch to gringo; would you > accept > such a thing? In principal yes, but my goal is to keep the language simple and not add too many primitives. Furthermore, I am not sure whether, from a knowledge representation point of view, it is desirable to have such a feature. If you stuff terms as arguments into a predicate, in my opinion, all those terms should share certain properties, like being integers on which arithmetical operations are allowed. > Anyway, I've really, really found ASP to be very nice for this purpose; > I've noted that SMT solvers seems to be popular among hardware > engineers, but I attempted to create exactly the same model using > SMT and ASP and found ASP infinitely easier & more pleasant. > That might change if/when the SMT solver people fully support the > lisplike interfaces given in SMTLIB2 ... which begs the question: > has there been any thought or work towards adding SMTlike > capabilities to ASP? Personally, I'm interested in the bitvector > theories, not the lineararithmetic theories, but thought I'd ask. We have a solver that incorporates a CSP solver into clingo; it is called clingcon (http://www.cs.unipotsdam.de/clingcon/). Unfortunately, this version is a bit outdated. Otherwise, there is work by Illka Niemela's group to translate ASP to SMT, which in principal allows for using SMT theories in ASP programs. You can google: Integrating Answer Set Programming and Satisfiability Modulo Theories. Regards, Roland 
From: Linas Vepstas <linasvepstas@gm...>  20110727 14:40:10

Hi Roland, On 27 July 2011 05:59, Roland Kaminski <kaminski@...> wrote: > On Tuesday, July 26, 2011 11:06:48 pm Linas Vepstas wrote: >> Hi, >> >> I've been using clingo a lot recently, and have come to really, really >> enjoy it! Although SMT solvers get a lot of attention these days, I'm not >> sure its deserved, >> as I find that writing ASP code is far far easier/simpler than writing >> equivalent >> SMT code! So congratulations on a job well done! > Thanks. Now, we just need the theories of SMT in ASP, but there is ongoing > work in this direction. > >> And now for the question: >> >> Does gringo/clingo have a predicate to distinguish strings from numbers? >> So, for example, if a number is small, I can write: >> >> num(0..5000) . >> foo(X) : bar(X), num(X) . >> >> which works well if X is less than 5000. But what I really want is for >> num(X) to be true if X is a number, and undefined if X is a string. >> Is there a way to do this? > One way to do this would be to attach type information: > p(string("a")). > p(string("b")). > p(string("c")). > p(int(1)). > p(int(2)). > p(int(3)). > Then you can use unification to perform the check: > foo(int(X)) : bar(int(X)). > % or foo(X) : bar(int(X)). Hmm. unexpected. Any comments about performance of this? In my case, X can potentially range over 2^32 values, although realistically, I don't think more than a few thousand ever get grounded (but I don't know/haven't (yet) looked) (or whatever; I haven't yet thought about grounding vs. solving...) > Another way would be to utilize lua to create a function that checks whether a > value is a string: > #begin_lua > function isString(x) > return Val.type(x) == Val.STRING or Val.type(x) == Val.ID > end > #end_lua. I'll try this, although I believe that this would best be implemented as a builtin primitive (after all, the other primitives, e.g. add, subtract) are there, and this one is pretty fundamental.) If the overwhelming urge hits me, I could prepare a patch to gringo; would you accept such a thing? >> Just to be clear, I want foo(X) to be true if bar(X) is true, and >> if X is a 32bit unsigned integer. I really don't care about num(X) >> at all; its just a handy utility in the above example. >> >> Ideally, I'd like one predicate if X is an unsigned 32bit integer >> (running from 0 to 2^321) and another for a signed integer >> (2^31 to 2^311) > There is no dedicated unsigned integer in gringo; all integers are signed. I'll have to ponder this. I'm using this to model a CPU, and its easiest to think of values stored in registers as 32bit unsigned quantities. But perhaps the signedness doesn't matter at all for my code. Anyway, I've really, really found ASP to be very nice for this purpose; I've noted that SMT solvers seems to be popular among hardware engineers, but I attempted to create exactly the same model using SMT and ASP and found ASP infinitely easier & more pleasant. That might change if/when the SMT solver people fully support the lisplike interfaces given in SMTLIB2 ... which begs the question: has there been any thought or work towards adding SMTlike capabilities to ASP? Personally, I'm interested in the bitvector theories, not the lineararithmetic theories, but thought I'd ask. linas 
From: Roland Kaminski <kaminski@cs...>  20110727 10:59:56

On Tuesday, July 26, 2011 11:06:48 pm Linas Vepstas wrote: > Hi, > > I've been using clingo a lot recently, and have come to really, really > enjoy it! Although SMT solvers get a lot of attention these days, I'm not > sure its deserved, > as I find that writing ASP code is far far easier/simpler than writing > equivalent > SMT code! So congratulations on a job well done! Thanks. Now, we just need the theories of SMT in ASP, but there is ongoing work in this direction. > And now for the question: > > Does gringo/clingo have a predicate to distinguish strings from numbers? > So, for example, if a number is small, I can write: > > num(0..5000) . > foo(X) : bar(X), num(X) . > > which works well if X is less than 5000. But what I really want is for > num(X) to be true if X is a number, and undefined if X is a string. > Is there a way to do this? One way to do this would be to attach type information: p(string("a")). p(string("b")). p(string("c")). p(int(1)). p(int(2)). p(int(3)). Then you can use unification to perform the check: foo(int(X)) : bar(int(X)). % or foo(X) : bar(int(X)). Another way would be to utilize lua to create a function that checks whether a value is a string: #begin_lua function isString(x) return Val.type(x) == Val.STRING or Val.type(x) == Val.ID end #end_lua. p(1). p(2). p("a"). p("b"). string(X) : p(X), @isString(X) == 1. nstring(X) : p(X), @isString(X) == 0. > Just to be clear, I want foo(X) to be true if bar(X) is true, and > if X is a 32bit unsigned integer. I really don't care about num(X) > at all; its just a handy utility in the above example. > > Ideally, I'd like one predicate if X is an unsigned 32bit integer > (running from 0 to 2^321) and another for a signed integer > (2^31 to 2^311) There is no dedicated unsigned integer in gringo; all integers are signed. If you want to distinguish between signed and unsigned integers, all you can do is attach type information, like: p(signed(1)) p(signed(1)) p(unsigned(3)) Of course, you still do not get 2^32 different positive integers this way. If you just want to know whether a number is positive, you can of course simply use the >= 0 comparison. Regards, Roland 
From: Linas Vepstas <linasvepstas@gm...>  20110726 21:07:15

Hi, I've been using clingo a lot recently, and have come to really, really enjoy it! Although SMT solvers get a lot of attention these days, I'm not sure its deserved, as I find that writing ASP code is far far easier/simpler than writing equivalent SMT code! So congratulations on a job well done! And now for the question: Does gringo/clingo have a predicate to distinguish strings from numbers? So, for example, if a number is small, I can write: num(0..5000) . foo(X) : bar(X), num(X) . which works well if X is less than 5000. But what I really want is for num(X) to be true if X is a number, and undefined if X is a string. Is there a way to do this? Just to be clear, I want foo(X) to be true if bar(X) is true, and if X is a 32bit unsigned integer. I really don't care about num(X) at all; its just a handy utility in the above example. Ideally, I'd like one predicate if X is an unsigned 32bit integer (running from 0 to 2^321) and another for a signed integer (2^31 to 2^311) If there is such a function, its not mentioned in the user's guide of 4 October 2010. Thanks, linas 