[Home] [Agent] [ADS][A][B][D] [Java] [SAT][ADS4SAT]

ArounD Sat (ADS) home page current version is 1.12 (9 january 2001)

What's new ?

What is ADS ?

ADS is a tool I began developing during my Ph.D. thesis in French IRIT laboratory, in Toulouse. My supervisor was Michel Cayrol.

ADS uses modified versions of SATisfaction algorithms to solve problems related to SAT: for instance, computing minimal models, compute an explanation, etc.

This tool is an academic tool, design to test certain algorithms behaviour and their application in propositional reasoning. It is not yet tuned for largescale real applications but can be useful if you want to test propositional reasoning approaches to solve your kind of problem, or for teaching purpose.
 

Features:

• Consistency checking (SAT problem)
• ATMS/[A]CMS: compute preferred label/nogoods.
• Closed World Reasoning (CWR): compute free for negation formulas for the five CWR
• Decision under uncertainty

What does ADS look like ?

ADS is also a tool that can be used from the command line to execute scripts or solving SAT instances.

If you have a Java Plugin 1.2 enabled browser, you can take a look at the ADS applet.

Alternatively, you can try the Java Web Start technology. It's a new way to deploy Java applications on the web. This technology is currently available for Windows, Linux and Solaris. You just need to download the Java Web Start launcher.
You have two possibilites:

• restricted application: it works as an applet, so do not let you have access to your hard drive to read/save a base. The main advantage is that you always run the last version of the tool, locally.
• If you trust me, you can try to launch ADS with the unrestricted option, such that you will be able to access to your hard drive to read/save files, and use Drag&Drop. This is the best way to use ADS if you have an internet connection: you will always run the last version on your computer.

ADS requirements

ADS is written in Java, so it can be used on most common platforms (Solaris/Windows/MacOs/Linux).
To use ADS you need a Java Virtual Machine. See our Java resource page to look for a JVM for your preferred OS.

ADS uses also two additional packages that can be found on Sun Java web site:
- Swing, which is a core package since the Java 1.2 release. You only need to download it if you have a Java 1.1.X virtual machine.
- Java Help.

Please install these two packages if needed before downloading ADS. Alternatively, if you do not want to install the whole Java Help package, you can download a simple JavaHelp package here.
 

How can I obtain it ?

Just go to the download page.
 

How to run it ?

If you are using a Java 2 virtual machine (aka JDK 1.2.X or greater), just put ADSJ2.jar and jh.jar in the same directory and just type:

java -jar ADSJ2.jar [command line parameters]

If you don't have a Java 2 compatible JVM, add ADS.jar and jh.jar in your CLASSPATH and type:

java ADS [command line parameters]

Where can I found documentation about ADS ?

ADS contains online help. Unfortunately, only the french version is available, I have not translated the help files in english yet.

You can use ADS for solving satisfaction problems: checkout this page.

I have also made a little tutorial (pdf format). The examples of the tutorial (and some others soon) can be found here.

If you experience some strange behaviour of ADS, take a look of ADS known bugs.

You can take a look to ADS api. For the moment, most of the comments are in French ! Please contact me if you want ADS sources.

If you have some questions, comments, wishes, feel free to contact me.
 

References

Salem Benfehart, Souhila Kaci, Daniel Le Berre, and Mary-Anne Williams. Weakening conflicting information for iterated revision and knowledge integration. In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI'01), Seattle, Washington, USA, August 4th-10th 2001. to appear.

Daniel Le Berre, ADS: a unified computational framework for some consistency and abductive based propsositional reasoning, In Proceedings of the 2nd Australasian Workshop on Computational Logic (AWCL01), 31 january-1 february 2001, Gold Coast, Australia. (pdf version)

Daniel Le Berre, Autour de SAT : le calcul d'impliquants P-restreints, algorithmes et applications, PhD thesis, Université Toulouse III - Paul Sabatier, presented the 12th january 2000 at IRIT, Toulouse, 2000.  (in French) (PDF version)

Dubois, D., Le Berre, D., Prade, H. and Sabbadin, R.Using Possibilistic Logic for Modeling Qualitative Decision: ATMS-based Algorithms In Fundamenta Informaticae (37) pp. 1-30, 1999 (postcript version)

Castell, T., Cayrol, C., Cayrol, C. and Le Berre, D.Modèles P-restreints : application à l'inférence propositionnelle In proc. of RFIA (RFIA'98), pp. 205-214, 1998  (in French)

Dubois, D., Le Berre, D., Prade, H. and Sabbadin, R.Logical representation and computation of optimal decisions in a qualitative setting In Proc. of the 14th National Conference on Artificial Intelligence (AAAI'98), pp. 588-593, 1998 (postcript version).

Le Berre, D. and Sabbadin, R.Decision-theoretic diagnosis and repair: representational and computational issues In Proc. of the 8th International Workshop on Principles of Diagnosis(DX'97), pp. 141-145, 1997 (postcript version)

Castell, T., Cayrol, C., Cayrol, M. and Le Berre, D.Using the Davis and Putnam procedure for an efficient computation of preferred models In proc. of ECAI'96, pp. 350-354, 1996 (postcript version)

Amgoud, L., Cayrol, C. and Le-Berre, D.Comparing Arguments Using Preference Orderings for Argument-based Reasoning In proc. of the 8th IEEE International Conference on Tools with Artificial Intelligence, pp. 400-403, 1996
 

Credits

To make ADS, I am using :

, jEdit syntax highlighting package.