ArounD Sat (ADS) home page
|9 january 2001||version 1.12||Updated the Belief Revision module. ADS is now available as a Java Web Start application.|
|3 july 2000||version 1.11||Small update. Modified the output of SAT solvers to facilitate their manipulation. Ask for the formula to revise/contract with in Belief Revision module instead of reading the selection.|
|29 june 2000||version 1.11||Small update. Added the DavPutSt3 preprocessing step available from the command line (-ch parameter, "compress heavy"). This method is very slow for the moment.|
|21 june 2000||version 1.11||New version of DavPutSt algorithm (DavPutSt3). The algorithm preprocessing step can be applied to compress dimacs instances from ADS command line (use -c or -cl parameter). This release works only on Java 2 platform !|
|9 june 2000||version 1.10||New version of DavPutSt algorithm. To use it, call DavPutSt2 instead of DavPutSt. The latter is less efficient version of the new algorithm, since it performs the double propagation on all the variables. This release works only on Java 2 platform ! The old one is still available here.|
|6 june 2000||version 1.09||I am now using Java Hotspot Server 2.0 on NT4 with JDK 1.3. Results are amazing: the gain is around 50 % once most of the code has been compiled !|
|25 may 2000||version 1.09||Corrected a bug on Adjustment algorithm.|
|24 may 2000||version 1.09||Added Belief Revision system. Check the online help (not available on the applet) to use it.|
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.
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:
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
- 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.
Just go to the download
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]or if you are using Windows just double clic on the ADS.jar icon.
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]
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.
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
To make ADS, I am using :
syntax highlighting package.