Package org.tweetyproject.logics.qbf.examples

Class QbfReasonersExample

java.lang.Object

org.tweetyproject.logics.qbf.examples.QbfReasonersExample

public class QbfReasonersExample
extends Object

Examples for using QBF solvers.

Author:

Anna Gessler

Constructor Summary

Constructors

Constructor	Description
QbfReasonersExample()	Default

Method Summary

Modifier and Type	Method	Description
static void	main(String[] args)	Demonstrates the use of various Quantified Boolean Formula (QBF) reasoners and solvers with the TweetyProject library.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

QbfReasonersExample

public QbfReasonersExample()

Default

Method Details

main

public static void main(String[] args)
                 throws ParserException,
IOException

Demonstrates the use of various Quantified Boolean Formula (QBF) reasoners and solvers with the TweetyProject library. The method parses belief sets and formulas from files or strings, and evaluates their satisfiability or consistency using different solvers such as NaiveQbfReasoner, CAQE, GhostQ, Qute, and Cadet. The demonstration includes: 1. Parsing belief sets and formulas using the QbfParser. 2. Performing naive classical inference using the NaiveQbfReasoner. 3. Utilizing external QBF solvers (CAQE, GhostQ, Qute, and Cadet) to check satisfiability and consistency of belief sets and formulas. Each solver is evaluated on the same set of inputs to compare their performance and behavior.

Parameters:

args - Command-line arguments (not used in this example).

Throws:

ParserException - If an error occurs during parsing.

IOException - If an error occurs during file I/O operations.