diff --git a/.gitignore b/.gitignore index 0f41f44..2f3ade2 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,6 @@ target +portsat +*.paf report/report.log report/report.aux diff --git a/Cargo.lock b/Cargo.lock index 459569e..8fce58c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -689,6 +689,16 @@ version = "0.3.24" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "58893f751c9b0412871a09abd62ecd2a00298c6c83befa223ef98c52aef40cbe" +[[package]] +name = "portsat" +version = "1.0.0" +dependencies = [ + "lalrpop", + "lalrpop-util", + "lazy_static", + "sat_portfolio", +] + [[package]] name = "precomputed-hash" version = "0.1.1" @@ -950,16 +960,6 @@ dependencies = [ "winapi", ] -[[package]] -name = "ter" -version = "0.1.0" -dependencies = [ - "lalrpop", - "lalrpop-util", - "lazy_static", - "sat_portfolio", -] - [[package]] name = "term" version = "0.7.0" diff --git a/Cargo.toml b/Cargo.toml index 67d65dc..463525e 100644 --- a/Cargo.toml +++ b/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 (quentinjanuel.pro@gmail.com)", + "Sylvain Declercq (syl.dec@live.fr)", + "Christophe Yang (christopheyang@live.fr)", ] license = "MIT" diff --git a/README.md b/README.md index 7d0c750..4b46aae 100644 --- a/README.md +++ b/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 -f -fo [-a ] [-s ] [--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 -``` \ No newline at end of file diff --git a/makefile b/makefile new file mode 100644 index 0000000..073463c --- /dev/null +++ b/makefile @@ -0,0 +1,5 @@ +NAME = portsat + +build: + cargo build --release + cp target/release/$(NAME) $(NAME) \ No newline at end of file diff --git a/src/af/extension.rs b/src/af/extension.rs index 882a7ca..6ca3793 100644 --- a/src/af/extension.rs +++ b/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(" ")) } } diff --git a/src/af/format.rs b/src/af/format.rs index 89a942c..0cd9b69 100644 --- a/src/af/format.rs +++ b/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)), } } diff --git a/src/af/mod.rs b/src/af/mod.rs index b330f84..8e42c8b 100644 --- a/src/af/mod.rs +++ b/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::().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::().unwrap() - 1; + let b_ind = b.parse::().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(); diff --git a/src/main.rs b/src/main.rs index dc3b0d6..03922b5 100644 --- a/src/main.rs +++ b/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(); diff --git a/src/problem/semantics.rs b/src/problem/semantics.rs index 2270a08..e609acb 100644 --- a/src/problem/semantics.rs +++ b/src/problem/semantics.rs @@ -3,7 +3,7 @@ use std::{ convert::TryFrom, }; -#[derive(Clone)] +#[derive(Clone, PartialEq)] pub enum Semantics { Complete, Grounded, diff --git a/src/solver/grounded.rs b/src/solver/grounded.rs index 18477c2..1003660 100644 --- a/src/solver/grounded.rs +++ b/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(()) } \ No newline at end of file diff --git a/src/solver/mod.rs b/src/solver/mod.rs index 7fa5522..e765c75 100644 --- a/src/solver/mod.rs +++ b/src/solver/mod.rs @@ -16,7 +16,7 @@ pub fn solve( af: AF, problem: Problem, sat_solver: Option>, - 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(()) } diff --git a/src/solver/preferred/enum_co.rs b/src/solver/preferred/enum_co.rs index 3446f23..9fe4f36 100644 --- a/src/solver/preferred/enum_co.rs +++ b/src/solver/preferred/enum_co.rs @@ -57,26 +57,28 @@ pub fn solve( Task::Enumerate => println!("[{}]", preferred.iter() .map(|e| e.to_string()) .collect::>() - .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!(), diff --git a/src/solver/preferred/mod.rs b/src/solver/preferred/mod.rs index cb78518..7c22fe8 100644 --- a/src/solver/preferred/mod.rs +++ b/src/solver/preferred/mod.rs @@ -11,11 +11,15 @@ pub fn solve( af: &AF, task: &Task, sat_solver: Option>, - 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) + // } } \ No newline at end of file diff --git a/src/solver/stable_complete.rs b/src/solver/stable_complete.rs index aa1ad94..0395ac2 100644 --- a/src/solver/stable_complete.rs +++ b/src/solver/stable_complete.rs @@ -53,7 +53,7 @@ where .iter() .map(|m| format!("{}", Extension::new(af, m))) .collect::>() - .join(","), + .join(", "), ) } Task::Credulous(arg) => { @@ -65,8 +65,10 @@ where BenchmarkTask::SATSolving, sat_solver.solve(&cnf), ); - if let Some(_) = model { + if let Some(model) = model { println!("YES"); + let extension = Extension::new(af, &model); + println!("{}", extension); } else { println!("NO"); } @@ -80,8 +82,10 @@ where BenchmarkTask::SATSolving, sat_solver.solve(&cnf), ); - if let Some(_) = model { + if let Some(model) = model { println!("NO"); + let extension = Extension::new(af, &model); + println!("{}", extension); } else { println!("YES"); } diff --git a/src/utils/mod.rs b/src/utils/mod.rs index 53d33e0..c50bbd0 100644 --- a/src/utils/mod.rs +++ b/src/utils/mod.rs @@ -23,7 +23,7 @@ pub fn details() { let author = env!("CARGO_PKG_AUTHORS") .split(":") .collect::>() - .join(", "); + .join("\n"); println!("{} v{}\n{}", name, version, author); } diff --git a/src/utils/solvers.rs b/src/utils/solvers.rs index a5dc990..532e2a3 100644 --- a/src/utils/solvers.rs +++ b/src/utils/solvers.rs @@ -46,20 +46,41 @@ pub fn show_available() { println!("[{}]", s); } -pub fn get_from_arg(arg: Option<&str>) -> Option> { - arg.map(|solver_names| { - let mut solvers: Vec> = vec![]; - let all_solvers = get_all(); - for solver_name in solver_names.split(',') { - if let Some(solver_gen) = all_solvers.get(solver_name) { - solvers.push(solver_gen().into()); - } else { - panic!("Unknown solver: {}", solver_name); - } - } - if solvers.len() < 1 { - panic!("No solver specified"); - } - Box::new(Portfolio::from(solvers)) as Box - }) +pub fn get_from_arg(/*arg: Option<&str>*/is_gr: bool) -> Option> { + // arg.map(|solver_names| { + // let mut solvers: Vec> = vec![]; + // let all_solvers = get_all(); + // for solver_name in solver_names.split(',') { + // if let Some(solver_gen) = all_solvers.get(solver_name) { + // solvers.push(solver_gen().into()); + // } else { + // panic!("Unknown solver: {}", solver_name); + // } + // } + // if solvers.len() < 1 { + // panic!("No solver specified"); + // } + // Box::new(Portfolio::from(solvers)) as Box + // }) + if is_gr { + None + } else { + Some(Box::new(Portfolio::from(vec![ + Arc::new(Manysat::new()), + Arc::new(Minisat::new()), + Arc::new(Maplesat::new()), + Arc::new(Glucose::new()), + Arc::new({ + let mut s = Glucose::new(); + s.enable_preprocessing(); + s + }), + // Arc::new({ + // let mut s = Glucose::new(); + // s.enable_syrup(); + // s + // }), + // Arc::new(DPLL::new()), + ]))) + } }