- decides the satisfiability of linear inequalities involving probabilities of classical propositional formulas
- gurobi solver (tested with v6.5)
javac -d bin src/genpsatmip.java to build
java -cp bin/ genpsatmip filename to run the program on file filename.
Input file format
The solver accepts input files in the following format:
- lines that begin with a
care comment lines
- one line that states size of problem such as
p cnf nvar nclauses nprobs, where
nvaris the number of propositional variables
nclausesis the number of propositional clauses
nprobsis the number of probabilistic clauses
- followed by
nclausespropositional clauses which are a sequence of 3 non-null numbers (3CNF) between -nvar and nvar ending with 0 on the same line. Negative numbers correspond to negated variables.
- followed by
nprobsprobabilistic clauses which are of the form TYPE (q0)v0 ... (qn)vn i where TYPE can be EQ, SG, SL, GE, LE, DI (standing for equal, strictly greater/less, greater/less or equal and different), qi and i are rational numbers and vi are variable names.
One example of this format is the following
c usage p cnf nvar nclauses nprobs p cnf 3 2 1 1 -2 3 0 2 1 -3 0 EQ (-0.3)1 (3)2 3
which corresponds to the GenPSAT problem
- v0.1 -- Initial release in August 2016
- C. Caleiro, F. Casal, and A. Mordido. Generalized probabilistic satisfiability. Preprint, SQIG - IT and IST - U Lisboa, 1049-001 Lisboa, Portugal, 2016.