Re: [Caml-list] [ANN] Boolean expression simplifier library

["\"Markus W. Weißmann\"" <markus.weissmann@in.tum.de>]

Hello,

On 19 Apr 2012, at 02:56, Francois Berenger wrote:

> I'm curious, what is it used for?
> 
> Is it for people doing proof checkers or things like this?
> 

Like that, yes:
We successfully use it for reducing the size of programs we want to perform model checking on. My concrete target are industrial robot systems [1].

I even tried to integrate it into a compiler to reduce the size of right-hand-side boolean expression; unfortunately for small expressions the normalization (that occurs during minimization) often made the results less optimal than just some heuristic rewriting rules.

Generally speaking you would use it for optimizing the execution time of boolean expressions; I would guess that the biggest user base of similar implementations are electrical engineers designing circuit boards.


Regards

-Markus

[1] http://www6.in.tum.de/Main/Publications/Weissmann2011.pdf

> On 04/19/2012 07:26 AM, "Markus W. Weißmann" wrote:
>> Hi,
>> 
>> I'd like to announce the first public release of the 'boolean expression simplifier' library "bes".
>> It is an implementation of several algorithms for minimizing boolean expressions similar to the espresso solver [1] -- though in OCaml.
>> The source code is available on ocamlforge under the new bsd license:
>> 
>> http://bes.forge.ocamlcore.org/
>> 
>> It comes with a simple front-end program for reading and simplifying expressions in DFA from text files.
>> Students trying to verify their Karnaugh Veitch map solutions rejoice! ;)
>> 
>> 
>> Regards
>> 
>> -Markus
>> 
>> [1] http://embedded.eecs.berkeley.edu/pubs/downloads/espresso/index.htm
>> 
> 

-- 
Markus Weißmann, M.Sc.
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
http://wwwknoll.in.tum.de/