Skip to content

crillab/scalop

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Scalop

Scalop is a solver designed for reasoning with argumentation frameworks, including abstract argumentation and assumption-based argumentation tasks. It was formerly named Crustabri.

This project contains both a library and from one to three binaries, depending on the selected features. The library allows to create and modify static and dynamic argumentation frameworks, and to execute queries on them. The first binary, scalop, allows various operations on input argumentation frameworks. Type scalop -h to get the description of the available subcommands and scalop <SUBCOMMAND> -h for the help for a given subcommand.

If the iccma feature is present, e.g. by compiling with cargo build --release --features iccma, two additional binaries will be present. The binary named scalop_iccma23 is a wrapper for Scalop to be compatible with the ICCMA'23 competition requirements. The binary named scalop_iccma25 is its counterpart for the 2025 edition of the competition; the main difference with the scalop_iccma23 is its ability to use an IPASIR-compatible SAT solver pointed by the IPASIR_LIBRARY environment variable.

Using an IPASIR SAT solver library

IPASIR is a simple C interface to incremental SAT solvers (it stands for Reentrant Incremental Sat solver API, in reverse.) This interface is supported by a few different solvers because it is used in the SAT competition's incremental track. Scalop is able to use any SAT solver following the IPASIR interface in place of its builtin solver.

For example, download the latest version of Cadical from its homepage (the most recent one is cadical-sc2020-45029f8.tar.xz at the time of writing). Extract the archive, then compile it with the flags required to build a shared library:

./configure CXXFLAGS=-fPIC
make -j
cd build
g++ -shared -o libcadical.so $(ls *.o | grep -v mobical.o)
IPASIR_LIBRARY=$(realpath libcadical.so)

This will create libcadical.so in the build directory of Cadical and set its path into the IPASIR_LIBRARY variable. Then, you can use this solver instead of the builtin using the dedicated CLI option:

scalop solve -f test.af -p SE-PR --ipasir-library "$IPASIR_LIBRARY"

Using an external SAT solver

Any SAT solver following the input/output format of SAT competitions can be used to replace the builtin one. Note that using an external SAT solver may decrease the performances of Scalop, especially when dealing with complex semantics.

scalop solve -f test.af -p SE-PR --external-sat-solver "$PATH_TO_SOLVER"

License

Scalop is developed at CRIL (Univ. Artois & CNRS). It is made available under the terms of the GNU GPLv3 license.

About

An argumentation framework library & solver.

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages