CRISNER ("chrissner"): A Qualitative Preference Reasoner

Conditional & Relative Importance Statement Network PrEference Reasoner (renamed from iPrefR to be more specific)

NEW Slides for AAAI 2014 Tutorial on Representing and Reasoning with Qualitative Preferences: Tools and Applications (pdf)

About

CRISNER is a practical reasoner tool for preferences expressed in qualitative preference languages. CRISNER is founded on decision theory, formal methods and software engineering.

Supported Features

• XML-based specification of preferences in a variety of qualitative preference languages -- CP-nets, TCP-nets, CP-Theories
• XML-based specification of preference queries (consistency, dominance) and their results for preferences stated in the above languages
• Preference reasoning via model checking -- by translating a preference specification into a Kripke Structure model and preference queries into temporal logic queries against this model
Note: The translation is performed at the higher level of preference rules rather than at the level of the induced preference graph, i.e., it takes as input the preference rules in the preference specification and produces a succinct specification of the Kripke Structure model. Hence, CRISNER never constructs the induced preference graph upfront. For more details, see Dominance Testing via Model Checking
• Provide explanation of the result of preference queries -- proof of dominance, inconsistency (cycles in the induced preference graph)

Reasoning Tasks

• Dominance Testing
• Consistency Checking
• Dominance Performance Test
• *Preference equivalence (subsumption) Checking whether one set of preferences induces the same set (or a subset) of preferences over outcomes as induced by another set of preferences

* The functionalities for equivalence and subsumption checking is currently being integrated into CRISNER and tested. It will be available for download shortly.

Platform & Dependencies

CRISNER is implemented in Java. It requires the following dependencies.

• Java Runtime Environment (tested with JRE 1.7)
  Third party Java libraries used (dependencies):
• guava-16.0.1
• xmlpull-1.1.3.1
• xpp3_min-1.1.4
• xstream-1.4.7
• jopt-simple-4.8.jar
• NuSMV model checker version 2.5.4

Work in Progress

• Support for reasoning with CI-nets
• Handle multiple stakeholders at different levels of authority who may hold possibly conflicting preferences
• Additional reasoning tasks -- Computing an ordering of the outcomes (The next-best solution)

Getting CRISNER

• Please send me an email at gsanthan@iastate.edu or ganeshram.santhanam@gmail.com to get the latest version of CRISNER.

Running CRISNER

To run CRISNER, ensure that NuSMV is installed and use one of the following commands, depending on whether you are starting with a preference specification or a query specification. The CRISNER.jar includes the needed java library dependencies listed above. If starting with a preference specification file (more about it below), then use the option "-s".

C:\Users\user>java -jar CRISNER.jar -s <"path to preference specification xml file"> -m <"path to NuSMV executable">

If starting with a query specification file (more about it below), then use the option "-q".

C:\Users\user>java -jar CRISNER.jar -q <"path to query specification xml file"> -m <"path to NuSMV executable">

In either case, the command line option should include the path to the NuSMV model checker executable, or an error will be reported.

USAGE:
 Please specify the model checker command to use AND the path to either:  (1) a preference specification file OR (2) query specification file.
 Example: "java -jar CRISNER.jar -m C:\Program files\NuSMV\bin\2.5.4\NuSMV.exe -s C:\Data\prefspec.xml" or "java -jar CRISNER.jar -m NuSMV -q query.xml"

For more on preference and query specification files, see examples below.

XML Syntax

Specifying preferences via an XML file

CRISNER accepts a preference specification for one of the above languages in a pre-specified XML format. The preference specification consists of a declaration of the preference variables, their domains and a set of preference statements each of which expresses a preference relation over the domain of that variable. There are examples below.

CRISNER then parses the XML to extract the preference rules and builds a corresponding SMV model (saved as a .smv file) suitable for model checking by the NuSMV model checker (version 2.5.4). This translation is based on our AAAI 2010 paper Dominance Testing via Model Checking and as presented in the AAAI 2014 tutorial.

Querying a preference specification

CRISNER allows querying a preference specification via either an XML file that specifies the reference preference specification, the query and its parameters, or via a reasoning menu served via the console interface when the tool is run with the "-s" option. Currently the tool supports dominance and consistency. In the future we plan to add anytime computation of an ordering of all outcomes (sequence of next-preferred outcomes respecting the preference rules); this is work in progress. If you are in need of this immediately, please send an email to get the latest working version for this functionality.

• Querying using an XML file

  CRISNER can accept queries for consistency and dominance via a pre-specified XML format see below. The XML contains the query type (consistency/dominance) and in the case of dominance queries, the dominating (better) and dominated (worse) outcomes are required.

• Querying via the console interface

  When running the tool with the "-s" option, CRISNER provides a simple menu via the console interface using which the user can perform consistency, dominance queries against the given preference specification. The console additionally provides a way to perform dominance testing for a given number of randomly generated pairs of outcomes for a preference specification.

• Viewing Query Results

  The results of a query contain a boolean result (true/false) and if applicable, a proof of the result, i.e., inconsistency (a cycle of outcomes) or a proof of dominance (a flipping sequence).

Downloadable Examples

• Example 1a: Specifying a CP-net with consistent preferences (cycle-free induced preference graph)

• Preference Specification

This basic preference specification for a CP-net shows how to declare variables and their domains, e.g., the following (excerpt from the above xml file) declares a preference variable a with a binary domain with values 0 and 1. Note that these valuations can take string values that are combinations of letters and numbers.

<PREFERENCE-VARIABLE>
 <VARIABLE-NAME>a</VARIABLE-NAME>
 <DOMAIN-VALUE>0</DOMAIN-VALUE>
 <DOMAIN-VALUE>1</DOMAIN-VALUE>
</PREFERENCE-VARIABLE>
	  

The following part of the specification declares a conditional preference over values of the variable c conditioned on the variable b. Note that there can be multiple conditions or no conditions as well. In addition, there can also be multiple preferences for a variable, e.g., if there is a variable with domain of {0,1,TestVal} then to specify the total order 0 > 1 > TestVal one would encode 0 > 1 as one preference followed by 1 > TestVal. The tool requires that the variable names and their assignments match with the preference variable declarations in the file.

<PREFERENCE-STATEMENT>
<STATEMENT-ID>p3</STATEMENT-ID>
<PREFERENCE-VARIABLE>c</PREFERENCE-VARIABLE>
<CONDITION>b=0</CONDITION>
<PREFERENCE>0:1</PREFERENCE>
</PREFERENCE-STATEMENT>
	  

• Graphical Illustration of the CP-net



• Induced Preference Graph



• Translated SMV model

In the translated SMV model, notice that each preference variable corresponds to a variable in the model, and the conditional preference table of a variable x is encoded within the next(x) section. This is how the tool succinctly encodes the preference specification without actually expanding the induced preference graph.

MODULE main

VAR
  a : {0,1};
  c : {0,1};
  b : {0,1};
  gch : {0,1};

FROZENVAR
  a_0 : {0,1};
  b_0 : {0,1};
  c_0 : {0,1};
IVAR
  cha : {0,1};
  chb : {0,1};
  chc : {0,1};

DEFINE
start := a=a_0 & b=b_0 & c=c_0;

INIT start=TRUE;
TRANS a_0=next(a_0) & b_0=next(b_0) & c_0=next(c_0);

ASSIGN
  next(a) :=
    case
      a=1 & cha=1 & chb=0 & chc=0 : 0; -- #p1 : null => a=[0:1]  >> []
      TRUE : a;
    esac;
  next(c) :=
    case
      c=1 & b=0 & cha=0 & chb=0 & chc=1 : 0; -- #p3 : [b=0] => c=[0:1]  >> []
      TRUE : c;
    esac;
  next(b) :=
    case
      b=0 & c=0 & cha=0 & chb=1 & chc=0 : 1; -- #p2 : [c=0] => b=[1:0]  >> []
      TRUE : b;
    esac;
  next(gch) :=
    case
      a=1 & cha=1 & chb=0 & chc=0 : 1;
      c=1 & b=0 & cha=0 & chb=0 & chc=1 : 1;
      b=0 & c=0 & cha=0 & chb=1 & chc=0 : 1;
      TRUE: 0;
    esac;

• Example 1b: Reasoning with a CP-net (cycle-free induced preference graph)

• Consistency Checking

  (Query) (Result)

• Consistency Checking via the console interface

  (Query) (Result)

C:\Users\user>java -jar CRISNER.jar -s samples\nocycle-cpnet\nocycle-cpnet.xml -m nusmv

Parsing preference specification ... samples\nocycle-cpnet\nocycle-cpnet.xml

Reasoning options:
[1] Test Dominance
[2] Test Dominance Performance
[3] Test Consistency
[4] Test Subsumption*
[5] Test Equivalence*
[9] Exit
(* - For subsumption and equivalence, we currently require both specifications to have the same set of preference variables and respective domains.)
Enter option: 3
Consistent
Result: TRUE; Query File: samples\nocycle-cpnet\nocycle-cpnet.xml-consistencyquery.xml

• Consistency Checking via a query file

  (Query) (Result)

C:\Users\user>java -jar CRISNER.jar -q samples\nocycle-cpnet\nocycle-cpnet.xml-consistencyquery.xml -m nusmv

Parsing query specification ... samples\nocycle-cpnet\nocycle-cpnet.xml-consistencyquery.xml
Consistent
Result: TRUE; Query File: samples\nocycle-cpnet\nocycle-cpnet.xml-consistencyquery.xml

• Dominance Testing

• Does <0,1,0> dominate <1,0,1>?

  (Query) (Result)

Reasoning options:
[1] Test Dominance
[2] Test Dominance Performance
[3] Test Consistency
[4] Test Subsumption*
[5] Test Equivalence*
[9] Exit
(* - For subsumption and equivalence, we currently require both specifications to have the same set of preference variables and respective domains.)
Enter option: 1
Dominating alternative
a = ? 0
b = ? 1
c = ? 0
Dominated alternative
a = ? 1
b = ? 0
c = ? 1
Please specify a file name to save query (optional): nocycle-cpnet-q1.xml

Result: TRUE; Proof: Sequence: [c = 1, a = 1, b = 0] -> [c = 1, a = 1, b = 0] -> [c = 0, a = 1, b = 0] -> [c = 0, b = 1, a = 1] -> [c = 0, b = 1, a = 0]; Query File: samples\nocycle-cpnet\nocycle-cpnet-q1.xml
Continue with another dominance test? [Y/N]

• Does <0,1,0> dominate <1,1,1>?

  (Query) (Result)

Continue with another dominance test? [Y/N] y
Dominating alternative
a = ? 0
b = ? 1
c = ? 0
Dominated alternative
a = ? 1
b = ? 1
c = ? 1
Please specify a file name to save query (optional): nocycle-cpnet-q2.xml

Result: FALSE; Query File: samples\nocycle-cpnet\nocycle-cpnet-q2.xml
Continue with another dominance test? [Y/N]

• Example 2: CP-net with inconsistent preferences (cyclic induced preference graph)

• Preference Specification

• Graphical Illustration of the CP-net



• Induced Preference Graph



• Translated SMV model

MODULE main

VAR
  c : {0,1};
  b : {0,1};
  a : {0,1};
  gch : {0,1};

FROZENVAR
  a_0 : {0,1};
  b_0 : {0,1};
  c_0 : {0,1};
IVAR
  cha : {0,1};
  chb : {0,1};
  chc : {0,1};

DEFINE
start := a=a_0 & b=b_0 & c=c_0;

INIT start=TRUE;
TRANS a_0=next(a_0) & b_0=next(b_0) & c_0=next(c_0);

ASSIGN
  next(c) :=
    case
      c=0 & a=0 & cha=0 & chb=0 & chc=1 : 1; -- #p4 : [a=0] => c=[1:0]  >> []
      c=1 & b=0 & cha=0 & chb=0 & chc=1 : 0; -- #p3 : [b=0] => c=[0:1]  >> []
      TRUE : c;
    esac;
  next(b) :=
    case
      b=0 & c=0 & cha=0 & chb=1 & chc=0 : 1; -- #p2 : [c=0] => b=[1:0]  >> []
      TRUE : b;
    esac;
  next(a) :=
    case
      a=1 & cha=1 & chb=0 & chc=0 : 0; -- #p1 : null => a=[0:1]  >> []
      TRUE : a;
    esac;
  next(gch) :=
    case
      c=0 & a=0 & cha=0 & chb=0 & chc=1 : 1;
      c=1 & b=0 & cha=0 & chb=0 & chc=1 : 1;
      b=0 & c=0 & cha=0 & chb=1 & chc=0 : 1;
      a=1 & cha=1 & chb=0 & chc=0 : 1;
      TRUE: 0;
    esac;

• Consistency Checking

  (Query) (Result)

C:\Users\user>java -jar CRISNER.jar -s samples\cycle-cpnet\cycle-cpnet.xml -m nusmv

Parsing preference specification ... samples\cycle-cpnet\cycle-cpnet.xml

Reasoning options:
[1] Test Dominance
[2] Test Dominance Performance
[3] Test Consistency
[4] Test Subsumption*
[5] Test Equivalence*
[9] Exit
(* - For subsumption and equivalence, we currently require both specifications to have the same set of preference variables and respective domains.)
Enter option: 3
Cycle found. Sequence: [c = 1, a = 0, b = 0] -> [c = 0, a = 0, b = 0] -> [c = 1, a = 0, b = 0]

Result: FALSE; Proof: Sequence: [c = 1, a = 0, b = 0] -> [c = 0, a = 0, b = 0] -> [c = 1, a = 0, b = 0]; Query File: samples\cycle-cpnet\cycle-cpnet.xml-consistencyquery.xml

Reasoning options:
[1] Test Dominance
[2] Test Dominance Performance
[3] Test Consistency
[4] Test Subsumption*
[5] Test Equivalence*
[9] Exit
(* - For subsumption and equivalence, we currently require both specifications to have the same set of preference variables and respective domains.)
Enter option:

• Example 3: TCP-net with consistent preferences (cycle-free induced preference graph)

• Preference Specification

Notice that the relative importance of a over b is specified by stating that the intra-variable PREFERENCE over valuations of a is REGARDLESS-OF b as in the below excerpt.

  <PREFERENCE-STATEMENT>
    <STATEMENT-ID>p1</STATEMENT-ID>
    <PREFERENCE-VARIABLE>a</PREFERENCE-VARIABLE>
    <PREFERENCE>0:1</PREFERENCE>
    <REGARDLESS-OF>b</REGARDLESS-OF>
  </PREFERENCE-STATEMENT>

• Graphical Illustration



• Induced Preference Graph



• Translated SMV model

MODULE main

VAR
  b : {0,1};
  c : {0,1};
  a : {0,1};
  gch : {0,1};

FROZENVAR
  a_0 : {0,1};
  b_0 : {0,1};
  c_0 : {0,1};
IVAR
  cha : {0,1};
  chb : {0,1};
  chc : {0,1};

DEFINE
start := a=a_0 & b=b_0 & c=c_0;

INIT start=TRUE;
TRANS a_0=next(a_0) & b_0=next(b_0) & c_0=next(c_0);

ASSIGN
  next(b) :=
    case
      a=1 & cha=1 & chb=1 & chc=0 : {0,1}; -- #p1 : [] => a=[0:1]  >> [b]
      b=0 & c=0 & cha=0 & chb=1 & chc=0 : 1; -- #p2 : [c=0] => b=[1:0]  >> []
      TRUE : b;
    esac;
  next(c) :=
    case
      c=1 & b=0 & cha=0 & chb=0 & chc=1 : 0; -- #p3 : [b=0] => c=[0:1]  >> []
      TRUE : c;
    esac;
  next(a) :=
    case
      a=1 & cha=1 & chb=1 & chc=0 : 0; -- #p1 : [] => a=[0:1]  >> [b]
      TRUE : a;
    esac;
  next(gch) :=
    case
      a=1 & cha=1 & chb=1 & chc=0 : 1;
      b=0 & c=0 & cha=0 & chb=1 & chc=0 : 1;
      c=1 & b=0 & cha=0 & chb=0 & chc=1 : 1;
      a=1 & cha=1 & chb=1 & chc=0 : 1;
      TRUE: 0;
    esac;

• Dominance Performance Test

This menu option allows the user to run a specified number of dominance tests (each test selects a random pair of outcomes) on a given preference specification. For more on generating CP-nets at random, a different problem, see related work by Judy Goldsmith's group at UKY. The below run shows what happens when we ask CRISNER to test dominance on 5 pairs of outcomes. Each dominance test query is saved in its corresponding query specification xml file as indicated, and the corresponding query results are also saved in xml files for the user to investigate them later. The query results will contain a proof of dominance if the dominance holds for that query.

C:\Users\user>java -jar CRISNER.jar -s samples\nocycle-tcpnet\nocycle-tcpnet.xml -m nusmv

Parsing preference specification ... samples\nocycle-tcpnet\nocycle-tcpnet.xml

Reasoning options:
[1] Test Dominance
[2] Test Dominance Performance
[3] Test Consistency
[4] Test Subsumption*
[5] Test Equivalence*
[9] Exit
(* - For subsumption and equivalence, we currently require both specifications to have the same set of preference variables and respective domains.)
Enter option: 2
Enter number of specifications to test: 5
QUERY     1   (a=0 & b=0 & c=1)                                  -> EX EF (a=1 & b=0 & c=0)

QUERY     2   (a=1 & b=0 & c=1)                                  -> EX EF (a=1 & b=0 & c=0)

QUERY     3   (a=0 & b=1 & c=1)                                  -> EX EF (a=0 & b=1 & c=1)

QUERY     4   (a=1 & b=1 & c=1)                                  -> EX EF (a=0 & b=0 & c=0)

QUERY     5   (a=0 & b=0 & c=0)                                  -> EX EF (a=1 & b=1 & c=0)

Dominance does not hold
Result: FALSE; Query File: samples\nocycle-tcpnet\nocycle-tcpnet.xml-query1.xml
QUERY     1   false         137   ms
Dominance does not hold
Result: FALSE; Query File: samples\nocycle-tcpnet\nocycle-tcpnet.xml-query2.xml
QUERY     2   false         107   ms
Dominance does not hold as the outcomes are equal
Result: FALSE; Query File: samples\nocycle-tcpnet\nocycle-tcpnet.xml-query3.xml
QUERY     3   false          90   ms
Dominance does not hold
Result: FALSE; Query File: samples\nocycle-tcpnet\nocycle-tcpnet.xml-query4.xml
QUERY     4   false         104   ms
Dominance holds.
Sequence: [c = 0, b = 1, a = 1] -> [] -> [a = 0, b = 0]
Sequence: [c = 0, b = 1, a = 1] -> [c = 0, b = 1, a = 1] -> [c = 0, a = 0, b = 0]
Proof of dominance:
Sequence: [c = 0, b = 1, a = 1] -> [c = 0, b = 1, a = 1] -> [c = 0, a = 0, b = 0]
Result: TRUE; Proof: Sequence: [c = 0, b = 1, a = 1] -> [c = 0, b = 1, a = 1] -> [c = 0, a = 0, b = 0]; Query File: samples\nocycle-tcpnet\nocycle-tcpnet.xml-query5.xml
QUERY     5   true          119   ms

Average time per dominance test: 111 ms

Preference Subsumption and Equivalence Test

This menu option allows the user to check if the already specified preference specification induces preferences subsumed by those induced by another preference specification.

C:\Users\user>java -jar CRISNER.jar -s samples\nocycle-cpnet\nocycle-cpnet.xml -m nusmv

Parsing preference specification ... samples\nocycle-cpnet\nocycle-cpnet.xml

Reasoning options:
[1] Test Dominance
[2] Test Dominance Performance
[3] Test Consistency
[4] Test Subsumption*
[5] Test Equivalence*
[9] Exit
(* - For subsumption and equivalence, we currently require both specifications to have the same set of preference variables and respective domains.)
Enter option: 4
Please enter another XML preference specification to test subsumption: 
Enter the location of the XML file: samples\nocycle-tcpnet\nocycle-tcpnet.xml
Is nocycle-cpnet.xml subsumed by nocycle-tcpnet.xml ?
Subsumption holds.
true; nocycle-cpnet.xml is subsumed by nocycle-tcpnet.xml

Reasoning options:
[1] Test Dominance
[2] Test Dominance Performance
[3] Test Consistency
[4] Test Subsumption*
[5] Test Equivalence*
[9] Exit
(* - For subsumption and equivalence, we currently require both specifications to have the same set of preference variables and respective domains.)
Enter option: 5
Please enter another XML preference specification to test equivalence: 
Enter the location of the XML file: samples\nocycle-tcpnet\nocycle-tcpnet.xml
Is nocycle-cpnet.xml subsumed by nocycle-tcpnet.xml ?
Subsumption holds.
Is nocycle-tcpnet.xml subsumed by nocycle-cpnet.xml ?
Subsumption does not hold.
false; nocycle-cpnet.xml is not equivalent to nocycle-tcpnet.xml

For further details regarding the usage of CRISNER or for help integrating CRISNER into your project, please contact me at the address on top of this page.
Please cite the following paper which contains the theoretical foundations of the tool Dominance Testing via Model Checking by Santhanam et al. (AAAI 2010).
Other publications related to preference reasoning

Funding and Support

The research activities of the project were supported in parts by US National Science Foundation grants CCF 1143734 and CCF 0702758.

Collaborators

• Dr. Samik Basu Department of Computer Science, Iowa State University
• Dr. Vasant Honavar College of Information Science and Technology, Penn State University

Updated: Jan, 2015