# This example solves boolean satisfiability problems (SAT).
#
# Usage: 'python gencons_sat.py <filename.cnf>'
# Find CNF files in the 'Data' folder
#
# Illustrates two different methods of modeling SAT problems using:
# (a) Uses xpress.And and xpress.Or
# (b) Uses xpress.addgencons
#
# (C) 2020-2025 Fair Isaac Corporation
import sys
import xpress as xp
def read_sat_instance(sat_instance):
"""
Read the cnf file.
CNF file format description c.f. http://www.satcompetition.org/2009/format-benchmarks2009.html
:param sat_instance: SAT instance in CNF format
:return:
"""
lines = []
n_vars = 0 # Number of variables.
n_clauses = 0 # Number of clauses.
try:
with open(sat_instance, 'r') as f:
lines = f.readlines()
except FileNotFoundError as e:
print("Input CNF file not found")
sys.exit(-1)
count = 0
for line in lines:
tokens = line.strip('\n').split()
if tokens[0] == 'c':
count += 1
continue
elif tokens[0] == 'p':
if tokens[1] != 'cnf':
print('error. input file not in cnf format')
sys.exit(-1)
n_vars = int(tokens[2])
n_clauses = int(tokens[3])
print('number of literals = {}. number of clauses = {}'.format(n_vars, n_clauses))
count += 1
break
return n_vars, n_clauses, lines[count:]
def get_disjunctions(lines, x, nx=None):
disjunctions = []
for i in range(len(lines)):
disjunction = []
tokens = lines[i].strip('\n').split()
N = range(len(tokens))
for j in N:
val = int(tokens[j])
if val == 0:
continue
if nx is not None:
expr = nx[-val - 1] if val < 0 else x[val - 1]
else:
expr = 1 - x[-val - 1] if val < 0 else x[val - 1]
disjunction.append(expr)
disjunctions.append(disjunction)
return disjunctions
def create_and_solve_model(n_vars, lines):
"""
:param n_vars: number of literals
:param lines: lines of the CNF file containing terms of the disjunctions
:return:
"""
p = xp.problem()
# Create literals - binary variables.
x = [p.addVariable(vartype=xp.binary, name='x_{}'.format(i + 1)) for i in range(n_vars)]
disjunctions = get_disjunctions(lines, x)
# print("SAT Formula:")
# print(xp.And(*[xp.Or(*disjunctions[i]) for i in range(len(disjunctions))]))
p.addConstraint(xp.And(*[xp.Or(*disjunctions[i]) for i in range(len(disjunctions))]) == 1)
optimize(p, x)
def create_and_solve_model_addgencons(n_vars, n_clauses, lines):
"""
Another way to model SAT using problem.addgencons method.
:param n_vars:
:param n_clauses:
:param lines:
:return:
"""
p = xp.problem()
# Create literals - binary variables.
x = [p.addVariable(vartype=xp.binary, name='x_{}'.format(i + 1)) for i in range(n_vars)]
nx = [p.addVariable(vartype=xp.binary, name='nx_{}'.format(i + 1)) for i in range(n_vars)]
# Create variables that will store the result of the disjunctive terms for bookkeeping.
y = [p.addVariable(vartype=xp.binary, name='y_{}'.format(j + 1)) for j in range(n_clauses)]
is_satisfiable = p.addVariable(vartype=xp.binary, name='is_satisfiable')
p.addConstraint([x[i] + nx[i] == 1 for i in range(n_vars)])
disjunctions = get_disjunctions(lines, x, nx)
con_type = [xp.GenConsType.OR for _ in range(n_clauses)]
con_type.append(xp.GenConsType.AND)
resultant = y
resultant.append(is_satisfiable)
col_start = []
cur_count = 0
for i in range(len(disjunctions)):
col_start.append(cur_count)
cur_count += len(disjunctions[i])
col_start.append(cur_count)
cols = [item for disjunction in disjunctions for item in disjunction]
for i in range(n_clauses):
cols.append(y[i])
p.addGenCons(con_type, resultant, col_start, cols, None, None)
p.addConstraint(is_satisfiable == 1)
optimize(p, x, y)
def optimize(prob, x, y=None):
prob.controls.timelimit = 300 # 5 minutes.
prob.optimize()
print("Problem status is {}".format(prob.attributes.solstatus.name))
if prob.attributes.solstatus in [xp.SolStatus.OPTIMAL, xp.SolStatus.FEASIBLE]:
x_sol = prob.getSolution(x)
y_sol = prob.getSolution(y) if y is not None else None
for i in range(len(x)):
print('{} = {}'.format(x[i], x_sol[i]))
if y is not None:
for j in range(len(y)):
print('{} = {}'.format(y[j], y_sol[j]))
print("Formula satisfiable")
elif prob.attributes.solstatus == xp.SolStatus.INFEASIBLE:
print("Formula unsatisfiable ")
else:
print("Satisfiability unknown")
def run_sat_solver(sat_instance):
n_vars, n_clauses, lines = read_sat_instance(sat_instance)
print("Literals = {}. Clauses = {}".format(n_vars, n_clauses))
create_and_solve_model(n_vars, lines)
# Uncomment the following line to run the alternate version.
#create_and_solve_model_addgencons(n_vars, n_clauses, lines)
if __name__ == '__main__':
if len(sys.argv) != 2:
print("Usage: python gencons_sat.py <filename.cnf>", file=sys.stderr)
sys.exit(-1)
f_name = sys.argv[1]
run_sat_solver(f_name)
|
# Build a Pseudoboolean optimization solver that uses the
# general constraints library.
#
# Usage: 'python gencons_pbo.py <filename.opb>'
# Find OPB files in the 'Data' folder
#
# c.f. http://www.cril.univ-artois.fr/PB16/
# http://www.cril.univ-artois.fr/PB16/format.pdf
# Parser loosely based on http://www.cril.univ-artois.fr/PB16/parser/SimpleParser.cc
#
# (C) 2020-2025 Fair Isaac Corporation
import sys
import re
import xpress as xp
class Term:
def __init__(self, cons, conj):
"""
:param cons: coefficient
:param conj: list of variables in the product
"""
self.constant = cons
self.conjunction = conj
class Constraint:
def __init__(self, trms, sns, r):
"""
:param trms: List of terms in the constraint
:param sns: Sense
:param r: RHS
"""
self.terms = trms
self.sense = sns
self.rhs = r
def ignore_ws(fh):
"""
Skip whitespaces.
:param fh: file object
:return:
"""
while True:
ch = fh.read(1)
if ch == ' ':
continue
else:
move_back(fh)
break
def read_constant(fh):
"""
:param fh: file object
:return: coefficient before a term in an expression
"""
constant = ''
while True:
ch = fh.read(1)
if ch == 'x' or ch == '~' or ch == ' ' or ch == ';':
move_back(fh)
break
else:
constant += ch
return float(constant) if constant != '' else 1.0
def move_back(fh):
"""
Move file ptr one step back.
:param fh: file object
:return:
"""
fh.seek(fh.tell() - 1)
def read_variable(fh):
"""
Read the variable identifier.
:param fh: file object
:return: variable as string
"""
ch = fh.read(1)
if ch != 'x':
print("Error. No variable identifier after negation at fpos {}".format(fh.tell() - 1))
sys.exit(-1)
# Read the variable index.
index = ''
while True:
ch = fh.read(1)
if ch == ' ':
move_back(fh)
break
index += ch
if index == ' ':
print("Error. No index after identifier at fpos {}".format(fh.tell() - 1))
sys.exit(-1)
return 'x' + index
def read_conj(fh):
"""
Read the terms in a conjunction.
:param fh: file object
:return: list of variables (with negations identified by '~' preceding the variable)
"""
conj = []
while True:
ignore_ws(fh)
ch = fh.read(1)
if ch == '+' or ch == '-' or ch == '=' or ch == '<' or ch == '>' or ch == ';':
move_back(fh)
break
if ch == '~':
conj.append('~' + read_variable(fh))
else:
move_back(fh)
conj.append(read_variable(fh))
return conj
def read_term(fh):
"""
Read the entire term of an expression.
:param fh: file object
:return: term of an expression, including the constant
"""
constant = read_constant(fh)
ignore_ws(fh)
conj = read_conj(fh)
if conj is []:
print("Error. Term returned zero or constant at pos {}".format(fh.tell()))
sys.exit(0)
return Term(constant, conj)
def get_objective(fh):
"""
Get the objective term.
:param fh: file object
:return: objective sense, list of terms in the objective
"""
o_terms = []
o_sense = None
# Ignore comments.
ch = ''
while True:
ch = fh.read(1)
if ch == '*':
fh.readline()
else:
break
# Read objective.
if ch == 'm':
s = fh.read(2)
o_sense = ch + s
fh.read(1) # skip the colon
while True:
ignore_ws(fh)
ch = fh.read(1)
if ch == ';':
fh.read(1) # skip newline
break
else:
move_back(fh)
term = read_term(fh)
o_terms.append(term)
return o_sense, o_terms
def get_constraint(fh):
"""
Read all constraints.
:param fh: file object
:return: list of constraint objects
"""
cons = []
c_sense = ''
c_rhs = None
c_expr = []
while True:
ignore_ws(fh)
ch = fh.read(1)
if ch == '\n':
break
elif ch == ';':
cons.append(Constraint(c_expr, c_sense, c_rhs))
if len(cons) % 10000 == 0:
print("Read ", len(cons), "cons")
c_sense = ''
c_rhs = None
c_expr = []
fh.read(1) # skip newline
elif ch == '*':
fh.readline()
elif ch == '>':
c_sense = '>='
fh.read(1)
ignore_ws(fh)
c_rhs = read_constant(fh)
elif ch == '<':
fh.read(1)
c_sense = '<='
ignore_ws(fh)
c_rhs = read_constant(fh)
elif ch == '=':
ignore_ws(fh)
c_sense = '='
c_rhs = read_constant(fh)
else:
move_back(fh)
term = read_term(fh)
c_expr.append(term)
return cons
def build_expr(terms, variables):
"""
:param terms: List of Term objects in the expression
:param variables: Xpress variables expressed in a dictionary
:return: Xpress expression
"""
expr = None
for term in terms:
coeff = term.constant
conjunction = term.conjunction
if len(conjunction) == 1: # linear
expr = coeff * variables[conjunction[0]] if expr is None else expr + coeff * variables[conjunction[0]]
else:
conj_terms = []
for item in conjunction:
if item.startswith('~'):
conj_terms.append(1 - variables[item[1:]])
else:
conj_terms.append(variables[item])
expr = coeff * xp.And(*conj_terms) if expr is None else expr + coeff * xp.And(*conj_terms)
return expr
if __name__ == '__main__':
if len(sys.argv) != 2:
print('A MIP-based Pseudoboolean solver')
print('Usage: python gencons_pbo_solver.py <filename.opb>')
sys.exit(-1)
else:
fname = sys.argv[1]
try:
with open(fname, 'r') as pbo:
line = pbo.readline()
# Read metadata.
pat = re.compile(r'#variable= (\d+)\s+#constraint= (\d+)')
match = re.search(pat, line)
if match:
n_vars = int(match.group(1))
n_cons = int(match.group(2))
print(line)
else:
print('Problem metadata not provided on line 1')
sys.exit(-1)
pbo.seek(0)
obj_sense, obj_terms = get_objective(pbo)
print("Reading objective complete")
constraints = get_constraint(pbo)
print("Reading constraints complete")
# Create the problem
p = xp.problem()
# Define the variables
var_keys = ['x{}'.format(i) for i in range(1, n_vars + 1)]
x = {i: p.addVariable(vartype=xp.binary) for i in var_keys}
# Add objective.
if len(obj_terms) > 1:
obj_expr = build_expr(obj_terms, x)
xp_sense = xp.minimize if obj_sense == 'min' else xp.maximize
p.setObjective(obj_expr, sense=xp_sense)
# Add constraints.
for constraint in constraints:
cons_expr = build_expr(constraint.terms, x)
rhs = constraint.rhs
sense = constraint.sense
if sense == '<=':
p.addConstraint(cons_expr <= rhs)
elif sense == '>=':
p.addConstraint(cons_expr >= rhs)
else:
p.addConstraint(cons_expr == rhs)
print('Finished adding constraints')
# Set a time limit (no limit otherwise).
p.controls.timelimit = 900
p.optimize()
except FileNotFoundError:
print("PBO instance file not found")
sys.exit(-1)
|
