(!******************************************************
Mosel Example Programs
======================
file cnf2mos.mos
````````````````
A (W)CNF to MOS converter.
(c) 2020 Fair Isaac Corporation
author: Y.Colombani, Jun. 2020
*******************************************************!)
model cnf2mos
version 0.0.1
uses 'mmsystem','deploy'
parameters
F="Rounded_BTWBNSL_asia_100_1_3.scores_TWBound_2.wcnf.gz" ! File to convert
MAXLEN=80 ! Maximum length of lines (for printing the objective)
end-parameters
declarations
! The following text is added before calling 'minimise'
before_solve=`
setparam('xprs_loadnames', true)
`
src,dest,fname,prefix: text ! Handling of filenames
line,objtext: text ! Aux. texts
nbvar,nbcl,nbwc: integer ! Various counters
whrd: real ! Weight value for binding clauses
iswcnf: boolean ! Whether problem is a WCNF
curlen: integer ! Line length indicator
wcfile="tmp:"+newmuid
! Subroutines defined by this program
procedure skipcomment(l:text)
procedure parseoptions(l:text)
procedure parseclause(l:text)
procedure displayclause(lst:list of integer)
procedure displaynotclause(lst:list of integer)
end-declarations
! Check for filename argument and display 'usage' banner if none is found
if argc=1 and argv(1)="mosel" then ! Not deployed: use model parameter
if F="" then
writeln("Usage: mosel cnf2mos F=filename (.cnf[.gz] or .wcnf[.gz])")
exit(1)
else
fname:=F
end-if
elif argc<>2 then
writeln("Usage: cnf2mos filename (.cnf[.gz] or .wcnf[.gz])")
exit(1)
else
fname:=argv(2)
end-if
! Check whether input file is compressed
src:=pathsplit(SYS_FNAME,fname)
if endswith(src,".gz") then
prefix:="zlib.gzip:"
dest:=src-".gz"
else
dest:=src
end-if
! Supported extensions: .cnf and .wcnf
if endswith(dest,".cnf") then
dest:=(dest-".cnf")+".mos"
elif endswith(dest,".wcnf") then
dest:=(dest-".wcnf")+".mos"
else
dest+=".mos"
end-if
! Don't overwrite existing file
if getfstat(dest)<>0 then
writeln("File '", dest, "' exists - aborting")
exit(2)
end-if
! Start the transformation
fopen(prefix+fname,F_INPUT)
writeln("Generating '", dest, "'...")
fopen(dest,F_OUTPUT)
! Header text for generated file
writeln("! Generated by cnf2mos v",getparam("model_version")," from '",src,"'");
writeln("model sat\nuses 'mmxprs'\n")
! Process the clauses
nbcl:=1
curlen:=5
while(readtextline(line)>0 and nbcl>0) do
case getchar(line,1) of
99: ! c
skipcomment(line)
112: ! p
parseoptions(line)
else
parseclause(line)
end-case
end-do
writeln
! Objective function for MAXSAT case, solver call and solution reporting
if iswcnf and objtext.size>0 then
if nbwc>0 then
writeln("RW:=1..",nbwc,"\nfinalise(RW)")
fclose(F_OUTPUT)
fcopy(wcfile,0,dest,F_APPEND)
fopen(dest,F_OUTPUT+F_APPEND)
writeln
end-if
deltext(objtext,1,1) ! remove leading '+'
writeln("Obj:=",objtext,"\n")
write(before_solve)
writeln("minimise(Obj)")
else
write(before_solve)
writeln("minimise(1)")
end-if
write(`
if getprobstat<>XPRS_OPT then
writeln("Problem is infeasible")
else
writeln("Solution:")
`)
if iswcnf then
writeln(' writeln(" Obj=", getobjval)')
end-if
writeln(`
forall(i in R | b(i).sol) write(" b(", i, ")")
writeln
end-if
end-model
`)
!**************** Implementation of subroutines ****************
! Skip comment line
procedure skipcomment(l:text)
deltext(l,1,1)
write("! ",l)
end-procedure
! Read options/instance parameters and generate Mosel declarations
procedure parseoptions(l:text)
type:=parsetext(l,3)
if type<>"cnf" and type<>"wcnf" then
fclose(F_INPUT)
fclose(F_OUTPUT)
writeln("Unsupported format '",type,"' - aborting")
exit(3)
end-if
asproc(nextfield(l))
nbvar:=parseint(l)
asproc(nextfield(l))
nbcl:=parseint(l)
if type="wcnf" then
iswcnf:=true
asproc(nextfield(l))
whrd:=parsereal(l)
end-if
writeln("public declarations\n R=1..",nbvar,"\n b: array(R) of boolvar")
if iswcnf then
writeln(" RW: range\n w: array(RW) of boolvar")
end-if
writeln("end-declarations\n")
writeln("writeln('Model generated from file \"",src,"\"')")
writeln("writeln('Problem size:')")
writeln("writeln(' variables: ",nbvar,"')")
writeln("writeln(' clauses: ",nbcl,"')")
if iswcnf then
writeln("writeln(' top weight:",whrd,"')")
end-if
writeln
end-procedure
! Read a clause
procedure parseclause(l:text)
declarations
lst:list of integer
firstval:boolean
txtline:text
end-declarations
setparam("sys_endparse",0)
firstval:=true
while(nextfield(l))
if iswcnf and firstval then
firstval:=false
weight:=parsereal(l)
else
lst+=[parseint(l)]
end-if
if iswcnf and weight<>whrd then
wtxt:=if(weight<>1,text(weight)+"*",text(""))
if lst.size=2 then ! only 1 value and 0
if lst(1)<0 then
txtline:=wtxt+"b("+(-lst(1))+").var"
else
txtline:=wtxt+"getvar(not b("+lst(1)+"))"
end-if
else ! 2 or more values
nbwc+=1
txtline:=wtxt+"w("+nbwc+").var"
fopen(wcfile,F_OUTPUT+F_APPEND)
write("w(",nbwc,")=(")
displaynotclause(lst)
writeln(")")
fclose(F_OUTPUT)
end-if
if curlen+txtline.size+1>MAXLEN then
curlen:=4+txtline.size
objtext+=text("+\n ")+txtline
else
curlen+=txtline.size+1
objtext+=text("+")+txtline
end-if
else
displayclause(lst)
writeln
end-if
nbcl-=1
end-procedure
! Output a clause in Mosel format
procedure displayclause(lst:list of integer)
declarations
firstdone:boolean
end-declarations
forall(i in lst|i<>0) do
if firstdone then
write(" or ")
else
firstdone:=true
end-if
if i<0 then
write("not b(",-i,")")
else
write("b(",i,")")
end-if
end-do
end-procedure
! Output the negation of a clause in Mosel format
procedure displaynotclause(lst:list of integer)
declarations
firstdone:boolean
end-declarations
forall(i in lst|i<>0) do
if firstdone then
write(" and ")
else
firstdone:=true
end-if
if i<0 then
write("b(",-i,")")
else
write("not b(",i,")")
end-if
end-do
end-procedure
end-model
|
