Adapted for ICCMA2023

.gitignore

@@ -1,4 +1,6 @@
 target
+portsat
+*.paf
 
 report/report.log
 report/report.aux

Cargo.toml

@@ -1,11 +1,11 @@
 [package]
-name = "ter"
-version = "0.1.0"
+name = "portsat"
+version = "1.0.0"
 edition = "2018"
 authors = [
-    "Christophe Yang",
-    "Quentin Januel",
-    "Sylvain Declercq",
+    "Quentin Januel ([email protected])",
+    "Sylvain Declercq ([email protected])",
+    "Christophe Yang ([email protected])",
 ]
 license = "MIT"
 

README.md

@@ -1,56 +1,21 @@
-# Computational model of argumentation
+# PORTSAT
 
-You can use the solver as described in the ICCMA'15 Supplementary Notes on probo:
+## Installation
 
-## Print the name, version and authors
-```
-cargo run --
-```
+### Prerequisites
 
-## Print the supported formats
-```
-cargo run -- --formats
-```
-**NOTE:** We have an extra format `loose-apx` which allows for APX file with less assumptions (e.g. the arguments and attacks can be mixed, or there can be multiple definitions per line). If your APX graph fails to parse with the default `apx` format, give a try to `loose-apx`. However the parsing is slower.
+PORTSAT is made in Rust, so you need to install Rust first. You can find the installation instructions [here](https://www.rust-lang.org/tools/install).
 
-## Print the supported problems
-```
-cargo run -- --problems
-```
-
-## Print the available SAT solvers
-```
-cargo run -- --solvers
-```
+### Compile source code
 
-## Solve a given problem
-```
-cargo run -- -p <problem> -f <file> -fo <fileformat> [-a <additional_parameter>] [-s <solvers>] [--pr-mss]
-```
-Example:
-```
-cargo run -- -p DC-CO -s manysat,dpll -f graph.tgf -fo tgf -a a
+You just need to run the make command in the root directory of the project.
+```bash
+make
 ```
-**NOTE**: You cannot set the solvers when the problem involves the grounded extension.
 
-**NOTE2**: The `--pr-mss` flag will make the solver use the MSS algorithms for the preferred semantics. Otherwise it will enumerate all complete extensions and filter the ones that are preferred.
+## Usage
 
-## Prerequisite
- - [Rust](https://www.rust-lang.org/)
- - [Python](https://www.python.org/) (10.0 or higher)
-### MacOS
-Make sure to have the `libomp` library installed. If you do not, you can install it with the following command:
+If the installation was successful, you can run the program with the following command:
 ```bash
-brew install libomp
-```
-
-## Compile
-The Python scripts will attempt to use the release version of the solver.
-In order to compile it, run the following command:
-```
-cargo build --release
-```
-In order to install the python dependencies, run
+./portsat
 ```
-pip install -r requirements.txt
-```

makefile

@@ -0,0 +1,5 @@
+NAME = portsat
+
+build:
+	cargo build --release
+	cp target/release/$(NAME) $(NAME)

src/af/extension.rs

@@ -33,6 +33,6 @@ impl<'a> Extension<'a> {
 
 impl fmt::Display for Extension<'_> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        write!(f, "[{}]", self.get_args().join(","))
+        write!(f, "w {}", self.get_args().join(" "))
     }
 }

src/af/format.rs

@@ -7,6 +7,7 @@ pub enum Format {
     TGF,
     APX,
     LooseAPX,
+    PAF,
 }
 
 impl Format {
@@ -15,6 +16,7 @@ impl Format {
             Format::TGF,
             Format::APX,
             Format::LooseAPX,
+            Format::PAF,
         ]
             .iter()
             .map(|f| f.to_string())
@@ -29,6 +31,7 @@ impl fmt::Display for Format {
             Format::TGF => write!(f, "tgf"),
             Format::APX => write!(f, "apx"),
             Format::LooseAPX => write!(f, "loose-apx"),
+            Format::PAF => write!(f, "paf"),
         }
     }
 }
@@ -40,6 +43,7 @@ impl FromStr for Format {
             "tgf" => Ok(Format::TGF),
             "apx" => Ok(Format::APX),
             "loose-apx" => Ok(Format::LooseAPX),
+            "paf" => Ok(Format::PAF),
             _ => Err(format!("Unknown format: {}", s)),
         }
     }

src/af/mod.rs

@@ -122,6 +122,36 @@ impl AF {
         }
         Self { arguments }
     }
+    pub fn from_paf(tgf: &str) -> Self {
+        let mut lines = tgf.lines();
+        let n = lines.next().unwrap().split(" ").nth(2).unwrap().parse::<usize>().unwrap();
+        let mut arguments = vec![];
+        for i in 1..=n {
+            let name = format!("{i}");
+            let arg = Argument {
+                name,
+                attackers: vec![],
+            };
+            arguments.push(arg);
+        }
+        for line in lines {
+            if line.is_empty() {
+                continue;
+            }
+            if line.starts_with("#") {
+                continue;
+            }
+            let mut iter = line.split(" ");
+            let (a, b) = (
+                iter.next().unwrap(),
+                iter.next().unwrap(),
+            );
+            let a_ind = a.parse::<usize>().unwrap() - 1;
+            let b_ind = b.parse::<usize>().unwrap() - 1;
+            arguments[b_ind].attackers.push(a_ind);
+        }
+        Self { arguments }
+    }
     pub fn phi_co(&self) -> CNF {
         let mut cnf = CNF::new();
         let len = self.arguments.len();

src/main.rs

@@ -11,6 +11,7 @@ use af::{
     AF,
     format::Format,
 };
+use problem::Semantics;
 use utils::{
     args::Args,
     solvers,
@@ -19,6 +20,8 @@ use utils::{
 use std::{convert::TryInto, str::FromStr};
 use solver::solve;
 
+use crate::problem::Problem;
+
 fn main() -> Result<(), String> {
     let args = Args::new();
     if args.has("-v") {
@@ -34,12 +37,13 @@ fn main() -> Result<(), String> {
         solvers::show_available();
     } else if let Some(problem) = args.get("-p") {
         let param = args.get("-a");
-        let problem = (problem, param).try_into()?;
+        let problem: Problem = (problem, param).try_into()?;
         let file = args.get("-f")
             .ok_or("The file is not specified")?;
         let format = Format::from_str(
             args.get("-fo")
-                .ok_or("The format is not specified")?
+                .unwrap_or("paf")
+                // .ok_or("The format is not specified")?
         )?;
         let file = utils::read_file(file)?;
         let af = benchmark!(
@@ -48,13 +52,15 @@ fn main() -> Result<(), String> {
                 Format::TGF => AF::from_tgf(&file),
                 Format::APX => AF::from_apx(&file),
                 Format::LooseAPX => AF::from_loose_apx(&file),
+                Format::PAF => AF::from_paf(&file),
             },
         );
+        let is_gr = problem.semantics == Semantics::Grounded;
         solve(
             af,
             problem,
-            solvers::get_from_arg(args.get("-s")),
-            args.has("--pr-mss"),
+            solvers::get_from_arg(/*args.get("-s"),*/ is_gr),
+            // args.has("--pr-mss"),
         )?;
     } else {
         utils::details();

src/problem/semantics.rs

@@ -3,7 +3,7 @@ use std::{
     convert::TryFrom,
 };
 
-#[derive(Clone)]
+#[derive(Clone, PartialEq)]
 pub enum Semantics {
     Complete,
     Grounded,

src/solver/grounded.rs

@@ -31,13 +31,22 @@ pub fn solve(
     match task {
         Task::FindOne => println!("{}", extension),
         Task::Enumerate => println!("[{}]", extension),
-        Task::Credulous(arg) | Task::Skeptical(arg) => {
+        Task::Credulous(arg) => {
             if extension.contains(arg) {
                 println!("YES");
+                println!("{}", extension);
             } else {
                 println!("NO");
             }
         },
+        Task::Skeptical(arg) => {
+            if extension.contains(arg) {
+                println!("YES");
+            } else {
+                println!("NO");
+                println!("{}", extension);
+            }
+        },
     };
     Ok(())
 }

src/solver/mod.rs

@@ -16,7 +16,7 @@ pub fn solve(
     af: AF,
     problem: Problem,
     sat_solver: Option<Box<dyn Solver>>,
-    pr_mss: bool,
+    // pr_mss: bool,
 ) -> Result<(), String> {
     match &problem.semantics {
         Semantics::Complete => {
@@ -38,7 +38,7 @@ pub fn solve(
         Semantics::Grounded =>
             grounded::solve(&af, &problem.task, sat_solver)?,
         Semantics::Preferred =>
-            preferred::solve(&af, &problem.task, sat_solver, pr_mss),
+            preferred::solve(&af, &problem.task, sat_solver/*, pr_mss*/),
     }
     Ok(())
 }

src/solver/preferred/enum_co.rs

@@ -57,26 +57,28 @@ pub fn solve(
             Task::Enumerate => println!("[{}]", preferred.iter()
                 .map(|e| e.to_string())
                 .collect::<Vec<_>>()
-                .join(","),
+                .join(", "),
             ),
             Task::Credulous(arg) => {
-                if preferred
+                let extension = preferred
                     .iter()
-                    .any(|e| e.contains(arg))
-                {
+                    .find(|e| e.contains(arg));
+                if let Some(extension) = extension {
                     println!("YES");
+                    println!("{}", extension);
                 } else {
                     println!("NO");
                 }
             },
             Task::Skeptical(arg) => {
-                if preferred
+                let extension = preferred
                     .iter()
-                    .all(|e| e.contains(arg))
-                {
-                    println!("YES");
-                } else {
+                    .find(|e| !e.contains(arg));
+                if let Some(extension) = extension {
                     println!("NO");
+                    println!("{}", extension);
+                } else {
+                    println!("YES");
                 }
             },
             _ => unreachable!(),

src/solver/preferred/mod.rs

@@ -11,11 +11,15 @@ pub fn solve(
     af: &AF,
     task: &Task,
     sat_solver: Option<Box<dyn Solver>>,
-    mss: bool,
+    // mss: bool,
 ) {
-    if mss {
-        mss::solve(af, task, sat_solver)
-    } else {
-        enum_co::solve(af, task, sat_solver)
+    match task {
+        Task::FindOne => mss::solve(af, task, sat_solver),
+        _ => enum_co::solve(af, task, sat_solver),
     }
+    // if mss {
+    //     mss::solve(af, task, sat_solver),
+    // } else {
+    //     enum_co::solve(af, task, sat_solver)
+    // }
 }