To use Nichrome, we need to first install and configure the PostgreSQL database, and provide a configuration file to help Nichrome find the software it depends on.

  1. Install PostgreSQL.

    Download and unpack the source of PostgreSQL. Let PG_DIST be the path where the source is unpaked and PG_INSTALL be the path where you want PostgreSQL to be installed, then build and install PostgreSQL as follows:

    cd PG_DIST 							
    ./configure –prefix=PG_INSTALL
    make; make install 
    cd PG_DIST/contrib/intarray 
    make; make install				
    cd PG_DIST/contrib/intagg 
    make; make install

    Then configure PostgreSQL as follows:

    cd PG_INSTALL/bin
    ./initdb -D ../data
    ./pg_ctl -D ../data/ -l ../log  start
    ./createuser -s -P Nichrome
    # Provide a password you like, e.g., Nichrome
    ./createdb Nichromedb
    

  2. Define a configuration file.

    Below is an example configuration file, which we will refer to as "Nichrome.conf".

    db_url = jdbc:postgresql://localhost:5432/Nichromedb
    
    # Database username; must be a superuser
    db_username = Nichrome
    
    # The password for db_username
    db_password = Nichrome
    
    # The working directory; Nichrome may write sizable temporary data here
    dir_working = <work-dir>
    
    maxsat = <path of the MaxSAT solver>
    lbx = <path of lbx>
    mcsls = <path of mcsls>

Nichrome currently supports MAP inference for MLN programs. Below is an example MLN program for the graph reachability problem, which we refer to as "graph.mln"

// graph.mln
// Define the relations. The "*" means closed-world assumption holds for the specified relation. Otherwise, open-world assumption is applied.
*edge(node,node)
path(node,node)

// Reflexivity
path(n,n).
// If there is a edge from n1 to n2, and there is a path from n2 to n3, then there is a path from n1 to n3. 
// This rule can also be written as 
// !edge(n1,n2) v !path(n2,n3) v path(n1,n3)
edge(n1,n2),path(n2,n3) => path(n1,n3).

// Least-fix-point contraint. Do not derive unnecessary paths.
1 !path(n1,n2)

The file below ("graph.edb") is an input file which defines a graph a --> b --> c.

// graph.edb
edge(a,b)
edge(b,c)

To solve the graph reachability on the graph defined above, we run Nichrome using the command below:

java -jar Nichrome.jar -conf Nichrome.conf -e graph.edb  -r result.txt  -i graph.mln -verbose 2 -solver lbxmcs  -lbxTimeout 18000 -lbxLimit 1 -printVio > log.txt
Nichrome will output the result to "result.txt". Below is the content of it after runing the above command.

// 0 Optimum value: 3.0
// 1 The following variables should be set to true: 
edge(a,b)
edge(b,c)
path(a,a)
path(b,b)
path(c,c)
path(b,c)
path(a,b)
path(a,c)

// 2 The following grounded clauses are not satified: 
// 1.0: NOT path(a,a)
// 1.0: NOT path(b,b)
// 1.0: NOT path(c,c)
// 1.0: NOT path(b,c)
// 1.0: NOT path(a,b)
// 1.0: NOT path(a,c)	

For details about the command options, please run "java -jar Nichrome.jar -help".

Coming soon.